研究課題/領域番号 |
08458066
|
研究種目 |
基盤研究(B)
|
研究機関 | 名古屋大学 |
研究代表者 |
稲垣 康善 名古屋大学, 工学部, 教授 (10023079)
|
研究分担者 |
河口 信夫 名古屋大学, 工学部, 助手 (10273286)
結縁 祥治 名古屋大学, 工学部, 助手 (70230612)
坂部 俊樹 名古屋大学, 工学部, 教授 (60111829)
|
キーワード | ネットワーク / 通信プロセスモデル / 並行システム / 項書換え系 / 検証 / 実時間システム / 形式意味論 / メタ計算モデル |
研究概要 |
本年度は,以下の項目について研究を実施した。 ●オープンソフトウェアの形式モデルと意味論の開発 オープンソフトウェアの形式モデルとして通信プロセスモデルを定式化した。実時間性が複数のオープンソフトウェアを組み合わせる場合に、非常な重要な概念となることに注目し、主に実時間性を導入することで、より実際的な形式モデルを提案した。実時間通信プロセスモデルの正則なクラスに対して、意味論としてテスト擬順序を定義し、その証明技法を示した。本モデルでは、時間は実数領域を用いるため、無限の状態が存在するが、正則な実時間通信プロセスでは、振舞いが変化するポイントはその記述から記号的に有限表現できることに着目して、証明技法を提案した。 ●オープンソフトウェアの形式モデルに対する計算メカニズムの開発 書換え型のメタ計算モデルのうち、動的項書換え計算(DTRC)の実装を行った。この実装において、項マッチングの速度と処理速度を向上させることのできるデータ構造を提案し、プロトタイプの実装を行った。 ●オープンソフトウェアの検証システムの設計 書換え型の計算を一般に視覚化できるシステム(TERSE)の設計・開発を行った。このシステムによってオープンソフトウェア検証の過程を視覚化できるようになり、検証を行う際のヒューリスティックスの獲得を容易にすることができるようになった。
|