SyncStitchを使ったAlternating bit protocol (ABP) の設計(4)〜発散をとりのぞく〜

さて、ようやく最終回です。前回は、仕様と実装を比較して、実装が仕様を満たすことを確認したものの、実は発散が含まれているという話でした。今回はこの発散を取り除いて改めて仕様との比較を行います。

まずもう一度発散を確認しましょう。発散検査を行い、バツになったら右クリックで「explore」を選んで発散となっているtau遷移の正体を確認します。


図1. 発散の遷移列

Pathを表示すると、受信者用チャネルはRC0→RC1→RC4、送信者用チャネルはSC0→SC2→SC6と歪みによるエラーが延々と繰り返されているのが分かります。しかし、実際の通信路でエラーが起きる確率は通常何パーセント以下になっていて、このようにエラーが延々と繰り返されることはありません。そこで、モデルに連続でエラーになる最大数を入れて、無限にエラーが繰り返されないようにします。

受信用チャネルを以下のように変更します。


図2. 修正後の受信者用チャネル

各状態に n という変数が加わったのが確認できます。この n が連続でエラーを起こせる最大数となります。n を初期状態で N (ここでは 3 としました)に初期化します。エラーを起こす遷移のガード条件を 0 < n とし、エラーを送ったときには n を 1 つ減らします。正常値を送る遷移にはガード条件は設けていないので常に遷移可能です。よって、n が正のときにはエラーと正常値のどちらが送られるかは非決定的になります。エラーが続き n が 0 になるとエラーを送る遷移のガード条件が偽になり、必ず正常値が送られます。正常値を送ったときには n を N に戻すのでまたエラーが発生させることができます。

送信者、受信者それぞれのチャネルを変更したら再び検査を行います。モデルを変更したので、再びデッドロック検査から行います。デッドロックがないことが確認できたら、次に発散検査です。ともに検査が通ることが確認できます。発散がないことを確認したら、仕様と比較します。これもトレース、拒否ともに検査が通ることが確認できます。

仕様を満たすプロトコルが設計できました。最後のモデルは、https://github.com/masateruk/blog/blob/master/20130911/abp-5.ss にあります。

まとめ

以上で、ABPの設計は終わりです。今回心がけたモデリングでのポイントをまとめます。

  • シンプルなモデルから始める
  • 振る舞いを追加したり変更したりするときは、その都度検査をしながら少しずつ変更する
  • 拒否検証は発散を取り除いてから行う

参考文献

最後に参考文献を紹介してこの記事を終わります。

[1] 株式会社 PRINCIPIA『SyncStitch ユーザガイド
今回使ったSyncStitchというツールのドキュメント。ツールの説明というより基礎となっているCSPの解説がメインになっています。CSPの概念について非常に易しく解説してあります。日本語で読めるCSPの解説書では最も易しいものだと思います。

[2] Roscoe, A. W.『The Theory and Practice of Concurrency
CSPの解説書。[1] を読んでより形式的な解説が欲しい方にはこちらがおすすめ。操作的意味論に加え表示的意味論の解説もあります。5.3節にはCSPを使ったABPのモデリングと検証について解説があります。

[3] Gerard J. Holzmann『コンピュータプロトコルの設計法
SPIN Model Checker の開発である、ホルツマンによるプロトコルの設計方法を解説した本です。書籍の中で使用する検証ツールはSPINですが、ツールの説明ではなくプロトコルの設計時の課題や技術について解説が豊富な良書。もちろんABPに関する解説もあります。

[4] 『Basic Spin Manual
拙訳ながら SPIN Model Checker のマニュアルも載せておきます。「付録:検証スイートの構築」にABPのモデリングと検証についての記述があります。