情報
SPIN モデル検査検証モデリング技法
SPINの基礎から実際の利用方法までを具体的に解説する日本で初めての書籍
◆SPINとは？
社会の様々なところにソフトウェアが組み込まれ、その規模が飛躍的に大きくなってきている中、従来その信頼性を確保するための手法であったテスト手法は、時間やコストなどの面で開発の現状に追いつけない状況が出てきている。
そのテスト手法に代わるものとして注目されてきているのが形式的手法による検証（モデル検査法）であり、その中の一つがSPINである。限られたテストケースでの誤りの無さを保障する従来のテスト手法に対して、数学的・論理的基盤に基づいて正しさを証明するモデル検査法は、無限に近い組合せに対しても正しさを保障できる手法であり、その中でもSPINは実際に産業界での適用事例も豊富で、その技術習得がソフトウェア技術者の必須要素として注目されてきている。
電子書籍¥3,800 小売希望価格（税別）
紙の書籍¥3,800定価（税別）
基本情報
| 発売日 | 2008年4月16日 |
|---|---|
| ページ数 | 256 ページ ※印刷物 |
| サイズ | B5 変形 |
| ISBN | 9784764903531 |
| ジャンル | 情報 |
| タグ | ソフトウェア・テスト |
| 電子書籍形式 | 固定型 |
主要目次
第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 まとめ
参考文献／Promelaクイック・レファレンス
コラム モデルのいろいろ／デッドロックの発生／LTLとCTL／無限長の受理列／SPINの工夫／NextオペレータとSPIN／MealyマシンとMooreマシン／UMLステートダイアグラム／スケジューリング・ポリシー／DbCとPDA／時間について