第1日

 モデル検査とは
 
1.1検査対象と状態遷移系
1.2検査する性質
1.3時相論理
 
1.4モデル検査
1.5まとめ
 

 例題「システムα」 モデル検査の基礎
 
2.1システムαの概要
2.2紙の上でのモデル検査
2.3ツールによるモデル検査
 
2.4モデル検査【Spin版】
2.5モデル検査【NuSMV版】
2.6まとめ
 

 例題「ランプ点灯」
 
3.1仕様書
3.2モデルと検査【Spin版】
 
3.3モデルと検査【NuSMV版】
3.4まとめ
 
第2日

 例題「Mini Life Game」窓辺の花
 
4.1モデル作り
4.2モデル【Spin版】
4.3モデル【NuSMV版】
4.4検査項目
 
4.5ツールで検査【Spin版】
4.6ツールで検査【NuSMV版】
4.7まとめ
 

 例題「ウサギちゃんとオオカミくん」
 
5.1モデル化
5.2コード【Spin版】
5.3コード【NuSMV版】
5.4検査項目
 
5.5検査【Spin版】
5.6検査【NuSMV版】
5.7まとめ
 

 例題:並行システムと排他制御
 
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日

 LTL式の概要
 
7.1状態遷移系とパス
7.2様相記号とLTL式
 
7.3LTL式の真偽
7.4まとめ
 

 例題「3進カウンタ」
 
8.1コード【Spin版】
8.2コード【NuSMV版】
 
8.3検査
8.4まとめ
 

 例題「階段ぴょんぴょん」
 
9.1モデルとコード【Spin版】
9.2モデルとコード【NuSMV版】
9.3検査
 
9.4類題「階段ぴょんぴょん」(その2)
9.5まとめ
 
第4日

 例題「プログラム(C言語)の試験」実践練習
 
10.1検査対象のプログラム
10.2従来の検証法
10.3モデル検査を用いた検査【Spin版】
 
10.4モデル検査を用いた検査【NuSMV版】
10.5プログラムに間違いがあった場合
10.6まとめ
 

 演習「自動販売機」
 
11.1仕様書
11.2検査項目
11.3解答例
 
11.4検査結果と主な改善点
11.5コードと検査式
 
Appendix

 仕様記述言語Promela
 
A.1大局構造
A.2コメント・区切り記号
A.3文字
A.4データ型・変数宣言
 
A.5変数のスコープ
A.6プロセス型定義
A.7制御フロー
A.8inline
 

 NuSMVの仕様記述言語
 
B.1大局構造
B.2コメント
B.3文字
B.4変数宣言部
 
B.5遷移記述部
B.6シンボル定義部
B.7右辺値
B.8検査式記述部
 

 命題論理式の真偽
 

 付録CD-ROMについて
 
D.1KNOPPIXについて
D.2システム要件
D.3起動方法
 
D.4終了方法
D.5使用についての注意
 
参考文献
索引
 
Copyright (C) 2006 NTS Inc. All right reserved.