| 研究課題/領域番号 |
08458066
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
稲垣 康善 名古屋大学, 大学院・工学研究科, 教授 (10023079)
|
|---|
| 研究分担者 |
河口 信夫 名古屋大学, 大学院・工学研究科, 助手 (10273286)
結縁 祥治 名古屋大学, 大学院・工学研究科, 助手 (70230612)
酒井 正彦 名古屋大学, 大学院・工学研究科, 助教授 (50215597)
坂部 俊樹 名古屋大学, 大学院・工学研究科, 教授 (60111829)
|
|---|
| キーワード | 並行プログラミング / 通信プロセスモデル / 形式意味論 / プログラミング環境 / デバッグ |
|---|
| 研究概要 |
本研究は通信環境に依存して動作が決定するオープンソフトウァを通信プロセスモデルに基づいてモデル化し、形式的意味論に基づいた検証法の確立を図るものである。
今年度は、昨年度に引続き(1)実用上の観点からの実時間意味論の拡張と検証の基礎となる代替特性化について考察を行なった。このほかに、(2)テスト意味論に基づく視覚的デバッガの試作、(3)オープンソフトウァのための仕様記述の設計を行った。その結果、以下の知見が得られた。
(1)時間の概念をオープンソフトウェアに導入することは、タイムアウトなど実用上の観点からは非常に自然な概念であるにもかかわらず、検証の点からは非常に複雑である。これは、状態変化が時間に依存するため、直観的にはすべての時間においての検証が要求されるためである。このため、代替特性化によって検証手続きを提案してが、実用的な記述とのギャップがまだ大きく(3)の研究との接点については今後の課題となった。
テスト等価性の意味論に基づいたデバッガでは、いかにしてユーザに理解可能な形で修正を提示するかが問題となった。この点に関して、モジュールの展開と合成を自動的に行うことにより、改善が得られた。
オープンソフトウェアの基本設計として構造的操作意味記述(SOS記述)について検討した。離散時間をとりいれたSOS記述に対して、モジュール性を表す合同性に関する結果を得た。
|
