| 研究課題/領域番号 |
08458066
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
稲垣 康善 名古屋大学, 工学研究科, 教授 (10023079)
|
|---|
| 研究分担者 |
河口 信夫 名古屋大学, 工学研究科, 助手 (10273286)
結縁 祥治 名古屋大学, 工学研究科, 助手 (70230612)
酒井 正彦 名古屋大学, 工学研究科, 助教授 (50215597)
坂部 俊樹 名古屋大学, 工学研究科, 教授 (60111829)
|
|---|
| 研究期間 (年度) |
1996 – 1997
|
| 研究課題ステータス |
完了 (1997年度)
|
| 配分額 *注記 |
7,800千円 (直接経費: 7,800千円)
1997年度: 1,200千円 (直接経費: 1,200千円)
1996年度: 6,600千円 (直接経費: 6,600千円)
|
|---|
| キーワード | 並行プログラミング / 通信プロセスモデル / 形式意味論 / プログラミング環境 / デバッグ / ネットワーク / 並行システム / 項書換え系 / 検証 / 実時間システム / メタ計算モデル |
|---|
| 研究概要 |
本研究は通信環境に依存して動作が決定するオープンソフトウェアを通信プロセスモデルに基づいてモデル化し、形式的意味論に基づいた検証法の確立を図るものである。本研究により、以下の結果が得られた。
(1)通信プロセスモデルに対する時間拡張に対して、従来からのテスト等価性意味を拡張し、検証のための代替特性化を導いた。
(2)通信プロセスモデルに対して確率分布によって非決定性を解決するモデル拡張に対して、従来からのテスト等価性意味を拡張し、検証のための代替特性化を導いた。
(3)離散時間に拡張した通信プロセスの操作意味定義に対して、合同性を保つ条件、および、時間の良定義性の条件を示した。
(4)オープンソフトウェアの理論的な意味づけにおいて、自己認識論理の基本的な枠組を検討した。
(5)オープンソフトウェアの設計において、通信プロセスモデルに基づくデバッグ手法を提案し、ツールのプロトタイプを実装した。
(6)オープンソフトウェアに対して、抽象的な仕様と実装のための情報を組み合わせた記述を提案し、C言語によるプログラム生成系を試作した。
|
