モデル検査ツール/SPIN - ソフトウェア関連の個人的備忘録

SPIN

---

概要メモ

• 分散・並列ソフトウェアを検証するために作られた検証器。
• 1980年頃からベル研究所で開発された。
• Holzman氏が開発。
• Promela(Process Meta Language)という仕様記述言語を持つ。
• SPINはSimple Promela Interpreterの略。

---

Promela

• チャネル通信オートマトンをベースにしている。
• オートマトンなので状態遷移系として記述する。
• チャネル通信の記述部分はCSP/Occamライクで、括弧の使い方とかセミコロンはC言語ライク？

---