出版社内容情報
まずはモデル検査を体験しよう！
ソフトウェアの検証法で、今、最も注目されているのがモデル検査です。
「コンピュータの間違いをコンピュータで探す」というこの技術を、本書では付属のＣＤ-ＲＯＭを使って、誰でも簡単に体験することができます。
著者 産業技術総合研究所 システム検証研究センター
第1日
1. モデル検査とは
1.1 検査対象と状態遷移系
1.2 検査する性質
1.3 時相論理
1.4 モデル検査
1.5 まとめ
2. 例題「システムα」 ?? モデル検査の基礎
2.1 システムαの概要
2.2 紙の上でのモデル検査
2.3 ツールによるモデル検査
2.4 モデル検査【Spin版】
2.5 モデル検査【NuSMV版】
2.6 まとめ
3. 例題「ランプ点灯？」
3.1 仕様書
3.2 モデルと検査【Spin版】
3.3 モデルと検査【NuSMV版】
3.4 まとめ
第2日
4. 例題「Mini Life Game」窓辺の花
4.1 モデル作り
4.2 モデル【Spin版】
4.3 モデル【NuSMV版】
4.4 検査項目
4.5 ツールで検査【Spin版】
4.6 ツールで検査【NuSMV版】
4.7 まとめ
5. 例題「ウサギちゃんとオオカミくん」
5.1 モデル化
5.2 コード【Spin版】
5.3 コード【NuSMV版】
5.4 検査項目
5.5 検査【Spin版】
5.6 検査【NuSMV版】
5.7 まとめ
6. 例題：並行システムと排他制御
6.1 モデル化
6.2 コード【Spin版】
6.3 検査【Spin版】
6.4 システム全体に求めるもの【Spin版】
6.5 コード【NuSMV版】
6.6 検査【NuSMV版】
6.7 システム全体に求めるもの【NuSMV版】
6.8 まとめ
第2日の練習問題
第2日の練習問題のコードと検査式
第3日
7. LTL式の概要
7.1 状態遷移系とパス
7.2 様相記号とLTL式
7.3 LTL式の真偽
7.4 まとめ
8. 例題「3進カウンタ」
8.1 コード【Spin版】
8.2 コード【NuSMV版】
8.3 検査
8.4 まとめ
9. 例題「階段ぴょんぴょん」
9.1 モデルとコード【Spin版】
9.2 モデルとコード【NuSMV版】
9.3 検査
9.4 類題「階段ぴょんぴょん」（その2）
9.5 まとめ
第4日
10. 例題「プログラム（C言語）の試験」実践練習
10.1 検査対象のプログラム
10.2 従来の検証法
10.3 モデル検査を用いた検査【Spin版】
10.4 モデル検査を用いた検査【NuSMV版】
10.5 プログラムに間違いがあった場合
10.6 まとめ
11. 演習「自動販売機」
11.1 仕様書
11.2 検査項目
11.3 解答例
11.4 検査結果と主な改善点
11.5 コードと検査式
Appendix
A. 仕様記述言語Promela
A.1 大局構造
A.2 コメント・区切り記号
A.3 文字
A.4 データ型・変数宣言
A.5 変数のスコープ
A.6 プロセス型定義
A.7 制御フロー
A.8 inline
B. NuSMVの仕様記述言語
B.1 大局構造
B.2 コメント
B.3 文字
B.4 変数宣言部
B.5 遷移記述部
B.6 シンボル定義部
B.7 右辺値
B.8 検査式記述部
C. 命題論理式の真偽
D. 付録CD-ROMについて
D.1 KNOPPIXについて
D.2 システム要件
D.3 起動方法
D.4 終了方法
D.5 使用についての注意
参考文献
索引
感想・レビュー
※以下の感想・レビューは、株式会社ブックウォーカーの提供する「読書メーター」によるものです。
kaizen@名古屋de朝活読書会
