複雑・多様化するシステムの形式検証のために。堅牢なシステム構築のための、システムの数理的なモデル化・解析手法の理論的背景を詳説。

第１部　システムのモデル化（システムの概念
オートマトンと形式言語　ほか）
第２部　性質・ふるまいの記述（時相論理によるシステムの性質の記述
遷移システム・ラベル付き遷移システム）
第３部　拡張モデル（時間・確率システムのモデル化
ハイブリッドシステムのモデル化）
第４部　解析・検証・制御（基本的解析問題
決定性時間システム・ハイブリッドシステムの解析　ほか）