2004 Fiscal Year Annual Research Report
システムレベル記述の時間制約を考慮した抽象化およびモデル検査
| Project/Area Number |
16700062
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
中田 明夫 大阪大学, 大学院・情報科学研究科, 助教授 (60295839)
|
|---|
| Keywords | システムレベル記述言語 / 時間制約 / パラメトリックモデル検査 / 抽象化 / 時間弱トレース等価性 / 時間試験等価性 |
|---|
| Research Abstract |
ハードウェアのシステムレベル記述言語やソフトウェアプログラムから制御フローおよび各動作の時間制約に関する情報を抽出したモデルとして、パラメトリック時間インターバルオートマトン(Parametric Time-Inerval Automaton、以下PTIAと略す)を提案し、PTIAでモデル化されたシステム全体が要求される時間制約および動的性質を満たすために、各動作の実行時間の間で成立すべき制約条件を効率よく自動導出する手法(パラメトリックモデル検査)に関する研究を行った。
PTIAは時間オートマトンのサブクラスであり、状態を訪れてから各動作を実行するまでの時間の上限と下限を、一般にパラメタ変数を用いた式で記述できるモデルである。パラメトリックモデル検査は一般に非常に計算量が大きいため、PTIAに対して興味のある性質を保存したまま状態縮約(抽象化)を行う手法を考案した。抽象化で保存される性質としては、(1)時間弱トレース等価性、すなわち動作の実行系列が実行タイミングも含めて等しいなら等価とみなす等価性、および、(2)時間試験等価性、すなわち外界からの試験によって区別不可能なものを等価とみなす等価性、の2つを対象とした。(2)に関する研究成果は平成16年10月31日〜11月3日に国立台湾大学にて開催された国際会議「2nd Int. Conf. on Automated Technology for Verification and Analysis (ATVA2004)」にて発表した。一方、複数のPTIAの並列合成(積オートマトン)で構成されたシステムに対しては、(2)の抽象化は個々のPTIAの間で行われる通信の振る舞いを保存するため、個々のPTIAに対して独立に適用しても全体の性質は保存されるが、(1)の抽象化では一般に保存しない。しかし(2)よりも(1)の方が一般に状態縮約の効果が大きい。そこで、PTIAの積オートマトンが単一のPTIAに変換してから抽象化を行うアルゴリズムを考案し、それによる高速化の効果を実験的に確認した。この研究成果は平成17年1月31日〜2月2日に京都大学数理解析研究所で開催された国内会議「2004年度冬のLAシンポジウム」にて発表した。
|
