UPPAAL拡張時間オートマトンの反例に基づく抽象化改良ループによるモデル抽象化手法

摘要

近年,情報システムの高信頼設計においてモデル検査は重要な役割を果たすようになってきている.実時間システムのモデル検査では,モデルの状態数が状態変数やクロック変数に対して指数的に増加し,スケーラビリティに厳しい制限が生じる.本稿では,時間モデル検査ツールであるUPPAALで用いられる拡張時間オートマトンに対する具体的なモデル抽象化手法を提案する.モデル抽象化技法はこのスケーラビリティ改善のための主要な手法として注目を浴びている.本手法では,Clarkeらが提案した反例に基づいた抽象化改良ループCEGARを適用しており,抽象化から検査までの全ての工程を自動的に行うことが可能である.また,反例によるモデルの再抽象化においては時間オートマトンの検証で用いられるデータ構造DBMを活用する工夫を行なっている.