オープンソフトウェアの形式モデルと検証技法に関する基礎的研究

1996 Fiscal Year Annual Research Report

• Project/Area Number: 08458066
• Research Category: Grant-in-Aid for Scientific Research (B)
• Research Institution: Nagoya University
• Principal Investigator: 稲垣 康善 名古屋大学, 工学部, 教授 (10023079)
• Co-Investigator(Kenkyū-buntansha): 河口 信夫 名古屋大学, 工学部, 助手 (10273286) ; 結縁 祥治 名古屋大学, 工学部, 助手 (70230612) ; 坂部 俊樹 名古屋大学, 工学部, 教授 (60111829)
• Keywords: ネットワーク / 通信プロセスモデル / 並行システム / 項書換え系 / 検証 / 実時間システム / 形式意味論 / メタ計算モデル

Research Abstract

本年度は,以下の項目について研究を実施した。
●オープンソフトウェアの形式モデルと意味論の開発
オープンソフトウェアの形式モデルとして通信プロセスモデルを定式化した。実時間性が複数のオープンソフトウェアを組み合わせる場合に、非常な重要な概念となることに注目し、主に実時間性を導入することで、より実際的な形式モデルを提案した。実時間通信プロセスモデルの正則なクラスに対して、意味論としてテスト擬順序を定義し、その証明技法を示した。本モデルでは、時間は実数領域を用いるため、無限の状態が存在するが、正則な実時間通信プロセスでは、振舞いが変化するポイントはその記述から記号的に有限表現できることに着目して、証明技法を提案した。
●オープンソフトウェアの形式モデルに対する計算メカニズムの開発
書換え型のメタ計算モデルのうち、動的項書換え計算(DTRC)の実装を行った。この実装において、項マッチングの速度と処理速度を向上させることのできるデータ構造を提案し、プロトタイプの実装を行った。
●オープンソフトウェアの検証システムの設計
書換え型の計算を一般に視覚化できるシステム(TERSE)の設計・開発を行った。このシステムによってオープンソフトウェア検証の過程を視覚化できるようになり、検証を行う際のヒューリスティックスの獲得を容易にすることができるようになった。

Research Products

• [Publications] 結縁祥治: "正則な実時間通信プロセスに対するテスト擬順序の記号的特性化" 電子情報通信学会論文誌(掲載決定).
• [Publications] 鈴木晃: "命令を並列に実行するCPUに対するSCCSによるコンパイラの仕様記述" 電子情報通信学会技術報告. COMP96-14. 49-58 (1996)
• [Publications] 鈴木晃: "SCCS動作式に対するunfold変換によるLTSモデルの効率的構成法" 電子情報通信学会技術報告. COMP96-47. 93-100 (1997)
• [Publications] K.Kawaguchi: "TERSE : A Visual Environment for Supporting Analysis,Verification and Transformation of Term Rewriting Systems" Proceedings of AMAST'96 (LNCS 1101). 571-574 (1996)
• [Publications] 西村徹: "動的項書き換え計算の実装" 平成8年度電気関係学会東海支部連合大会講演論文集. 328-328 (1996)
• [Publications] 河口信夫: "項書換え系における書換え系列の視覚化の拡張-中間実行とフィルター" 電気関係学会東海支部連合大会講演論文集. 659-659 (1996)