第1章　設計モデル検証とモデル検査
第2章　モデル検査概論
第3章　モデル検査ツールSPIN概要
第4章　SPINによるモデル検査
第5章　SPINによる設計モデルの検証プロセス
第6章　設計モデルの検証の実際
第7章　検証の実践：抽象化・効率化・デバッグ

付録A　PROMELA/SPINリファレンスマニュアル
付録B　設計モデルの検証プロセス
付録C　簡易ステートマシン図のシンタックスとセマンティクス
付録D　簡易ステートマシン図とPROMELAの対応