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

前回までは通信路に歪みがないことを仮定してましたが、今回から通信路に歪みを考慮に入れます。つまり、送信した値と異なる値が相手に届くことがあると状況をつくります。 チャネルのモデリング これまではSyncStitchのチャネルをそのまま使用していました…

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

以前いっしょに仕事していた先輩がSyncStitchという設計ツールを開発したので試用してみました。SyncStitchの特徴は、状態遷移図で書いたモデルの振る舞いをシミュレーションしたり検証できたりします。さらに複数の状態遷移図を組み合わせときの振る舞いに…