SyncStitchを使ったAlternating bit protocol (ABP) の設計（2）〜仕様と実装の比較〜

形式手法 CSP

前回は通信路に歪みがないと仮定して、その上で 0, 1 をやり取りする送信者と受信者をモデル化してデッドロック検査を行いました。今回は仕様を状態遷移図で表し、その仕様との比較を試してみます。

さて、その仕様ですが、今回のABPの設計で確認したい事は「送信側から 0 を送信したら受信側に 0 が到達し、1 を送信したら 1 が到達する」です。この送信側の送信から受信側での到達の間、何回かのメッセージのやり取りがあるかもしれませんが、それは気にせずとにかく 0 を送ったら 0、1 を送ったら 1 となってほしいのです。

これを状態遷移図で表します。send.0, send.1 はそれぞれ送信側で 0, 1 の送信を開始するイベント、recv.0, recv.1 はそれぞれ受信側で待っていた 0, 1 を受信した通知のイベントです。


図1. 仕様の状態遷移図

上記仕様と比較するためにSenderとReceiverの定義を少し直します。今まではSenderは 0 および 1 の送信を（受信者の準備ができたら）自発的に行っていましたが、それぞれ開始のイベント send.0, send.1 で送信を始めるようにします。送信者の状態遷移図は以下のようになります。

図2. 送信者の状態遷移図

受信者は受信待ちになっているビットを受信したら通知のイベント recv.0, recv.1 を発行するようにします。これにより、受信者の状態遷移図は以下のようになります。

図2. 受信者の状態遷移図

最後にSYSプロセスの定義を以下のように修正します。

(define-process SYS
  (hpar (list sch rch) S0 R0))

前回は並行合成演算子 par を使いましたが、今回は隠蔽付き並行合成演算子hparを使用します。これによりSYSの外側からは rch, sch を使ったやり取りは見えません。逆に隠蔽されてない send.0 や recv.1 は観測可能です。よって、SYS プロセスで send.0 が観測できた後期待通り 0 が受信側に渡れば recv.0 が観測できるはずです。

ではSYSプロセスを検証しましょう。まずはデッドロック検査です。SYSを変更したのでもう一度デッドロック検査をしておきます。問題なく終了し、デッドロックがないことがわかります。次はいよいよ仕様とSYSの比較です。これにはトレース検証と拒否検証の二種類の検証があります。

トレース検証

詳しい定義はSyncStitchのユーザガイドを見てもらうとして一言で説明すると、トレース検証とは「仕様にない振る舞いをしないこと」を検証することです。仕様に書いていない良くない振る舞いをしない性質のことを安全性とも言うので、トレース検証とは安全性検査であるとも言えます。

SyncStitchでのトレース検証のやり方はAssertionsに (trace SPEC SYS) を追加してダブルクリックするだけです。検査すると緑色のチェックが表示され、トレース違反がないことが確認できます。

拒否検証

もうひとつの検証は、拒否検証です。トレース検証は仕様に書いていないことをしないことを検証する方法ですが、これだとSYSが何もしないとトレース違反がないことになります。実際にはこれは期待している事ではなく、仕様で定義する期待する振る舞いを実装がしてほしいものです。これを検査するのが拒否検証です。やはり正確な定義はユーザガイドを見てもらうとして、一言で説明すると拒否検証とは仕様が規定する振る舞いを実装が拒否しない、つまり、実装も同じように振る舞う事ができることを検証する事です。トレース検証の安全性と対比して、応答性の検査だと言われることがあります。

SyncStitchでの拒否検証のやり方はトレース検証と同様、Assertionsに (failure SPEC SYS) を追加してダブルクリックするだけです。検査すると緑色のチェックが表示され、拒否違反がないことが確認できます。

以上で、歪みがない通信路で 0, 1 を順番に送信する方法がわかりました（改めて検査するまでもないくらい簡単ですが）。
次回は、このモデルに歪みを入れていきます。

※ モデルは https://github.com/masateruk/blog/blob/master/20130816/abp-1.ss にあります。