Promelaで記述した検査モデル
前述の検査項目1～4、前提条件1～3を元に、同期処理コードから検査に最低限必要な部分をPromelaで記述し直しました（図5およびリスト3）。実際のアプリケーションの動作と同等なものをPromelaで記述しており、このコードが実装の検査モデルに相当します。
なお、リスト3に示したプログラムは一部です。全てのプログラムは、サンプルファイル「spec-1.pml」「spec-2-to-5.pml」「spec-7-and-8.pml」内にあります。これらのファイルには、検査対象プログラムに続き、表3の検査式を記述しています。なお、「spec-1.pml」については、公平性制約により検査式が長くなり、spinでの処理に問題が出たため、検査式をspinでの「発生してはいけない条件」の記述であるNever claimに置き換えたものを記載しています。検査式からNever claimへの変換には、LTL2BAを使用しています。
例えば、変数browser_a_stateは「ブラウザAの動作状態」を表しており、初期状態（browser_initial）や接続済み状態（browser_connected）などの値をとります。同様にbrowser_a_revisionは状態値のリビジョン番号、browser_a_arevisionはブラウザから見たサーバーが保持していると思われる状態値のリビジョン番号（認証済みリビジョン番号）となります。例えば、ブラウザの認証済みリビジョン番号が3の場合、同期相手であるサーバーがリビジョン番号3の値を持っていると、ブラウザが認識しているという意味になります。そのため、リビジョン番号と認証済みリビジョン番号が異なる場合は、同期がとれていないことになり、同じである場合は同期がとれていることになります。
コードが複雑になっていますが、大まかには「:: 条件式 -> 処理」、つまり条件が合致すれば処理を実行するといった記述がたくさん並んでいます。例えばリスト3中の「:: (browser_a_state == browser_connecting && msg_type == msg_connect_reply) -> browser_a_state = browser_connected;」は、ブラウザが接続試行状態（browser_connecting）の時に、接続要求応答（msg_connect_reply）を受信すると、接続済み状態（browser_connected）に遷移するといった動作を記述しています。この検査コード抽出においては、ブラウザやサーバーだけでなく、元々の同期処理コードには現れないネットワークも記述してあります。これは検査項目にある通信切断やメッセージロスを模擬するためです。また、検査項目4にある複数のブラウザが同一の状態を参照する場合も検査できるよう、ブラウザAとBが実装されています。リスト3はブラウザAの部分のみを示しました。ブラウザとサーバーはそれぞれ状態の値と状態のリビジョン番号、状態の認証済みリビジョン番号を持っています。
active proctype browser_a() {
mtype msg_type; // 受信したメッセージの種類
short revision; // 受信したリビジョン番号
short arevision; // 受信した認証済みリビジョン番号
short dcount = 1; // 残り通信切断可能回数
do
:: n2c_a_ch ? msg_type, revision, arevision ->
if
:: (browser_a_state == browser_connecting && msg_type == msg_connect_reply) ->
browser_a_state = browser_connected;
:: (browser_a_state == browser_vm_connecting &&
msg_type == msg_vm_connect_reply) ->
if
:: (browser_a_revision <= revision) ->
browser_a_revision = revision;
:: else -> skip;
fi;
if
:: (revision <= arevision) -> browser_a_arevision = arevision;
:: else -> browser_a_arevision = revision;
fi;
c2n_a_ch ! msg_vm_ack, 0, revision;
browser_a_state = browser_vm_connected;
:: (is_browser_connected(browser_a_state) &&
msg_type == msg_vm_ack && browser_a_arevision < arevision) ->
browser_a_arevision = arevision;
検査対象である同期処理をPromelaで書き直したので、このコードを元に先の検査項目1～4を具体的な検査式に落とし込みます。それらを表3に示しました。LTLで記述する検査式は、[]はすでに説明した通り「常に」ですが、<>は「いつかは真になる」という意味です。またWは2項演算子で、前後の条件式をa、bとした場合、a W bは「bが成り立つまでにはaが必ず成り立つ、もしくはaが常に成り立つ」という意味です。
| 検査式1 |
サーバーまたはブラウザのどちらかが再起動する場合でも、サーバーおよびブラウザの両方が接続済み状態に到達する。 [] <> (browser_a_state == browser_state_connected && server_a_state == server_state_connected) |
|---|---|
| 検査式2 |
サーバー再起動後、または一時的通信切断後、ブラウザのリビジョン番号と認証済みリビジョン番号が等しい状態に常に到達する。 [] <> (browser_a_revision == browser_a_arevision) |
| 検査式3 |
ブラウザ再起動後、または一時的通信切断後、サーバー側のリビジョン番号とブラウザ側のリビジョン番号が等しい状態に常に到達する。 [] <> (server_revision == browser_a_revision) |
| 検査式4 |
ブラウザの持つリビジョン番号が同期・再同期時に振動しない。 任意の整数xに対し[] ((browser_revision == x) -> ((x <= browser_revision) W (x <= browser_revision && browser_state == browser_disconnected))) |
| 検査式5 |
サーバーの持つリビジョン番号が同期・再同期時に過去の番号に戻らない。 任意の整数xに対し[] ((server_revision == x) -> ((x <= server_revision) W (x <= server_revision && (server_a_state == server_disconnected server_b_state == server_disconnected)))) |
| 検査式6 |
複数のブラウザが同一の状態を参照する場合、サーバーまたはブラウザのどちらかが再起動する場合でも、サーバーおよびブラウザの両方が接続済み状態に到達する。 [] <> (browser_a_state == browser_state_connected && server_a_state == server_state_connected && browser_b_state == browser_state_connected && server_b_state == server_state_connected) |
| 検査式7 |
複数のブラウザが同一の状態を参照する場合、サーバー再起動後、または一時的通信切断後、ブラウザ側リビジョン番号と認証済みリビジョン番号が等しい状態に常に到達する。 [] <> (browser_a_revision == browser_a_arevision && browser_b_revision == browser_b_arevision) |
| 検査式8 |
複数のブラウザが同一の状態を参照する場合、ブラウザ再起動後、または一時的通信切断後、サーバー側リビジョン番号と認証済みリビジョン番号が等しい状態に常に到達する。 [] <> (server_revision == server_a_arevision && server_revision == server_b_revision) |
ただし検査式2、3、7、8においては検査式1と6の成立が事前に示されており、サーバーおよびブラウザのどちらも接続済み状態（browser_a_state == browser_state_connected && server_a_state == server_state_connected）としています。また、メッセージロスや通信切断が発生し続けるような明らかな例外ケースを除外するため、再起動や通信切断、メッセージロスは全て最大1回までとしています。同様に、検査式1の検査では、サーバーとブラウザの通信路確立時にブラウザ側でタイムアウトが発生し続け、いつまでも通信路を確立できないケースも除外しています（リスト4）。こうした明らかな例外ケースを除外し、検査範囲を制限することを公平性制約と呼びます。
[] (
(s2cnetwork_a:msg_type == msg_connect_reply
-> <> browser_a_state == browser_connected) &&
(s2cnetwork_a:msg_type == msg_state_connect_reply
-> <> browser_a_state == browser_state_connected) &&
(c2snetwork_a:msg_type == msg_state_connect_reply
-> <> server_a_state == server_state_connected)
)
効率的に検査を進めるための簡略化
検査対象コードと検査式がそろったので検査を行えるようになりましたが、検査式6～8についてはブラウザ側が複数あるため検査に時間がかかります。しかし、ブラウザAとBは状態値や状態のリビジョン番号を通して間接的に影響を与えるだけであり、かつブラウザAとBは対称的なため、ブラウザBを簡易的に扱っても問題はありません。つまり、ブラウザBによる状態への操作のみを残したブラウザB模擬に置き換えても検査には問題がありません（図6）。
これにより検査式6～8は表4の通りに簡略化されます。
| 検査式6 | [] <> (browser_a_state == browser_state_connected && server_a_state == server_state_connected) |
|---|---|
| 検査式7 | [] <> (browser_a_revision == browser_a_arevision) |
| 検査式8 | [] <> (server_revision == server_a_arevision) |
また、ブラウザB模擬による影響は状態値とリビジョン番号の変更だけなので、検査式6にブラウザB模擬は影響を与えません。したがって検査式6の場合、ブラウザＢ模擬も削除可能で、結果検査式1と同じとなるため検査式6は検査を省略できます。
