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

1997 Fiscal Year Annual Research Report

• Project/Area Number: 08458066
• Research Institution: Nagoya University
• Principal Investigator: 稲垣 康善 名古屋大学, 大学院・工学研究科, 教授 (10023079)
• Co-Investigator(Kenkyū-buntansha): 河口 信夫 名古屋大学, 大学院・工学研究科, 助手 (10273286) ; 結縁 祥治 名古屋大学, 大学院・工学研究科, 助手 (70230612) ; 酒井 正彦 名古屋大学, 大学院・工学研究科, 助教授 (50215597) ; 坂部 俊樹 名古屋大学, 大学院・工学研究科, 教授 (60111829)
• Keywords: 並行プログラミング / 通信プロセスモデル / 形式意味論 / プログラミング環境 / デバッグ

Research Abstract

本研究は通信環境に依存して動作が決定するオープンソフトウァを通信プロセスモデルに基づいてモデル化し、形式的意味論に基づいた検証法の確立を図るものである。
今年度は、昨年度に引続き(1)実用上の観点からの実時間意味論の拡張と検証の基礎となる代替特性化について考察を行なった。このほかに、(2)テスト意味論に基づく視覚的デバッガの試作、(3)オープンソフトウァのための仕様記述の設計を行った。その結果、以下の知見が得られた。
(1)時間の概念をオープンソフトウェアに導入することは、タイムアウトなど実用上の観点からは非常に自然な概念であるにもかかわらず、検証の点からは非常に複雑である。これは、状態変化が時間に依存するため、直観的にはすべての時間においての検証が要求されるためである。このため、代替特性化によって検証手続きを提案してが、実用的な記述とのギャップがまだ大きく(3)の研究との接点については今後の課題となった。
テスト等価性の意味論に基づいたデバッガでは、いかにしてユーザに理解可能な形で修正を提示するかが問題となった。この点に関して、モジュールの展開と合成を自動的に行うことにより、改善が得られた。
オープンソフトウェアの基本設計として構造的操作意味記述(SOS記述)について検討した。離散時間をとりいれたSOS記述に対して、モジュール性を表す合同性に関する結果を得た。

Research Products

• [Publications] 結縁祥治、坂部俊樹、稲垣康善: "正則実時間通信プロセスの記号的代替特性化" 電子情報通信学会分誌. J80-D-I-6. 474-485 (1997)
• [Publications] S.Feng, T.Sakabe, Y.Inagaki: "Confluence Progerty of Simple Frames in Dynamic Term Rewriting Systems" IEICE Trans. on Information and Systems. E80-D-4. 510-517 (1997)
• [Publications] 外山晴彦、稲垣康善、福村晃夫: "多エージェント系自己認識論理に基づく状態継続と因果関係の表現" 人工知能学会論文誌. Vol.12. 466-474 (1997)
• [Publications] M.Sakai: "Left-Incompatible Term Rewriting Systems and Functional Strategy" IEICE Trans. on Information and Systems. E80-D-12. 1176-1182 (1997)
• [Publications] R.Cleaveland, Z.Dayar, S.A.Smolka, S.Yuen, A.Zwarico: "Testing Preorders for Probabilistic processes" Information and Computation. (to appear). (1998)