モデル検査 上級編

第1章 導入 第2章 状態遷移系の合成 第3章 抽象化-状態数を減らす 第4章 CTL(計算木論理) 付録A 仕様記述言語Promela 付録B NuSMVの仕様記述言語 付録C 演習環境について