モデル検査ツール > SPIN


※上記の広告は60日以上更新のないWIKIに表示されています。更新することで広告が下部へ移動します。

SPIN


概要メモ

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


Promela

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