本研究では、モデルの単純さをできるだけ損なわないようにしながら、タイムペトリネットにレベル指向のための拡張を行うことにより、時間オートマトン並に使いやすくすると共に、partial order reduction技術による高速化を可能とした新しい形式モデル、および、その解析手法を開発すること、および、開発した技術をツールとしてまとめることを目的として研究を行った。 本研究は以下の順に行った。それぞれのステップでの成果の概要は次の通りである。 1.モデルの策定とプロトタイプの実装 トランジションの発火条件にバイナリ変数の積和形からなる条件式を書けるようにし、また、トランジションが発火する際には複数のバイナリ変数への値の代入を可能としたLTN(Level Time Petri net)をモデルとして選び、LTN用のpartial order reductionアルゴリズム、および、階層的検証手法を実装した解析エンジンのプロトタイプを作成した。 2.ケーススダディの実施 ケーススタディとして、非同期式プロセッサTITAC2の命令キャッシュ制御回路の検証を行った。特に、階層的検証の効果を確認するため、2つのブロックを選び、そのブロックの部分仕様を構築し、階層的検証を試みた。 3.ツールの本格的実装 タイムペトリネットから構成されるプリミティブ、プリミティブから構成されるモジュール、モジュールと仕様からなるシステム、および、検証対象となるシステムとしてプロジェクトを定義し、それらの階層性を見た目通りに管理できるGUIを設計した。さらに、このGUIを組み込み、最終的に検証ツールVINAS-P (Ver.2)を開発した。
|