時間オートマトンによる実時間システムの形式的検証

摘要

時間オートマトンは，有限オートマトンの拡張であり，システムを離散的なイベントと連続的な時間経過の両方による状態遷移で記述するモデルである．時間オートマトンでは連続的な時間経過を扱うため，一般にクロックによる同期のない物理的な制御対象との相互作用を自然な形で記述可能である．また，離散イベント間の時間制約を記述可能であり，時間的な挙動と離散的な状態遷移が相互に影響しあう動作を記述できる．さらに，イベントと時間のみに着目し，ほかの観測量，制御量や具体的な入出力データなどを捨象するため，効率の良いモデル検査が可能で，実用に耐えるシールも近年整備されてきている．本稿では，時間オートマトンによる実時間システムの振る舞いのモデル化手法，および，安全性などの性質の形式的検証技術の概要について，技術の詳細な内容には立ち入らず，例題とツールを用いた検証の実例を交えて紹介する．