中島震「SPIN モデル検査」近代科学社

先日の CEDEC のセミナーで NII の石川先生が勧めていらっしゃった書籍をさっそく買ってみました。

タイトルどおり、SPIN というモデル検査ツールの本なのですが、SPIN のツールとしての使い方で終わっていないのがよいですね。簡単なモデル検査の概論から、SPIN が内部的に行っているモデル検査の仕組みに関する説明までしっかりと押さえており、LTL ベースのモデル検査の勉強をしたいという方にもオススメできる一冊です。

また、SPIN の記述言語の Promela の文法を学んだだけでは、なかなか使い物にならないのですが、本書ではケーススタディも豊富で、応用で使いたいときにどう書けばいいのかが分かりやすいのではないかと思います。現実の問題に適用する場合にしばしばぶつかる抽象化についてもきちんと章を割いています。

モデル検査は本当に日本語の情報が足りていませんでしたので、こういった良書がどんどん出てきてくれるといいですね。

ただ、LTL の SPIN 陣営が強いため、CTL のモデル検査に関する日本語情報はなかなか増えないのが辛いところです。「モデル検査のゲームシナリオへの適用」という記事をなんとか一通り書き上げましたので、これで少しでも CTL 陣営の勢いが増してくれればいいんですが。