masateruk https://blog.hatena.ne.jp/masateruk/ masateruk’s blog https://masateruk.hatenablog.com/ 形式手法 CSP 前回は通信路に歪みがないと仮定して、その上で 0, 1 をやり取りする送信者と受信者をモデル化してデッドロック検査を行いました。今回は仕様を状態遷移図で表し、その仕様との比較を試してみます。さて、その仕様ですが、今回のABPの設計で確認したい事は「送信側から 0 を送信したら受信側に 0 が到達し、1 を送信したら 1 が到達する」です。この送信側の送信から受信側での到達の間、何回かのメッセージのやり取りがあるかもしれませんが、それは気にせずとにかく 0 を送ったら 0、1 を送ったら 1 となってほしいのです。これを状態遷移図で表します。send.0, send.1 はそれぞれ送信側で 0,… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fmasateruk.hatenablog.com%2Fentry%2F20130816%2F1376633172" title="SyncStitchを使ったAlternating bit protocol (ABP) の設計（2）〜仕様と実装の比較〜 - masateruk’s blog" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> https://cdn-ak.f.st-hatena.com/images/fotolife/m/masateruk/20130815/20130815222718.png Hatena Blog https://hatena.blog 2013-08-16 15:06:12 rich https://masateruk.hatenablog.com/entry/20130816/1376633172 1.0 100%