Loading article…
SPINは、並行ソフトウェアモデルの正当性を厳密かつほぼ自動化された方法で検証するための汎用ツールです。1980年にベル研究所の計算機科学研究センターのUnixグループに所属していたジェラード・J・ホルツマンらによって開発されました。1991年以降は無償で公開されており、この分野の新たな発展に合わせて進化を続けています。
検証対象システムは、非同期分散アルゴリズムを非決定性オートマトンとしてモデル化できるPromela （プロセスメタ言語）で記述されます（SPINは「Simple Promela Interpreter」の略）。検証対象の特性は線形時相論理（LTL）式で表現され、モデル検査アルゴリズムの一部として、これらの式は否定された後、Büchiオートマトンに変換されます。SPINはモデル検査に加えて、シミュレータとしても機能し、システム内の実行パスを一つ辿り、その結果得られた実行トレースをユーザーに提示します。
多くのモデルチェッカーとは異なり、SPINはモデル検査自体を実行するのではなく、問題固有のモデルチェッカー用のCソースコードを生成します。この手法により、メモリを節約し、パフォーマンスを向上させるとともに、Cコードの断片をモデルに直接挿入することが可能になります。SPINは、モデル検査プロセスをさらに高速化し、メモリを節約するための多数のオプションも提供しています。例えば、以下のようなものがあります。
1995年以来、SPINユーザー、研究者、およびモデル検査に一般的に関心のある人々を対象としたSPINワークショップが（ほぼ）毎年開催されています。
2001年、Association for Computing MachineryはSPINにシステムソフトウェア賞を授与しました[ 1 ] [ 2 ]。