プログラミングなどなど

プログラミングに関係しそうな内容を

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