環境
Ubuntu20.04
Spin 6.5.1
背景
さて、店舗セキュリティ事業会社のシステム設計担当である貴方は以下のような、遠隔キーからの指令でシャッターの制御、表口と裏口の施錠を行えるようなシステムの設計を任されました。なおシャッターには高電圧が掛けられ、触れると電気ショックが流される機能があり、むだのない通電や安全性についても考慮する必要があります。例えば、シャッターが上がっている間は通電しないなど。
必要なハードウェア要素を以下とし、
要素技術的に以下の割り振りでA,B,Cの各社にお願いしたほうが良いと判断しました。つぎにシステム全体として要求を満たすために各社に対し、要求を分解して伝える必要があります。A社にはキー操作関連、B社にはドア関連と言った具合に。この分解後の論理構造に誤りがあった場合、各社が完璧に仕事をしたにもかかわらず、全体としての要求を満たすことが出来ない結果となります。例えば、シャッター通電中にドア解錠が可能であったため中に居た子供がドアを開けてシャッターに触り感電してしまうなど。
そのためこの要求分解はシステムを動かす上で非常に重要な作業となるのですが、その責任の重大さにも関わらずこの正しさを保証するには、人間が脳みそを使って論理的試行を巡らせるしか方法は無いように思えます。プログラミングという作業だったらその場でフィードバックがありますが、この作業の場合はフィードバックとなるものが思考実験か各社が作業完了したあとにのみ得られます。いえ、そう思えます。
SPINによる論理の保証
人間の思考実験においては、”シャッターが閉じているときに通電要求があった場合、シャッターに通電させる”と言った、IF-THEN論理構造の集合を用いてシステムの挙動をシミュレーションしていると考えられます。言うは易いですが、最終的にはすべての状態に対し、思考(試行)を終わらせる必要が在るので、考慮漏れの不安が付き纏います。これを計算機にやらせようという試みがモデル検査という分野であり、その一つのツールが今回紹介するSPINです。SPINはPromelaという記述言語を使用してユーザが対象システムの論理モデルを記述し、それを処理して網羅的にその挙動の検査を行います。背景に上げた例を用いて、その利用法を示してみます。
細かなSPIN仕様の説明は省略します。適宜別記事を参照してください。
私は以下の教科書で学習しました。
https://www.amazon.co.jp/gp/product/B01MD13BNP/ref=kinw_myk_ro_title
要求分解
各社への要求分解時点に話を戻します。あなたは以下のように要求を分解しました。
なお、変数空間はKey,Door,ShutterController間で共有していると仮定します。例えばドアの開閉状態はShutterControllerからでも見れます。背景で貼った図を別タブを開いて隣り合わせで確認してみてください。
A社： Key & Key Controller
以下の要求を出せる
REQ_A_01 : 表口ドア 施錠/解錠
REQ_A_02 : 裏口ドア 施錠/解錠
REQ_A_03 : シャッター 上げ/下げ
REQ_A_04 : シャッター通電(電気ショック) ON/OFF
B社：Door Controller
※ドア閉はドアが閉じている状態のこと。
REQ_B_01 : IF 表口ドア閉 THEN IF 表口ドアロック解錠要求 THEN 表口ドアロック解錠
REQ_B_02 : IF 表口ドア閉 THEN IF 表口ドアロック施錠要求 THEN 表口ドアロック施錠
REQ_B_03 : IF 裏口ドア閉 THEN IF 裏口ドアロック解錠要求 THEN 裏口ドアロック解錠
REQ_B_04 : IF 裏口ドア閉 THEN IF 裏口ドアロック施錠要求 THEN 裏口ドアロック施錠
C社： Shutter Controller
REQ_C_01 : IF シャッター上げ要求 THEN シャッター上げ
REQ_C_02 : IF シャッター下げ要求 THEN シャッター下げ
REQ_C_03 : IF シャッター通電ON要求 AND シャッター下げ状態 AND 裏口表口すべてドア閉かつロック施錠
THEN シャッター通電ON
REQ_C_04 : IF シャッター通電OFF要求 THEN シャッター通電OFF
さて、上記の分解後の各社への要求には安全面、エネルギ消費面で穴があります。どこかわかりますか？
SPINで検査
上記の各社への要求をSPINで処理するためにPromela言語で記述してゆきます。最終的なコードは以下にあげています。
github
A社のKey&KeyControllerへの要求ですが、これは要求を素通しして変数格納するだけですので省略し、遠隔キー操作ユーザの振る舞いモデルとして表現します。この振る舞いモデルは可能な操作を羅列しておくことで、SPINではシステム全体が網羅的に状態遷移するように逐次選択して実行検査します。
振る舞いモデルUserコード
active proctype User()
{
printf("User started.\n")
do
:: printf("select door action\n");
// 解錠されたドアのみ開閉できる振る舞い
if
:: door_lock_front_state == DOOR_UNLOCKED ->
if
:: door_front_state = DOOR_OPENED;
printf("door front opened\n");
:: door_front_state = DOOR_CLOSED;
printf("door front closed\n");
:: else
fi;
:: door_lock_back_state == DOOR_UNLOCKED ->
if
:: door_back_state = DOOR_OPENED;
printf("door back opened\n");
:: door_back_state = DOOR_CLOSED;
printf("door back closed\n");
:: else
fi;
:: else
fi;
printf("select action\n");
if
:: door_lock_front_req = DOOR_LOCK_REQ; // REQ_A_01
:: door_lock_front_req = DOOR_UNLOCK_REQ;
:: door_lock_back_req = DOOR_LOCK_REQ; // REQ_A_02
:: door_lock_back_req = DOOR_UNLOCK_REQ;
:: shutter_req = SHUTTER_UP_REQ; // REQ_A_03
:: shutter_req = SHUTTER_DOWN_REQ;
:: es_req = ES_ON_REQ; // REQ_A_04
:: es_req = ES_OFF_REQ;
:: else
fi;
printf("down reqs\n");
door_lock_front_req = NO_REQ;
door_lock_back_req = NO_REQ;
shutter_req = NO_REQ;
es_req = NO_REQ;
od;
}
B社のDoorControllerのコードは以下です。
DoorControllerコード
active proctype DoorController()
{
do
:: if
:: atomic{
// REQ_B_01, REQ_B_02
door_front_state == DOOR_CLOSED->
if
:: atomic{
door_lock_front_req == DOOR_LOCK_REQ ->
door_lock_front_state = DOOR_LOCKED;
printf("front door locked\n");
}
:: atomic{
(door_lock_front_req == DOOR_UNLOCK_REQ) ->
door_lock_front_state = DOOR_UNLOCKED;
printf("front door unlocked\n");
}
:: else
fi;
}
:: else
fi;
if
:: atomic{
// REQ_B_03, REQ_B_04
door_back_state == DOOR_CLOSED->
if
:: atomic{
door_lock_back_req == DOOR_LOCK_REQ ->
door_lock_back_state = DOOR_LOCKED;
printf("back door locked\n");
}
:: atomic{
(door_lock_back_req == DOOR_UNLOCK_REQ) ->
door_lock_back_state = DOOR_UNLOCKED;
printf("back door unlocked\n");
}
:: else
fi;
}
:: else
fi;
od
}
C社のShutterControllerのコードは以下です。
ShutterControllerコード
active proctype ShutterController()
{
do
:: atomic{
shutter_req == SHUTTER_UP_REQ ->
shutter_state = SHUTTER_UPPED;
printf("shutter upped\n");
}
:: atomic{
shutter_req == SHUTTER_DOWN_REQ ->
shutter_state = SHUTTER_DOWNED;
printf("shutter downed\n");
}
:: atomic{
(es_req == ES_ON_REQ) && (shutter_state == SHUTTER_DOWNED) &&
(door_front_state == DOOR_CLOSED) && (door_lock_front_state == DOOR_LOCKED) &&
(door_back_state == DOOR_CLOSED) && (door_lock_back_state == DOOR_LOCKED) ->
es_state = ES_ON;
printf("electronic shock ON!!!!!!!!!!!!!!\n");
}
:: atomic{
es_req == ES_OFF_REQ ->
es_state = ES_OFF;
printf("electronic shock OFF\n");
}
:: else;
od;
}
また、安全と省エネルギーに関する以下の条件もLTLで記述します。
w1は、”いずれのドアが解錠され、且つシャッターに通電されている状態は、常にあってはならない”
w2は、”シャッターが上がっていて、且つシャッターに通電されている状態は、常にあってはならない”
という意味です。
# define C_ES_ON (es_state == ES_ON)
# define C_ANY_UNLOCKED ((door_lock_front_state == DOOR_UNLOCKED) ||\
(door_lock_back_state == DOOR_UNLOCKED))
# define C_SHUTTER_UPPED (shutter_state == SHUTTER_UPPED)
// For inner person safety.
ltl w1{always !((C_ES_ON) && (C_ANY_UNLOCKED))}
// For energy saving.
ltl w2{always !((C_ES_ON) && (C_SHUTTER_UPPED))}
まとめたコードはgithubにshutter.pmlとしてあげています。
上記を試しに以下コマンドでシミュレーション実行します。シミュレーション実行はシステム全体の振る舞いをランダムに決定して遷移させていくモードです。
spin -u1000 shutter.pml
以下のような出力となります。シャッターを何度も下げたり、ドアを解錠したりをしています。(2回おなじ操作が来た場合はエラーとしていないので大丈夫です。)ここでは軽く動いているか確認する程度で見てください。また、文法に間違いが在る場合はこの時点でわかります。
...
shutter downed
shutter downed
shutter downed
shutter downed
select door action
door front opened
select action
down reqs
shutter downed
select door action
door back closed
select action
down reqs
back door unlocked
es_state: ES_OFF
...
次に、網羅的に全体の振る舞いを見てみます。
LTL記述したw1について検証します。
spin -a shutter.pml
gcc pan.c
./a.out -m100000 -N w1
spin -t -c shutter.pml
以下の出力が得られました。
シャッター通電状態で表口ドアロックが解錠される状態が検出されたためにエラーとなっています。
electronic shock ON!!!!!!!!!!!!!!
door_lock_front_state: DOOR_LOCKED
door_lock_back_state: DOOR_LOCKED
select door action
select action
down reqs
front door unlocked
es_state: ES_ON
spin: _spin_nvr.tmp:3, Error: assertion violated
spin: text of failed assertion: assert(!(!(!(((es_state==ES_ON)&&((door_lock_front_state==DOOR_UNLOCKED)||(door_lock_back_state==DOOR_UNLOCKED)))))))
次に、LTL記述したw2について検証します。
./a.out -m100000 -N w2
spin -t -c shutter.pml
以下の結果となりました。
シャッター通電状態でシャッターが上がった状態が検出されたためにエラーとなっています。
...
down reqs
electronic shock ON!!!!!!!!!!!!!!
...
shutter upped
spin: _spin_nvr.tmp:12, Error: assertion violated
spin: text of failed assertion: assert(!(!(!(((es_state==ES_ON)&&(shutter_state==SHUTTER_UPPED))))))
各社への要求の修正
SPINの出力結果から、w1,w2を満たしていないことがわかりました。
これに基づき要求を修正しましょう。
修正前：
B社：Door Controller
※ドア閉はドアが閉じている状態のこと。
REQ_B_01 : IF 表口ドア閉 THEN IF 表口ドアロック解錠要求 THEN 表口ドアロック解錠
REQ_B_02 : IF 表口ドア閉 THEN IF 表口ドアロック施錠要求 THEN 表口ドアロック施錠
REQ_B_03 : IF 裏口ドア閉 THEN IF 裏口ドアロック解錠要求 THEN 裏口ドアロック解錠
REQ_B_04 : IF 裏口ドア閉 THEN IF 裏口ドアロック施錠要求 THEN 裏口ドアロック施錠
C社： Shutter Controller
REQ_C_01 : IF シャッター上げ要求 THEN シャッター上げ
REQ_C_02 : IF シャッター下げ要求 THEN シャッター下げ
REQ_C_03 : IF シャッター通電ON要求 AND シャッター下げ状態 AND 裏口表口すべてドア閉かつロック施錠
THEN シャッター通電ON
REQ_C_04 : IF シャッター通電OFF要求 THEN シャッター通電OFF
修正後：
B社：Door Controller
※ドア閉はドアが閉じている状態のこと。
REQ_B_01 : IF 表口ドア閉 THEN
IF 表口ドアロック解錠要求 AND シャッター通電OFF // Added!
THEN 表口ドアロック解錠
REQ_B_02 : IF 表口ドア閉 THEN IF 表口ドアロック施錠要求 THEN 表口ドアロック施錠
REQ_B_03 : IF 裏口ドア閉 THEN
IF 裏口ドアロック解錠要求 AND シャッター通電OFF // Added!
THEN 裏口ドアロック解錠
REQ_B_04 : IF 裏口ドア閉 THEN IF 裏口ドアロック施錠要求 THEN 裏口ドアロック施錠
C社： Shutter Controller
REQ_C_01 : IF シャッター上げ要求
THEN シャッター上げ, シャッター通電OFF // Added!
REQ_C_02 : IF シャッター下げ要求 THEN シャッター下げ
REQ_C_03 : IF シャッター通電ON要求 AND シャッター下げ状態 AND 裏口表口すべてドア閉かつロック施錠
THEN シャッター通電ON
REQ_C_04 : IF シャッター通電OFF要求 THEN シャッター通電OFF
Promelaにも変更を適用しましょう。変更はこのgithub変更履歴をご覧ください。
これで、w1,w2のエラーは消えたはずです。以下で確認してみましょう。
spin -a shutter.pml
gcc pan.c
./a.out -m100000 -N w1
./a.out -m100000 -N w2
w1, w2の実行ともに、以下のようにerrors:0と表示されます。
すなわち、修正により求めていた安全性、無駄な電力消費が解決出来たということです。
...
State-vector 52 byte, depth reached 787, errors: 0
...
これで、論理の保証付きで各社に分解後の要求を出せます。
注意点
今回はかなりモデルを省略して書いています。例えば、シャッターを上げる要求を受けたら直ぐにシャッターが上がった状態に成るようにモデルを記述しているため中間状態がありません。実務では中間状態にこそ論理の抜け漏れが多く潜んでいると考えられるため、"上がりきった状態" "下がる途中"など細かくモデルを組むべきと思います。また、通常のプログラミング言語同様、intなどの連続値も使えるので、0%~100%の昇降位置で表現しても容易かも知れません。
感想
通常のプログラミング言語と書き方は似ていますが、背景に在る考え方が異なるので少々苦労しました。また、解説サイトが少ないので、トラブルシュートも大変です。Google検索句を活用し"[word] site:spinroot.com"と検索すると良いです。
大規模な論理構造、構成要素数であり、初期の構築後に機能が追加されるようなシステムであれば、このツールの効果は絶大なものと成ると思いました。これまで思考実験を繰り返しながら論理を修正していったシステムに対し、機能を追加したいとなった場合、その思考をトレースする労力が必要ですし、設計担当者が変わった場合、はしばらく前担当者にレクチャーを受ける必要があります。そのような属人化を回避できるのは大きな利点です。
しかし言語として難解であるために、誤った論理表現をしてしまう可能性があります。実務に際してはケーススタディを繰り返して慎重に利用すべきと思います。
今後
組み込みの用途においては "ボタンON後10sec後に動作開始" などの時相表現がよく利用されますので、そのPromela上での表現方法を調査します。