 |
 |
| 第1日 |
 |
|
|
 |
モデル検査とは |
|
| |
| 1.1 | 検査対象と状態遷移系 |
| 1.2 | 検査する性質 |
| 1.3 | 時相論理 |
|
|
|
| |
 |
例題「システムα」 モデル検査の基礎 |
|
| |
| 2.1 | システムαの概要 |
| 2.2 | 紙の上でのモデル検査 |
| 2.3 | ツールによるモデル検査 |
|
|
| 2.4 | モデル検査【Spin版】 |
| 2.5 | モデル検査【NuSMV版】 |
| 2.6 | まとめ |
|
| |
 |
例題「ランプ点灯」 |
|
| |
|
|
|
|
| |
| 第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式の概要 |
|
| |
|
|
|
|
| |
 |
例題「3進カウンタ」 |
|
| |
| 8.1 | コード【Spin版】 |
| 8.2 | コード【NuSMV版】 |
|
|
|
| |
 |
例題「階段ぴょんぴょん」 |
|
| |
| 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.4 | 検査結果と主な改善点 |
| 11.5 | コードと検査式 |
|
| |
| Appendix |
|
|
|
 |
仕様記述言語Promela |
|
| |
| A.1 | 大局構造 |
| A.2 | コメント・区切り記号 |
| A.3 | 文字 |
| A.4 | データ型・変数宣言 |
|
|
| A.5 | 変数のスコープ |
| A.6 | プロセス型定義 |
| A.7 | 制御フロー |
| A.8 | inline |
|
| |
 |
NuSMVの仕様記述言語 |
|
| |
| B.1 | 大局構造 |
| B.2 | コメント |
| B.3 | 文字 |
| B.4 | 変数宣言部 |
|
|
| B.5 | 遷移記述部 |
| B.6 | シンボル定義部 |
| B.7 | 右辺値 |
| B.8 | 検査式記述部 |
|
| |
 |
命題論理式の真偽 |
|
| |
 |
付録CD-ROMについて |
|
| |
| D.1 | KNOPPIXについて |
| D.2 | システム要件 |
| D.3 | 起動方法 |
|
|
|
| |
参考文献
索引 |
| |
