モデル検査[初級編] ―基礎から実践まで4日で学べる―
産業技術総合研究所システム検証研究センター
| 2009年11月24日発行 | |
| 定価 | 本体2,800円＋税 |
|---|---|
| A5判変形 | 並製 204頁 |
| ISBN | 978-4-7649-5505-9 |
| 発行 | ナノオプト・メディア |
| 発売 | 近代科学社 |
内容
本書は，独立行政法人産業技術総合研究所（産総研）システム検証研究センター主催「システム開発者のためのモデル検査研修コース（初級編）」のテキストを基に加筆修正後，単行本化した，モデル検査を体験＆理解してもらうためのテキストです。
モデル検査とは、システムが取り得る状態を計算機の力を使ってしらみつぶしに調べて、バグを発見する、あるいはソフトウェアの正しさを保証する手法のことである。
ソフトウェア開発者は、仕様書・試験要領書の整備，試験用機器・開発ツールの導入、上級技術者によるソースコードチェックなどで、開発中に発生する不具合・バグを除去し、ソフトウェアの品質を向上させるために努力をしています。しかし、これらの方法は担当する技術者の知識と経験に頼ったものであり、どれだけ綿密に行っても技術者が想定した状況には必ず「モレ」が生じます。微妙なタイミングで発生する不具合やいくつもの条件が重なって発生するエラーをすべて発見することは容易ではなく、障害の原因となる、開発者の意図しないシステムの振る舞いは、システム稼働後に初めて発見されるのが常です。
このような新システム稼働の際に常につきまとう問題を防ぐのに有効な方法が、モデル検査です。モデル検査は知識と経験によらず機械的かつ網羅的にシステムの検査を行える技術です。
モデル検査とは、システムが取り得る状態を計算機の力を使ってしらみつぶしに調べて、バグを発見する、あるいはソフトウェアの正しさを保証する手法のことである。
ソフトウェア開発者は、仕様書・試験要領書の整備，試験用機器・開発ツールの導入、上級技術者によるソースコードチェックなどで、開発中に発生する不具合・バグを除去し、ソフトウェアの品質を向上させるために努力をしています。しかし、これらの方法は担当する技術者の知識と経験に頼ったものであり、どれだけ綿密に行っても技術者が想定した状況には必ず「モレ」が生じます。微妙なタイミングで発生する不具合やいくつもの条件が重なって発生するエラーをすべて発見することは容易ではなく、障害の原因となる、開発者の意図しないシステムの振る舞いは、システム稼働後に初めて発見されるのが常です。
このような新システム稼働の際に常につきまとう問題を防ぐのに有効な方法が、モデル検査です。モデル検査は知識と経験によらず機械的かつ網羅的にシステムの検査を行える技術です。
目次
第1日
1. モデル検査とは
2. 例題「システムα」―モデル検査の基礎
3. 例題「ランプ点灯？」
第2日
4. 例題「Mini Life Game」窓辺の花
5. 例題「ウサギちゃんとオオカミくん」
6. 例題「並行システムと排他制御」
第3日
7. LTL式の概要
8. 例題「3進カウンタ」
9. 例題「階段ぴょんぴょん」
第4日
10. 例題「プログラム（C言語）の試験」実践練習
11. 演習「自動販売機」
Appendix
A. 仕様記述言語Promela
B. NuSMVの仕様記述言語
C. 命題論理式の真偽
D. 演習環境について
1. モデル検査とは
2. 例題「システムα」―モデル検査の基礎
3. 例題「ランプ点灯？」
第2日
4. 例題「Mini Life Game」窓辺の花
5. 例題「ウサギちゃんとオオカミくん」
6. 例題「並行システムと排他制御」
第3日
7. LTL式の概要
8. 例題「3進カウンタ」
9. 例題「階段ぴょんぴょん」
第4日
10. 例題「プログラム（C言語）の試験」実践練習
11. 演習「自動販売機」
Appendix
A. 仕様記述言語Promela
B. NuSMVの仕様記述言語
C. 命題論理式の真偽
D. 演習環境について
