SyncStitchを使ったAlternating bit protocol (ABP) の設計（3）〜歪みに対応する〜

形式手法 CSP

前回までは通信路に歪みがないことを仮定してましたが、今回から通信路に歪みを考慮に入れます。つまり、送信した値と異なる値が相手に届くことがあると状況をつくります。

チャネルのモデリング

これまではSyncStitchのチャネルをそのまま使用していましたが、歪みを入れられるように自分でモデル化します。最初は歪みのないチャネルをモデル化して、今までと同じ検証結果が得られるか確認します。

受信者用のチャネルは以下のように定義します。send_to_r.0 と send_to_r.1 はそれぞれ受信者への 0, 1 を送信を要求するイベントです。send_to_r.0 の後、受信者が実際に受信するチャネル rch へ 0 または 1 を送信します。現時点では歪みを入れないので、send_to_r.0 の後の RC1 状態からは rch!0 の遷移しかまだありません。


図1. 受信者用のチャネル

送信者用のチャネルも同様に定義します。

図2. 送信者用のチャネル

最後にSYSを以下のように修正します。まず、Sender（のS0状態）と受信者のチャネル（の状態RC0）を合成し、send_to_r.0, send_to_r.1 を隠蔽します。send_to_r.0, 1 を隠蔽するのはそれが Sender と 受信者のチャネルの間のみやり取りされるイベントだからです。それとReceiver（のR0状態）と送信者のチャネル（の状態SC0）を同様に合成したプロセスと合成し、チャネル通信イベントを隠蔽します。

(define-process SYS
  (hpar (list sch rch)
     (hpar (list send_to_r.0 send_to_r.1) S0 RC0)
     (hpar (list send_to_s.0 send_to_s.1) R0 SC0)))

ここまで出来たら前回と同様に検証します。検査式は前回のままです。検証するとすべて通る事が確認できます。3つとも問題なく通れば、チャネルのモデル化に問題ないと言えるでしょう。これは言わば、リファクタリングしてテストを通すのと同じですね。

ここまでのモデルは https://github.com/masateruk/blog/blob/master/20130831/abp-2.ss にあります。

歪みをモデル化

ここまで出来てようやく歪みをモデルに入れていきます。ここでは通信路による歪みはチェックサムなどの誤り検出技術により検出できると仮定して、値 e が送られるとします。状態遷移で表すには、歪みの結果 e を送信する場合とそのまま送れる場合の2つの遷移を非決定的に組み合わせます。状態遷移図は次の通りです。


図3. 歪みを含む受信者用のチャネル

いったん、二つのtau遷移で二つの状態に別れてからそれぞれの値を送信します。tau遷移は外から観測できない内部遷移であり、今のように複数のtau遷移を用いると非決定的な状態遷移を表す事が出来ます。送信者用のチャネルも同様の修正を施します。

チャネルに歪みの可能性を入れたら他を変えずに検査をしてみます。するとデッドロック検査で違反が見つかります。右クリックで「explore」を選ぶとどこで止まっているか確認できます。


図4. デッドロック状態

図を見ると歪みが起きて受信用チャネルが RC4 で本来 0 を送るべきところを歪みの結果、e を送信しようとしています。一方、受信者は R0 で 0 を待っているためデッドロックが起きています。このデッドロックを含むモデルは https://github.com/masateruk/blog/blob/master/20130831/abp-3.ss にあります。

では、直しましょう。受信者は期待している値と異なる値を受信した場合は、ひとつ前に受け取った値を送信者に返信するようにします。一方、送信者は自分が送った値が返ってくるのを待ちますが、期待していたものと異なる場合は先に送った値を再送信します。それぞれの状態遷移図は以下のようになります。


図5. 歪みに対応した受信者の状態遷移図


図6. 歪みに対応した送信者の状態遷移図

ではもう一度検証してみましょう。今度は無事通りました。

発散

無事検査が通ったので、めでたし、めでたし、これで終わり。と行きたいところですが、そうはいかないのです。

実はこのモデルには問題があるのです。それを確認するためにひとつ検査を追加してみます。

(divergence SYS)

検査すると通らないことがわかります。この検査は何をやっているかと言うと、発散がないかどうか検査しているのです。発散とは、循環したtau遷移のことです。つまり、発散があるとtau遷移だけを延々と繰り返すことがあるのです。tau遷移は内部遷移であり、外からは観測できないので外から見ると何だか動いているようだが何ら仕事をしてないように見えます。いわゆるライブロックと呼ばれるものです。デッドロックと同様「explore」メニューから問題の遷移を見ると、歪みが置き続けて再送信が延々と繰り返されている事が分かります。

SYSに発散があるだけでもまずいのですが、さらに悪いことに発散があると拒否検証の結果は意味をなさないのです。よって、発散を除いてから拒否検証を行わないといけないのです。

ということで次回はこの発散を除く方法を紹介したいと思います。

最後のモデルは、https://github.com/masateruk/blog/blob/master/20130831/abp-4.ss にあります。