ソフトウェアが正しく設計されているかを保証するための手法として，システムを数学的に厳密なモデルで記述し，仕様が満たされているかどうかを数理的に調べる，「形式検証」が注目されている．

本書では，モデル検査に代表されるように，現実のシステムにも適用可能になってきた形式検証を理解し，使いこなすための理論的背景について解説する．

離散事象システム，実時間システム，ハイブリッドシステムなど，さまざまなシステムに対する形式的モデル化手法と，その解析方法が網羅された1冊．
◆第1部　システムのモデル化
第1章　システムの概念
第2章　オートマトンと形式言語
第3章　ペトリネット
第4章　プロセス代数

◆第2部　性質・ふるまいの記述
第5章　時相論理によるシステムの性質の記述
第6章　遷移システム・ラベル付き遷移システム

◆第3部　拡張モデル
第7章　時間・確率システムのモデル化
第8章　ハイブリッドシステムのモデル化

◆第4部　解析・検証・制御
第9章　基本的解析問題
第10章　決定性時間システム・ハイブリッドシステムの解析
第11章　確率システムの解析
第12章　モデル検査
第13章　離散事象システムの制御

付録A　数学用語の解説
付録B　演習問題の解答例