SPINモデル検査：検証モデリング技法
中島 震
近代科学社従来その信頼性を確保するための手法であったテスト手法は、時間やコストなどの面で開発の現状に追いつけない状況にある。そのテスト手法に代わるものとして注目されてきているのが形式的手法による検証（モデル検査法）であり、その中の一つがSPINである。本書はSPINの基礎から実際の利用方法までを具体的に解説する日本で初めての書籍である。
【注意】本書のEPUB版は固定レイアウト型になっております。文字の大きさの変更や検索、引用などはお使いいただけません。画面の大きい端末でご利用ください。
書籍情報
著者: 中島 震
発行日: 2016-11-01
最終更新日: 2016-11-01
バージョン: 1.0.0
ページ数: 259ページ(PDF版換算)ページ
対応フォーマット: PDF, EPUB
出版社: 近代科学社
対象読者
自動検証, モデル検査法, Promela, 拡張有限状態オートマトン, Promela言語に興味のある方
著者について
1981年東京大学大学院理学系研究科修士課程修了。現在、国立情報学研究所教授・総合研究大学院大学教授 学術博士（東京大学）。
この間、科学技術振興機構さきがけ研究員（兼任）、北陸先端科学技術大学院大学客員教授を歴任。形式手法、自動検証、ソフトウェア・モデリングなどの研究に従事。
目次
第1章 モデル検査とは―自動検証とモデル検査法
- 1.1 振舞い仕様とモデル検査法
- 1.2 モデル検査法の発展
第2章 SPINを使ってみよう―Promelaの書き方とコマンドの使い方
- 2.1 簡単な並行実行プロセス
- 2.2 通信プロトコル
第3章 性質を表現する―正しさの基準
- 3.1 プリンタとスキャナ
- 3.2 時相論理を用いた性質表現
- 3.3 反駁のための記述
第4章 対象を広げる―Promelaの実行規則
- 4.1 拡張有限状態オートマトン
- 4.2 Promela言語の基本
第5章 仕組みを理解する―SPINの検証法
- 5.1 SPINのツール概要
- 5.2 オートマトンによる形式化
- 5.3 状態空間の探索法
- 5.4 時相論理との関係
第6章 ケーススタディ(1) ソフトウェアデザインを検証する―状態遷移ダイアグラムの解析
- 6.1 状態遷移システム
- 6.2 分散協調システム
- 6.3 バリエーション
第7章 ケーススタディ(2) モデル検査を使い分ける―Java並行プログラムの解析
- 7.1 デザイン検証とJavaプログラム
- 7.2 Javaの並行同期機構
- 7.3 入れ子モニターの不具合
第8章 ケーススタディ(3) 組込みソフトウェアの解析に使う―システムソフトウェアへの適用
- 8.1 割り込み処理と共有資源
- 8.2 リアルタイム・スケジューリング
第9章 ケーススタディ(4) 検査対象の大きさを適切に保つ―抽象化の方法
- 9.1 抽象化の重要性
- 9.2 データ値に着目した抽象化
- 9.3 制御の流れに着目した抽象化
- 9.4 連続時間の抽象化
第10章 ケーススタディ(5) デザイン検証の実際を知る―分散コンポーネントの振舞い検証
- 10.1 ドキュメントからのモデリング
- 10.2 システム記述と検査性質
- 10.3 まとめ