抽象化と精密化による実時間モデル検査の改善
スポンサーリンク
概要
- 論文の詳細を見る
本研究の目的は,抽象化・精密化の手法を用いて,実時間モデル検査の状態数爆発問題を解決することにある.実時間モデル検査は,実時間システムの検証に用いられる手法で,そのシステムを時間オートマトンで記述する.実時間モデル検査における状態数爆発問題は,探索する状態空間が,実数値をとるクロック変数の数に対し指数的に大きくなり,実用的な時間内で検査が終了しないというものである.抽象化・精密化に基づくぞデル検査法では,抽象化によりクロック変数をすべて省いた,初期抽象システムを構築し検査する.しかし,このような抽象化では検証結果として,間違った結果すなわち偽物の反側を得てしまうことがある.その場合,初期抽象システムから抽象化のレベルを低くしたシステムに作り替え,検証をやり直す.これを,正しい結果が得られるまで繰り返す.この手法の最大の課題は,得られた反側を基に,抽象化のレベルが高くかつ検証可能なシステムをどのように作るかということである.提案手法では,取り除いた変数のうち必要なものを復元する精密化を行う.また状態数を抑えるため,システム全体に変数を復元するのではなく,部分的に復元する.さらにクロック変数を復元せず不必要な遷移を除去する,もう1つの精密化を併用することで状態数の増加を抑える.本稿では,提案手法の適用例として時間オートマトンの到達可能性解析を試み,実験でその有効性の検証を行った.
- 2004-11-15
著者
関連論文
- 二階文脈計算(プログラミング及びプログラミング言語)
- 定理証明システムCoq上でのPre Logical Relationを用いた詳細化の正しさの証明
- 自己反映的証明体系RPTの理論と実現
- 抽象化と精密化による実時間モデル検査の改善
- 多値モデル検査を利用したモデル化の誤りの発見
- 限定継続に基づくスケーラブルなウェブアプリケーション構築手法
- 1Q-5 マルチステージプログラミングのための計算体系の実装(プログラミング言語・実装・支援,学生セッション,ソフトウェア科学・工学)
- 動的環境と限定継続を持つプログラム言語の意味論と実装
- オブジェクト指向言語に対するメタプログラミング言語の設計と実装
- 階層化コントロールオペレータに対する型システムの構築
- 構成的数学体系RPTに基づく超数学の定理の形式化
- 結果型を変更可能な限定継続の模倣