プロトコルの形式的検証に関するお勉強メモ。
簡単な実例を用いて、検証ツールの使いかたに慣れるのを当面の目標とする。 Spin, Murphi のふたつのツールを用いて、同じ対象を扱う。
Spin はソフトウエア向け、Murphi はハードウエア向けみたいな説明を見かけることもあるが、 きっと、そんなはずはない。 ハード上で実行しようが、ソフト上で実行しようが、紙と鉛筆で計算しようが、 計算の本質は同じでしょ？
実例としては、
の二つから始める。
Spin, Murphi のいずれもチュートリアルの題材として、これらを紹介している。
>>次ページ：Dekker0 by Spin