著者

中島 一 亀山 幸義

出版者

一般社団法人情報処理学会

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.45, no.12, pp.11-24, 2004-11-15

被引用文献数

2

---

本研究の目的は,抽象化・精密化の手法を用いて,実時間モデル検査の状態数爆発問題を解決することにある.実時間モデル検査は,実時間システムの検証に用いられる手法で,そのシステムを時間オートマトンで記述する.実時間モデル検査における状態数爆発問題は,探索する状態空間が,実数値をとるクロック変数の数に対し指数的に大きくなり,実用的な時間内で検査が終了しないというものである.抽象化・精密化に基づくモデル検査法では,抽象化によりクロック変数をすべて省いた,初期抽象システムを構築し検査する.しかし,このような抽象化では検証結果として,間違った結果すなわち偽物の反例を得てしまうことがある.その場合,初期抽象システムから抽象化のレベルを低くしたシステムに作り替え,検証をやり直す.これを,正しい結果が得られるまで繰り返す.この手法の最大の課題は,得られた反例を基に,抽象化のレベルが高くかつ検証可能なシステムをどのように作るかということである.提案手法では,取り除いた変数のうち必要なものを復元する精密化を行う.また状態数を抑えるため,システム全体に変数を復元するのではなく,部分的に復元する.さらにクロック変数を復元せず不必要な遷移を除去する,もう1 つの精密化を併用することで状態数の増加を抑える.本稿では,提案手法の適用例として時間オートマトンの到達可能性解析を試み,実験でその有効性の検証を行った.We address the state explosion problem in real-time model checking. Real-time model checking automatically verifies real-time systems described as timed automata. This method suffers from the state explosion problem: the size of the state space grows exponentially with the number of real-valued clock variables. We use abstraction-refinement for reducing the state space. Using this method, an initial abstract system, which is an over-approximation to behaviors of the timed automaton, is constructed by removing all clock variables, and then the abstract system is verified. This kind of conservative abstraction may lead to a false result, that is a spurious counterexample. In this case, the abstract system is refined on the basis of the counterexample and the refined system is verified. The process is repeated until a correct result is obtained. The difficulty in this method is how the system is refined. In our approach, we extract clock variables needed in the refinement. Additionally, we do not refine the whole system but a part of the system. Besides this refinement, we introduce another refinement removing transitions which are proved to never fire in the timed automaton. Our approach avoids the state explosion problem by combining these refinements. In this work, we apply our techniques to reachability analysis of timed automata.