| 研究概要 |
本研究では,実時間制約を持つシステムの検証を階層的に行い,非常に高効率な時間検証方式を開発することを目的とする.本研究の成果は以下の3点である.(1)仕様および検証対象システムをタイムペトリネットを用いてモデル化することとし,スタンフォード大のD.Dillらによる,ペトリネットに基づく検証方式をベースに検証アルゴリズムを開発した.Dillらの方式は,非同期式回路の(時間を含まない)性質の検証が目的であり,実時間は扱えない.そこで,Dillらのアルゴリズムの根底をなすトレース理論を拡張し,時間トレース理論を提案した.これにより,実時間制約を持つシステムのsafety性のほか,Dillらの方式では容易には扱えなかった(ある種の)liveness性も容易に扱えるようになった.(2)時間トレース理論に基づき,仕様および検証対象システム(いくつかのモジュールから成る)を表すいくつかのタイムペトリネットの状態空間を探索し,各可到達状態がsafetyあるいはlivenessに反していないかどうかを調べるアルゴリズムを開発した.また,実際にインプリメントした.(3)いくつかの例を用いて検証を行った結果,確かに階層的検証により大幅に検証時間を削滅できることがわかったが,一状態あたりの処理にやや時間がかかり過ぎるという問題が見つかった.検討の結課,状態を表す連立一次不等式の標準形を求めるのにかなりの時間がかかっていることがわかった.そこで,タイムペトリネットの状態を表す連立一次不等式の特殊性に着目し,従来用いていたO(n^3)のアルゴリズムを改良し,O(n^2)のアルゴリズムを開発した.以上より,本研究の目的はほぼ達成できたが,さらに効率を向上するため,不要な順序関係を生成しないように状態探索を行うというpartial orderの考え方を導入し,アルゴリズムを改良することが今後の課題である.
|
