| Research Abstract |
本年度は,まず,リアルタイムソフトウェアを形式化するモデルの策定を行った.その結果,partial order reduction手法による効率的状態空間探索が有効に働く点,および,階層的検証手法が可能である点から,ペトリネット系のモデルを使用することとした.一方,純粋なペトリネットは可読性,記述性に問題があるため,トランジションの発火条件にバイナリ変数の積和形からなる条件式を書けるようにし,また,トランジションが発火する際には複数のバイナリ変数への値の代入を可能としたLTN(Level Time Petri net)を侯補とした.次に,LTN用のpartial order reductionアルゴリズム,および,階層的検証手法を実装した解析エンジンのプロトタイプを作成した.これを用いて,時間オートマトンに基づく検証ツール等と,記述能力,検証効率等を比較した結果,場合によっては記述能力が若干劣るものの,大きな問題ではなく,また,(階層的でない)フラットな検証実験でも同等あるいはそれ以上の検証効率を持つことがわかった.階層的検証の効果はまだ十分に解析できていないが,予備実験では検証コスト削減に非常に良好な結果が得られている.時間オートマトンツールは,そのような階層的検証の機能を持たないため,これは本方式の大きな利点となる.これらの検討から,モデルをLTNに確定しプロトタイプの実装を本格化した.さらに,次年度でツールとしてまとめる際に,このような階層的検証機能を容易に使うために,どのようなGUI(Graphic User Interface)を用意すべきかについて検討し,画面の構成,メニュー・コマシド等について検討を行った.
来年度は,ケーススタディを通して解析エンジンを最適化し,ツールとしての仕様(主にGUI)を定め,ソフトウェア会社に実装を発注する予定である.
|
