「モデル検査ツール/SPIN」の編集履歴（バックアップ）一覧はこちら

モデル検査ツール/SPIN - (2011/01/26 (水) 15:47:10) の最新版との変更点

追加された行は緑色になります。

削除された行は赤色になります。

*SPIN
----
**概要メモ
-分散・並列ソフトウェアを検証するために作られた検証器。
-1980年頃からベル研究所で開発された。
-Holzman氏が開発。
-Promela(Process Meta Language)という仕様記述言語を持つ。
-SPINはSimple Promela Interpreterの略。
----
**Promela
-チャネル通信オートマトンをベースにしている。
-オートマトンなので状態遷移系として記述する。
-チャネル通信の記述部分はCSP/Occamライクで、括弧の使い方とかセミコロンはC言語ライク？
----
**バージョンに関するメモ
-SPIN v6.0.0
--2010年12月にv6になる
--Never Claimを一つのファイルに複数書くことができるようになったらしい
---実行時に「./a -N <ncname>」で指定
---検証は一つずつ
--GraphvizのDotがサポートされた
---実行時に「./a -D」でDot言語に変換した形で出してくれる
---これはつまり、図形化できるということだと思う
---実際にやった。素晴らしい。

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