SPINモデルチェッカとは？わかりやすく解説

SPINモデルチェッカ（英: SPIN model checker）は、ソフトウェアのモデル検査のためのツールである。Gerard J. Holzmann らが開発し、15年以上に渡って改良を続けてきた。2001年にAssociation for Computing Machinery (ACM) のソフトウェアシステム賞を受賞している。1995年以来、ほぼ毎年モデル検査に興味のある SPIN ユーザーや研究者による 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 が準備されている。

Promela

その名前(Process Meta Language)が示すように、元来通信プロトコルの検証のために設計された言語である。検査対象であるシステムは非同期並行動作するプロセスの集まりとして記述される。C言語に似た文法を持ち、各プロセスの振る舞いを手続き的に記述する。プロセス間通信、非決定的な振る舞いを明示的に記述する文法要素を備えている。

コード内にアサーションをおくことができる。線形時相論理で記述される検証項目はモデル全体に関する性質を記述するのに対して、アサーションはそれが置かれた場所で満たすべき条件を記述する。

参考文献

ジェラード・J.ホルツマン, 水野忠則 (訳) "コンピュータプロトコルの設計法―正しいプロトコルの設計と検証へ導く総合解説書 "カットシステム 1994/11 ISBN 978-4906391103

Holzmann, G. J., The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, 2004年. ISBN 0-321-22862-6.
中島震, SPINモデル検査―検証モデリング技法, 近代科学社, 2008年. ISBN 978-4764903531.
Basic Spin Manual – http://www.asahi-net.or.jp/~hs7m-kwgc/ spin/Man/Manual_japanese.html
産業技術総合研究所システム検証研究センター, 4日で学ぶモデル検査, エヌ・ティー・エス 2006/07 ISBN 978-4860431198

外部リンク

SPIN website

SPINモデルチェッカとは？わかりやすく解説