uDiary

◆ [お勉強] Spin もしくは Murphi を用いた Formal Verification

Formal Verification Memo (UikiTeXi)

有名どころのツールを用いて、プロトコルの形式的検証を行うことにする。 とりあえず目を付けたのは、Spin と Murφ のふたつ。

かつて、「Spin はソフトウエア検証向けであって、ハード向けじゃないお」 と言われてヘコんでしまったような記憶があるのだが、

Spin targets efficient software verification, not hardware verification.

ううむ、よく読むと、「ソフトウエアの検証を効率良く行うことが出来ます」 としか言ってませんな。あはは。

ま、ともあれ、両方使ってみる作戦。

いまのところ、両者の能力に大差は無いんじゃないかと踏んでいるんですが、まだ不明。 モデリング言語の醸し出す雰囲気は全然違います。したがって、書き心地はだいぶ違う。

今日はとりあえず、「Dekker の初期の解といわれているらしい、 排他になっていない排他制御の穴を、ちゃんと見つけられますか」問題 *1をやってみた。

これは、Basic Spin Manual にある例そのままなので、 Promela でのモデリングについてはいわれるがまま。 同じものを Murphi 向けに書き直すのは、自分でやってみました。 ちゃんと出来たと思うんですが、これで良いのかどうかは、いまいち自信がない。

今後の予定ですが、どうせなので The Dekker's Algorithm の方もきちんと扱っておこう。 プロトコル検証とは直接関係ないけど、 SPARC V9 Manual にあるようなメモリバリアの話も一応述べておくかなぁ。

次は、Spin, Murphi ともに例題にあげている Alternative Bit Protocol (ABP) をやってみる予定。