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

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

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

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

OCamlで書いてC言語に変換するプログラム、最低限入れたかった機能を実装して一応形になりました（ソースコードはこちら）。プライベートな時間をちまちま使って作ったので思ったより時間がかかってしまいました。最初にブログで紹介してから1年半もたちまし…

私は5年ほど前から、仕事に費やす時間を計測している。何に、何分費やしたか？をすべて記録している。その記録を見返せば何時何分には何をやっていたのかを知る事ができる。私がこのような計測をしているにはねらいがあって、それは、 計測データを蓄積する…

忙しいエンジニアにとって電車での通勤時間は貴重な勉強時間。しかし、何気にかばんから取り出したiPhoneでTwitterやらFacebookやらを眺めて気づけばもうすぐ会社に到着ってこと、たまにありません？こうなるのを防ぐのにいい方法がないかなーっと先日会社で…