SPIN:モデル(安全性(排他)と応答性)
LTLに少し慣れた気がしたので、簡単なモデルを記述し練習してみることにしました。
モデルとしては、サーバでは標準で第1サービスが有効になっているが、運用者から第2サービスの開始操作があった場合に、サービスを切り替えるというものです。サービスは排他関係になっており、第1と第2サービスがともに有効になってはならないものとしています。検査の範囲としては、運用者が第2サービスを開始操作を行い、その後、停止操作を行うという流れを考えています。
モデル(model.pml)
/* OPE-SV間のメッセージ定義 */ mtype = { START_SND_SRV, /* 第2サービス開始 */ STOP_SND_SRV /* 第2サービス停止 */ } /* SVとの通信用チャネル */ chan svCh = [2] of { mtype } /* 運用者による操作を受付てSVに操作に対応するメッセージを送信するプロセス */ active proctype OPE() { bool sndSrvOrd = false; /* 運用者による第2サービス開始操作 */ atomic { sndSrvOrd = true; svCh ! START_SND_SRV; } /* 時間経過などもろもろ */ /* 運用者による第2サービス停止操作 */ atomic { sndSrvOrd = false; svCh ! STOP_SND_SRV; } } /* 実際のサービスを制御するサーバプロセス */ active proctype SV() { /* デフォルトでは第1サービスが有効になっているものとする。*/ /* 運用者から第2サービスの開始操作が行われた場合に、 第2サービスを開始する。*/ /* 第1サービスと第2サービスは排他関係になっており、両者が共に有効になってはならない。*/ bool isFstSrvOn = true; bool isSndSrvOn = false; mtype event; do :: svCh ? event -> if :: atomic { event == START_SND_SRV -> isFstSrvOn = false; isSndSrvOn = true; } :: atomic { event == STOP_SND_SRV -> isFstSrvOn = true; isSndSrvOn = false; } fi od }
検証式の追加
先頭にnが付いているものは、動作確認用にエラーを出力させるために用意しました。
安全性
/* 第1サービスと第2サービスが共に有効で無い状態が、常に成り立つ。*/ ltl safe { []!(SV:isFstSrvOn == true && SV:isSndSrvOn == true) } ltl nsafe { ![]!(SV:isFstSrvOn == true && SV:isSndSrvOn == true) } /* 第1サービスと第2サービスが共に無効な状態は、常に成立しない。*/ /* -> どちらかのサービスは有効である。*/ ltl notStop { []!(SV:isFstSrvOn == false && SV:isSndSrvOn == false) }
応答性(第2サービス開始)
/* 運用者による第2サービスの開始操作が行われたら、第1サービスが無効になり、第2サービスが有効になる。*/ ltl liveSndStart { [](OPE:sndSrvOrd == true -> <>(SV:isFstSrvOn == false && SV:isSndSrvOn == true)) } ltl nliveSndStart { ![](OPE:sndSrvOrd == true -> <>(SV:isFstSrvOn == false && SV:isSndSrvOn == true)) }
応答性2(第2サービス停止)
/* 運用者による第2サービスの停止操作が行われたら、第1サービスが有効になり、第2サービスが無効になる。*/ ltl liveSndStop { [](OPE:sndSrvOrd == false -> <>(SV:isFstSrvOn == true && SV:isSndSrvOn == false)) } ltl nliveSndStop { ![](OPE:sndSrvOrd == false -> <>(SV:isFstSrvOn == true && SV:isSndSrvOn == false)) }
試し
試しにSVがSTOP_SND_SRVイベントの処理を行う部分のatomicを取り除き以下の様にしてみます。
// :: atomic { event == STOP_SND_SRV -> isFstSrvOn = true; isSndSrvOn = false; } :: event == STOP_SND_SRV -> isFstSrvOn = true; isSndSrvOn = false;
すると、安全性の検査でisFstSrvOnとisSndSrvOnの両方がtrueになるケースがエラーとして検出されます。
検出例
$ spin -t -p -l model.pml pan: ltl formula safe pan:1: assertion violated !( !( !(((SV.isFstSrvOn==1)&&(SV.isSndSrvOn==1))))) (at depth 19) pan: wrote model.pml.trail (Spin Version 6.5.0 -- 17 July 2019) Warning: Search not completed + Partial Order Reduction Full statespace search for: never claim + (safe) assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid end states - (disabled by never claim) State-vector 44 byte, depth reached 19, errors: 1 8 states, stored 0 states, matched 8 transitions (= stored+matched) 5 atomic steps hash conflicts: 0 (resolved) Stats on memory usage (in Megabytes): 0.001 equivalent memory usage for states (stored*(State-vector + overhead)) 0.278 actual memory usage for states 128.000 memory used for hash table (-w24) 0.534 memory used for DFS stack (-m10000) 128.730 total actual memory usage pan: elapsed time 0 seconds
$ spin -t -p -l model.pml ltl safe: [] (! (((SV:isFstSrvOn==1)) && ((SV:isSndSrvOn==1)))) ltl nsafe: ! ([] (! (((SV:isFstSrvOn==1)) && ((SV:isSndSrvOn==1))))) ltl notStop: [] (! (((SV:isFstSrvOn==0)) && ((SV:isSndSrvOn==0)))) ltl liveSndStart: [] ((! ((OPE:sndSrvOrd==1))) || (<> (((SV:isFstSrvOn==0)) && ((SV:isSndSrvOn==1))))) ltl nliveSndStart: ! ([] ((! ((OPE:sndSrvOrd==1))) || (<> (((SV:isFstSrvOn==0)) && ((SV:isSndSrvOn==1)))))) ltl liveSndStop: [] ((! ((OPE:sndSrvOrd==0))) || (<> (((SV:isFstSrvOn==1)) && ((SV:isSndSrvOn==0))))) ltl nliveSndStop: ! ([] ((! ((OPE:sndSrvOrd==0))) || (<> (((SV:isFstSrvOn==1)) && ((SV:isSndSrvOn==0)))))) starting claim 2 Never claim moves to line 4 [(1)] 2: proc 0 (OPE:1) model.pml:16 (state 1) [sndSrvOrd = 1] OPE(0):sndSrvOrd = 1 3: proc 0 (OPE:1) model.pml:16 (state 2) [svCh!START_SND_SRV] 5: proc 1 (SV:1) model.pml:35 (state 1) [svCh?event] SV(1):event = START_SND_SRV 7: proc 1 (SV:1) model.pml:37 (state 2) [((event==START_SND_SRV))] 8: proc 1 (SV:1) model.pml:37 (state 3) [isFstSrvOn = 0] SV(1):isFstSrvOn = 0 9: proc 1 (SV:1) model.pml:37 (state 4) [isSndSrvOn = 1] SV(1):isSndSrvOn = 1 11: proc 0 (OPE:1) model.pml:21 (state 4) [sndSrvOrd = 0] OPE(0):sndSrvOrd = 0 12: proc 0 (OPE:1) model.pml:21 (state 5) [svCh!STOP_SND_SRV] 14: proc 1 (SV:1) model.pml:35 (state 1) [svCh?event] SV(1):event = STOP_SND_SRV 16: proc 1 (SV:1) model.pml:39 (state 6) [((event==STOP_SND_SRV))] 18: proc 1 (SV:1) model.pml:39 (state 7) [isFstSrvOn = 1] SV(1):isFstSrvOn = 1 Never claim moves to line 3 [(!(!(((SV.isFstSrvOn==1)&&(SV.isSndSrvOn==1)))))] spin: _spin_nvr.tmp:3, Error: assertion violated spin: text of failed assertion: assert(!(!(!(((SV.isFstSrvOn==1)&&(SV.isSndSrvOn==1)))))) spin: trail ends after 20 steps #processes: 2 queue 1 (svCh): 20: proc 1 (SV:1) model.pml:39 (state 8) SV(1):event = STOP_SND_SRV SV(1):isSndSrvOn = 1 SV(1):isFstSrvOn = 1 20: proc 0 (OPE:1) model.pml:22 (state 7) <valid end state> OPE(0):sndSrvOrd = 0 20: proc - (safe:1) _spin_nvr.tmp:2 (state 6) 2 processes created