| Research Abstract |
本年度は,まずケーススタディとして,非同期式プロセッサTITAC2の命令キャッシュ制御回路の検証を行った.特に,階層的検証の効果を確認するため,2つのブロックを選び,そのブロックの部分仕様を構築し,階層的検証を試みた.最終的には,階層的検証の効果は十分に確認できたが,部分仕様の構築がそれほど容易ではないという問題点も明らかとなった.この問題を解決するため,ブロックの構造から,ある程度機械的に部分仕様を導出する手法を考案し,それを適用することにより,ある程度の効果が得られることがわかった.これは,新たな知見であり,まだ改良の余地があることから,今後の発展へとつなげたい.
次に,このような階層的検証の機能を容易に使うため,どのようなGUI(Graphic User Interface)を用意すべきかについて検討した.(タイム)ペトリネットから構成されるプリミティブ,プリミティブから構成されるモジュール,モジュールと仕様からならるシステム,および,検証対象となるシステムとしてプロジェクトを定義し,それらの階層性を見た目通りに管理できるGUIを設計した.特に,プロジェクトの要素であるモジュールは,自由に部分仕様を設定し,部分仕様とそのモジュール間の検証,および,検証が成功した場合のモジュールの部分仕様による置き換えが容易に行えるように留意した.このようなGUIの仕様を策定し,ソフトウェア会社に実装を発注した.その後,ソフトウェア会社の設計担当者と打ち合わせを繰り返し,GUIの仕様を適宜修正することにより,より使いやすいシステムを開発することができた.マニュアル等を整備し,webサイトにて近いうちに公開する予定である.
|
