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