情報
トップエスイー実践講座 第3巻
SPINによる設計モデル検証モデル検査の実践ソフトウェア検証
昨今、ソフトウェアの正しさを保証するソフトウェア検証の技術が重要視されているが、その中でも特にモデル検査が脚光を浴びている。それは数理論理学などに関する知識があまりない技術者にも、ソフトウェア開発の中で利用することが可能だからであろう。本書はSPINを中心にモデル検査をいかにしてソフトウェア開発のプロセスの中に位置づけるかについて実例を通して詳説している。
電子書籍¥3,960 小売希望価格(税込)
紙の書籍¥3,960定価(税込)
基本情報
発売日 | 2008年9月26日 |
---|---|
本体価格 | 3,600円 |
ページ数 | 256 ページ ※印刷物 |
サイズ | B5 変形 |
ISBN | 9784764903548 |
ジャンル | 情報 |
タグ | ソフトウェア工学 |
電子書籍形式 | 固定型 |
主要目次
第 1 章 設計モデル検証とモデル検査
1.1 分散システムを開発する際の課題
1.2 ソフトウェア検証とは?
第 2 章 モデル検査概論
2.1 振る舞いの特性
2.2 モデル検査の仕組み
2.3 演習問題
第 3 章 モデル検査ツール SPIN 概要
3.1 PROMELA/SPIN 概要
3.2 PROMELA 入門
第 4 章 SPIN によるモデル検査
4.1 モデル検査
4.2 XSPIN
4.3 演習問題
第 5 章 SPIN による設計モデルの検証プロセス
5.1 検証プロセス概論
5.2 検証プロセスの詳細
第 6 章 設計モデルの検証の実際
6.1 例題:HD/DVD レコーダのネットワーク連携
6.2 検証要求の分析例
6.3 検証対象モデルの設計例
6.4 検証対象モデル(VM)の実装例
6.5 検証と設計へのフィードバッグ例
6.6 演習問題
第 7 章 検証の実践:抽象化・効率化・デバッグ
7.1 パターンを使った性質の記述
7.2 抽象化・スライシング
7.3 検証効率化
7.4 バグの発見・原因追究・修正
参考文献 187
付録 A PROMELA/SPIN リファレンスマニュアル
付録 B 設計モデルの検証プロセス
付録 C 簡易ステートマシン図のシンタックスとセマンティクス
付録 D 簡易ステートマシン図と PROMELA の対応
索 引
1.1 分散システムを開発する際の課題
1.2 ソフトウェア検証とは?
第 2 章 モデル検査概論
2.1 振る舞いの特性
2.2 モデル検査の仕組み
2.3 演習問題
第 3 章 モデル検査ツール SPIN 概要
3.1 PROMELA/SPIN 概要
3.2 PROMELA 入門
第 4 章 SPIN によるモデル検査
4.1 モデル検査
4.2 XSPIN
4.3 演習問題
第 5 章 SPIN による設計モデルの検証プロセス
5.1 検証プロセス概論
5.2 検証プロセスの詳細
第 6 章 設計モデルの検証の実際
6.1 例題:HD/DVD レコーダのネットワーク連携
6.2 検証要求の分析例
6.3 検証対象モデルの設計例
6.4 検証対象モデル(VM)の実装例
6.5 検証と設計へのフィードバッグ例
6.6 演習問題
第 7 章 検証の実践:抽象化・効率化・デバッグ
7.1 パターンを使った性質の記述
7.2 抽象化・スライシング
7.3 検証効率化
7.4 バグの発見・原因追究・修正
参考文献 187
付録 A PROMELA/SPIN リファレンスマニュアル
付録 B 設計モデルの検証プロセス
付録 C 簡易ステートマシン図のシンタックスとセマンティクス
付録 D 簡易ステートマシン図と PROMELA の対応
索 引