形式仕様記述とモデル検査の基礎知識を一気に習得！！

優れた開発者として最先端の理論やツールと使ってソフトウェア開発をするために必要な基礎知識である、論理学、並行システム、オートマトン、モデル検査のアルゴリズムや実装技術、モデル検証ツールをこの1冊にまとめて解説

第1章　論理―正しいと考えられる事柄から正しい事柄を新たに導く
命題と述語
命題論理
述語論理

第2章　集合―多様な構造や構成の方法を知る
集合と元
包含関係
集合の演算
集合算の法則
集合族
関数，写像
集合の同等性
公理的集合論
列上の帰納法
バグ（bag）

第3章　並行プログラム―並行性に特有の概念と知識を学ぶ
並行プログラムとは？
並行プログラムの課題

第4章　時相論理―システムやプログラムの動的な性質を記述する
命題線形時相論理PLTL
分岐時相論理CTL

第5章　検証性質の記述―一般の技術者がシステムの性質を記述する
到達可能性
安全性
活性
公平性
性質記述パターン

第6章　オートマトン―コンピュータの動作を形式的に表現する
有限オートマトン
正規表現
B¨uchiオートマトン
時間オートマトン

第7章　モデル検査基礎―並行システムのモデル検査を行う
並行システムのモデル化
CTLモデル検査
TCTLモデル検査
PLTLモデル検査

第8章　モデル検査実装―検証モデル記述のノウハウを利用する
BDD（二分決定グラフ）による記号モデル検査
部分順序関係を利用した状態数削減
On-the-fly手法
ハッシュ手法
状態圧縮

第9章　抽象解釈―モデル検査の複雑さを軽減する
抽象化とは
データ抽象
述語抽象
抽象化と健全性
プログラムスライシング

第10章　モデル検査ツール―SPIN，SMV，LTSA，UPPAALを使う
SPIN, SMV, LTSA, UPPAAL