| 研究概要 |
本研究では,実用的な実時間システムの諸性質(安全性,設計の正しさ)を自動判定することを目標に,有理数プレスブルガー文の真偽判定アルゴリズムの実用的高速化方法を考案し,実際にそのような応用システムに使用できる真偽判定プログラムを実装する.
昨年までに基本アルゴリズムは完成し,また高速化のためのアルゴリズムの検討が終わっていた.そこで今年度はその高速アルゴリズムの実装と評価を行った.また評価実験の結果をまとめ論文投稿を行った.本研究の基本となるアルゴリズムは,従来の種々提案されてきた判定アルゴリズムとは大きく異なり,計算幾何学上のアルゴリズムに基づくものである.実装にあたり,表現データ構造である凸多面体の数をなるべく少なくする,真偽判定の処理に伴って必要であるデータ構造の変形をなるべく効率よく行う,冠頭標準形ではない,一般の形の式を扱えるようにするなどの工夫を行った.実装した有理数プレスブルガー文の真偽自動判定ルーチンに対して評価実験を行った結果を,非同期バス転送プロトコルの試験系列の自動生成など実用的な検証例題に適用した結果,十分実用時間で試験系列の生成ができることが確かめられた.また,一般のプレスブルガー文に対してアルゴリズムの振る舞いを調べた結果,改良前よりも高速に判定できることがわかった.
|
