ＳＰＩＮ　モデル検査: 検証モデリング技法

著者 : 中島震

• 近代科学社 (2008年4月30日発売)

作品紹介・あらすじ

リソースには限界がある。技術者にとって大切なことは制約の中で目的とする記述を得る方法の習得である。本書はまさにこのようなモデリング技法について述べている。

感想・レビュー・書評

[akiyama924さんの感想 · 2012年4月30日]

初心者向けSPINの実用書です。

SPINとは、"Simple Promela Interpreter"の略で、"Promela"は、Gerard J. Holzmannが作った並列処理を伴う状態遷移（オートマトン）を記述できる形式仕様記述言語のことです。
この本は、実例（Promelaプログラムサンプル）を通してソフトウェアの振る舞いの形式記述法を学び、SPINでそれを動かしてデッドロックや、プロセスのプライオリティ逆転等々のモデルチェッキングの方法を学ぶことができます。

SPIN自体は、プログラマが振る舞いの検証を行うために使うツールと思いますので、いわゆる第三者検証を実施しているテスト設計を行う人が使うことはないと思いますが、SPINでどんなことが検証できるのかを知っておくことは悪くないと思います。

また、特に9章の「検査対象の大きさを適切に保つ……抽象化の方法」は普通のテスト設計にも非常に役に立つと思います。この章の始めに、抽象化が重要であることは容易にわかるが、抽象化によってシステムがもともと持っていた性質が消えてしまっては元も子もない。という文があるのですが、じゃあどういう観点で抽象化していくのと言う答えがこの章にあります。節名だけ書くと、
　9.2 データ値に着目した抽象化
　9.3 制御の流れに着目した抽象化
　9.4 連続時間の抽象化
です。

山本訓稔さんがリーディングされている「Model Checkingを適用した実践的非同期制御検証」は、要するにモデル設計フェーズで作成しているxUMLからPromelaを自動生成するツールを作ったってことです。
こうすることで、xUMLからC++へ変換されるC++の3万行のコードに対して、300万もの状態を自動検証したことと同等の効果を得ることができ、きわどい欠陥を検出できています。

つまり実用段階の技術となってきているのですね。

著者プロフィール

中島震（国立情報学研究所 教授）

「2019年 『デジタル・プラットフォーム 解体新書』 で使われていた紹介文から引用しています。」