内容説明
UPPAALは，モデル検査ツールとしては比較的利用が容易ではあるが，実際の開発には多くのハードルがある．本書では，そのようなハードルを乗り越えるために必要な，UPPAALツール，時間オートマトン，検証したい性質を記述するための時間時相論理に関する知識，および実際の開発で検証の対象となるUML設計仕様のUPPAALによるモデル化方法など，具体的事例も交えてノウハウを解説している．
目次
第1章 UPPAALを使ってみよう
第2章 UPPAALのシステムモデルと検証式
第3章 検証プロセス
第4章 ケーススタディ(1)オートクラッチ車ギア制御
第5章 ケーススタディ(2)オーディオデータ通信プロトコル
第6章 ソフトウェア設計とモデル検査
第8章 おわりに
付録 演習問題の解答例
