モデル検査ツールの選定
モデル検査を行うにあたっては、まずツールを選定する必要があります。今回の場合、すでに存在しているコードが検査対象であり、また規模も大きくなかったため、コードとの対応関係が分かりやすく、通信処理がモデル化しやすいSpinが適切だと判断しました。Spinは公式Webサイトからダウンロードできます。
SpinではPromelaと呼ばれるC言語に似た独自言語で検査対象コードを記述します。例えばリスト1は、2人の顧客が預金（balance）から100円単位で入金と出金を繰り返している状況が記述されています。変数balanceは預金残高を示し、active [ 2 ]で2人分の預金口座を示すプロセスタイプが作られています。::と->は、「もし～ならば、～をする」記述です。
short balance = 100
active [ 2 ] proctype customer() {
START: do
// 預金残高（balance）が100円以上の時に100円取り出す
:: 100 <= balance -> balance = balance - 100;
// 預金残高（balance）が200円未満の時に100円入金する
:: balance < 200 -> balance = balance +100;
od
goto START;
}
このコードを検査対象とし、預金残高（balance）が常に0以上であることを確認するにはリスト2の検査式を記述します。ltlは線形時相論理（Linear-time Temporal Logic）式を意味し、[] は「常に後続の条件（0 <= balance）が成り立つ」という意味です。
// 預金残高（balance）は常に0以上
ltl spec { [] (0 <= balance) }
この状態でSpinによる検査を行うと、図3の赤枠「errors: 4」が示すように反例が4件あることが示されます。
反例の1つを表示させると、残高が100円以上であるかどうかの評価（100 <= balance）と出金（balance = balance - 100）がアトミックに行われていないため、預金残高（balance）が0未満になることがあると示されています（図4）。
このように、検査対象コードと検査式をPromelaで記述し、反例がないかどうかを検査することがSpinでの検査の流れとなります。反例がないということは、検索式が成り立たない場合がないと結論付けることができます。
同期処理に対する検査項目
まず検査を行うにあたり、同期処理の何を検査するかを決めます。監視制御システムに求められる要求項目から、今回は表1の検査項目を選びました。
| 検査項目1 | サーバー再起動後、サーバーの状態がブラウザの状態から再同期されて設定される。またはブラウザ再起動後、ブラウザの状態がサーバー状態から再同期されて設定される。 |
|---|---|
| 検査項目2 | 一時的通信切断後、状態が再同期される。 |
| 検査項目3 | 状態の同期・再同期にあたり、サーバーとブラウザのどちらにおいてもその値が過去の値に戻ることがない。 |
| 検査項目4 | 複数のブラウザがサーバー上の同じ状態を参照する場合に、サーバー／ブラウザの再起動、一時通信切断が発生しても正しく同期される。 |
ただし、Webアプリケーションであることやモバイル環境を考慮し表2の前提条件を追加しました。
| 前提条件1 | HTTP通信の制約により、通信切断発生時に、サーバーないしはブラウザのどちらか一方しか切断を検知しない場合がある。 |
|---|---|
| 前提条件2 | サーバー側のスレッド構造の制約により、受信したメッセージの処理順序が逆転することがある。 |
| 前提条件3 | モバイル通信で発生する可能性が高いものとして、通信メッセージの消失がある。 |
