SPINモデルチェッカ
SPIN(Simple Promela INterpreter)は、オートマトンに基づく模型検査器(model checker)。検査対象のシステムは専用の言語Promela (Process Meta Language) で記述される。Promela は、非同期分散アルゴリズムを非決定的オートマトンとしてモデル化する。検証される属性は線形時相論理の論理式で表される。この論理式の否定形をBüchiオートマトンに変換して Promela のモデルと合成し、モデル検査アルゴリズムの一部とする。モデル検査の他に、SPIN はシミュレータとしても操作可能であり、システムのとりうる実行経路の1つを実行し、そのトレース結果をユーザーに示す。
多くのモデルチェッカとは異なり、SPIN はモデル検査そのものを実施するわけではなく、その問題に固有のモデルチェッカのC言語ソースを生成する。このような若干古い技法を使うことでメモリ使用量を削減し、性能を向上させると共に、モデルにユーザーが自由にCのコードを追加できるという利点がある。SPIN では性能向上やメモリ使用量削減のために以下のような様々なオプションを用意している。
半順序法(partial order reduction)
状態データ圧縮
ビット状態ハッシング(状態情報全体を格納するのではなく、ハッシュコードをビットフィールドで記憶する。完全性は犠牲になるが、メモリを大幅に削減できる)
弱い公平性の施行(weak fairness enforcement)
GUI として XSpin,JSpin,iSpin が準備されている。