SPIN モデル検査：検証モデリング技法

中島震

※この商品はタブレットなど大きいディスプレイを備えた端末で読むことに適しています。また、文字だけを拡大することや、文字列のハイライト、検索、辞書の参照、引用などの機能が使用できません。

社会の様々なところにソフトウェアが組み込まれる中、従来その信頼性を確保するための手法であったテスト手法は、時間やコストなどの面で開発の現状に追いつけない状況にある。そのテスト手法に代わるものとして注目されてきているのが形式的手法による検証（モデル検査法）であり、その中の一つがSPINである。本書はSPINの基礎から実際の利用方法までを具体的に解説する日本で初めての書籍である。

• カテゴリ: ビジネス・実用
• ジャンル: IT・コンピュータ / 情報科学
• 出版社: 近代科学社
• ページ数: 258ページ
• 電子版発売日: 2018年04月21日
• コンテンツ形式: EPUB
• サイズ(目安): 58MB

[ブクログ · ★★★★☆]

初心者向け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万もの状態を自動検証したことと同等の効果を得ることができ、きわどい欠陥を検出できています。

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