モデル検査ツール > SPIN

「モデル検査ツール/SPIN」の編集履歴(バックアップ)一覧に戻る

モデル検査ツール/SPIN - (2011/01/26 (水) 16:18:09) のソース

*SPIN
----
**概要メモ
-分散・並列ソフトウェアを検証するために作られた検証器。
-1980年頃からベル研究所で開発された。
-Holzman氏が開発。
-Promela(Process Meta Language)という仕様記述言語を持つ。
-SPINはSimple Promela Interpreterの略。
----
**Promela
-チャネル通信オートマトンをベースにしている。
-オートマトンなので状態遷移系として記述する。
-チャネル通信の記述部分はCSP/Occamライクで、括弧の使い方とかセミコロンはC言語ライク?
----