| 研究課題/領域番号 |
15300009
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウエア
|
|---|
| 研究機関 | 国立情報学研究所 |
|---|
研究代表者 |
米田 友洋 国立情報学研究所, 情報基盤研究系, 教授 (30182851)
|
|---|
| 研究期間 (年度) |
2003 – 2004
|
| 研究課題ステータス |
完了 (2004年度)
|
| 配分額 *注記 |
7,900千円 (直接経費: 7,900千円)
2004年度: 5,700千円 (直接経費: 5,700千円)
2003年度: 2,200千円 (直接経費: 2,200千円)
|
|---|
| キーワード | Level Time Petri nets / Partial order reduction / 階層的検証 / リアルタイムソフトウェア / 時間オートマトン / 形式的検証 / レベルタイムペトリネット |
|---|
| 研究概要 |
本研究では、モデルの単純さをできるだけ損なわないようにしながら、タイムペトリネットにレベル指向のための拡張を行うことにより、時間オートマトン並に使いやすくすると共に、partial order reduction技術による高速化を可能とした新しい形式モデル、および、その解析手法を開発すること、および、開発した技術をツールとしてまとめることを目的として研究を行った。
本研究は以下の順に行った。それぞれのステップでの成果の概要は次の通りである。
1.モデルの策定とプロトタイプの実装
トランジションの発火条件にバイナリ変数の積和形からなる条件式を書けるようにし、また、トランジションが発火する際には複数のバイナリ変数への値の代入を可能としたLTN(Level Time Petri net)をモデルとして選び、LTN用のpartial order reductionアルゴリズム、および、階層的検証手法を実装した解析エンジンのプロトタイプを作成した。
2.ケーススダディの実施
ケーススタディとして、非同期式プロセッサTITAC2の命令キャッシュ制御回路の検証を行った。特に、階層的検証の効果を確認するため、2つのブロックを選び、そのブロックの部分仕様を構築し、階層的検証を試みた。
3.ツールの本格的実装
タイムペトリネットから構成されるプリミティブ、プリミティブから構成されるモジュール、モジュールと仕様からなるシステム、および、検証対象となるシステムとしてプロジェクトを定義し、それらの階層性を見た目通りに管理できるGUIを設計した。さらに、このGUIを組み込み、最終的に検証ツールVINAS-P (Ver.2)を開発した。
|
