連続的な動作

本研究で提案した手法の中に仕様を検査するステップが存在する. その仕様をSPINを 用いて検査する際に，Promela文に何も処置を施さない場合にはエラーを出力すること

がある. これはユーザからの刺激を受けるオブジェクトが複数存在する場合に発生する.

ユーザからの刺激を受けるオブジェクトが複数ある場合，SPINは状態空間の網羅的な探 索を行なうため，ある仕様におけるサービスを完結する前に他のオブジェクトに割り込み が入って，仕様のサービスが起こらないサイクルを発見する.

例えば図4.2のように，ボタンとレバーのついたシステムがあったとしよう. ボタンイ ベントとレバーイベントはそれぞれべつのオブジェクトが管轄している.ここでシステム にはボタンを押すとサービス１が提供され，レバーを引くとサービス２が提供されるとい う仕様があったとする. Promela文に何も施さない場合は，ボタンが押されてからサービ ス1が提供されるまでの間に，レバーが引かれてサービス２を提供するという動作を繰り 返すという意図しないサイクルまで探索してエラーを出力する.

時間軸

PUSHBUTTON

SERVICE2

PULLLEVER

SERVICE2

SERVICE1

割り込み発生

PULLLEVER

サイクル

SPINが エラーを検出

図 4.2: 意図しないエラーの検出

そこでこの意図しないエラー出力を回避するために以下の制約を設けた.

• 仕様の動作が完結するまでは他のオブジェクトに割り込まれない.

この制約を適用するためにatomicシーケンスとイベント許可フラグを用いた. atomic シーケンスは実行の権利を他のオブジェクトに渡さずに連続的に実行を続けることの出 来る記述である. イベント許可フラグとは仕様の動作が完了した時に真となるフラグで，

ユーザからイベントを受けるオブジェクト全てに存在する. 全てのフラグが真である時に，

イベントの受理が可能となりユーザからのイベントを受け付ける. これは状態の活動部分 にサービスが付加している仕様を検査する時に有効に働く.

これらを用いることで仕様が完結するまで他のオブジェクトに割り込まれないモデルを 作ることができる. 以下にはその記述例を示した.

proctype objectA(){

: STATE:

if

::u_a?event ->

a_b!message;

:

::ok = false -> goto INSTATE;

fi;

INSTATE:

:

ok = true;

goto STATE;

}

proctype objectB(){

: STATE:

if

::atomic{a_b?message ->

statement;

: }

この例ではオブジェクトAが状態STATEにいる時，ユーザがeventを出すとobjectA がそのイベントを受け取り，objectBに向けてmessageを送る. objectBはメッセージを受

け取るとatomicシーケンスに入り，他のオブジェクトに実行を渡さずに命令文を実行す

る. またobjectAがイベントを受理せずに活動フェイズに入ったら，イベント許可フラグ

okをfalseにして活動に移る. 活動が終了したらokを真としてイベント受理フェイズに移

る. この方法を用いることで，ユーザからのイベントを受理したり活動を行なう際に，他 のオブジェクトに割り込まれずに実行を続けることが可能となる．okのフラグの使用例 は次の節で示す.