SyncStitchを使ったAlternating bit protocol (ABP) の設計（1）〜シンプルなモデルの作成とデッドロック検査〜

形式手法 CSP

以前いっしょに仕事していた先輩がSyncStitchという設計ツールを開発したので試用してみました。

SyncStitchの特徴は、状態遷移図で書いたモデルの振る舞いをシミュレーションしたり検証できたりします。さらに複数の状態遷移図を組み合わせときの振る舞いについても同様にシミュレーションと検証ができます。これによりマルチコアやマルチスレッドで動作するソフトウェアの再現性の低いバグを設計時につぶすことが期待できます。詳細はこちらの紹介文かこちらからダウンロードできるユーザガイドを見てください。

今回はこのSyncStitchを使ってAlternating bit protocol (ABP) の設計をしてみました。ABPは歪みのある通信路で 0 と 1 を交互に送信するためのプロトコルです。

最初は簡単なモデルから

こういった設計の基本はいきなり全部入りの複雑なものから始めるのではなく、単純なモデルから始める事です。そこで、最初は歪みのないモデルからスタートします。

まずどうやってモデル化するかの大雑把な方針を決めます。SyncStitchは動作する主体をプロセス、プロセス間の通信にはイベントもしくはチャネル通信を使ってモデル化します。まず送信者と受信者をそれぞれプロセスとして定義すると決めます。これは良いでしょう。次に送信者と受信者の間の通信路ですが、最初は歪みがないことを仮定していますのでSyncStitchのチャネルをそのまま使用する事にします。あとで歪みを考慮に入れるときには、チャネルをそのまま使ってはうまくモデル化できませんが今の段階では確実に通信が行われると仮定しているのでチャネルをそのまま使うことにします。チャネルは通信路の方向ごとに用意します。送信者から受信者への通信路を rch チャネル、受信者から送信者への通信路を sch チャネルとします。

方針がきまったらそれぞれを定義していきます。

まずは送信者を状態遷移図で定義します。初期状態をS0として、0 を送ったらS1状態へ遷移します。rch は受信者プロセスへ送るためのチャネルです。通信路に歪みがなければ、受信者から送信者のチャネル sch に 0 が返ってくるはずです。S1状態はその 0 を待っている状態です。S1 状態で 0 を受け取ると受信者が 0 を受信したことが確認できたので 1 を送信するS2状態に遷移します。S2状態で 1 を送信するとS3状態に遷移し 1 を待ち、1 を受信すると最初のS0に戻って再び 0 の送信を行います。以上が送信者の振る舞いです。


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

受信者は、送信者を鏡移しにしたような振る舞いです。初期状態R0では 0 を待ちます。0 を受け取ったらR1へ。0 を返信したらR2へ遷移して 1 を待ちます。1 を受け取ったらR3へ遷移して 1 を返信して最初のR0に戻ります。

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

最後に送信者と受信者が協調して動くシステムプロセスを並行合成演算子parを使って定義します。"並行合成演算子"は並行に動作する複数のプロセスからなるプロセスを定義する演算子です。(list sch rch)は同期リストと呼ばれ、プロセス間で同期するイベントです。チャネルを同期リストに指定した場合はそのチャネルを介した通信イベントをすべて指定したことになります。

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

ここまでできたらシミュレーションをしてみます。プロセスリストからSYSを選択して右クリックして「explore」を選択。プロセス式の入力を求められたら、「SYS」と入れます。すると、プロセスの初期状態が表示され、左側に遷移リストが表示されます。遷移リストを選択すると、次の状態が表示されるので順番に遷移を選択する事で正しくモデル化できているか確認する事ができます。


図3. SYSのシミュレーション画面

ある程度シミュレーションをして正しそうだと確信したら、次は検証を行います。まずは一番簡単で手軽なデッドロックがないことを検査します。チャネル通信は同期通信ですので、もし送信とペアになる受信の遷移がなければプロセスは止まってしまいます。今回は受信者、送信者ともに一本道の遷移ですので遷移のガード条件や送信パラメータに誤りがなければデッドロックはないはずです。デッドロック検査はプロセスリストのAssertionsボタンを押して表示されるAssertionsウィンドウで(deadlock SYS)と入力してダブルクリックすることで検査できます。実行するとすぐに緑色のチェックが出てデッドロックがないことが分かりました。これでモデル化に単純なミスがないことが確認できました。

以上が最初のモデルの作成とデッドロック検査のやり方です。今回紹介したデッドロック検査は強力ですが、デッドロックがないことだけでは検証が十分とは言えません。そこで、次回はSYSプロセスと仕様を比較することで、SYSが仕様を満たしているかどうか検証する方法を紹介します。

今回のモデルは https://github.com/masateruk/blog/blob/master/20130813/abp-0.ss にアップしてあります。