| 研究課題/領域番号 |
60550263
|
|---|
| 研究種目 |
一般研究(C)
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
情報工学
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
稲垣 康善 名大, 工学部, 教授 (10023079)
|
|---|
| 研究分担者 |
坂部 俊樹 三重大学, 工学部, 助教授 (60111829)
阿曽 弘具 名古屋大学, 工学部(昭和61年10月より東北大学・工学部), 助教授 (10005522)
|
|---|
| 研究期間 (年度) |
1985 – 1986
|
| 研究課題ステータス |
完了 (1986年度)
|
| 配分額 *注記 |
2,000千円 (直接経費: 2,000千円)
1986年度: 1,000千円 (直接経費: 1,000千円)
1985年度: 1,000千円 (直接経費: 1,000千円)
|
|---|
| キーワード | 並列計算システム / 代数的仕様記述法 / 仕様の検証 / CCS / CSP / 時相論理 / 通信プロトコルの仕様記述 / シストリックアルゴリズム |
|---|
| 研究概要 |
並列計算システムの形式性,記述性,理解性,簡潔性に優れた仕様記述ならびに検証のための体系の構成の基礎を確立することを目的として、以下の5項目について研究を行い、所期への成果を得ると共に、今後の研究の展望を得ることができた。
(1)相互通信逐次型プロセス系の正当性検証体系:CSPの実行可能な命令系列とその命令系列を実行途中に通る状態も含めて記録するセマンティックスとして計算履歴集合をcentralized approachによって定義し、それに基づいて、CSPの部分的正当性とデッドロックフリー性を同時に検証する公理系を与え、その健全性を示した。
(2)CCSの解析の基礎としてのw正規表現の代数:閉じた正規表現の代数に対する公理系を与え、その完全性を示した。CCSの方程式系の解を陽に与え、それと閉じた正規表現の間の関係の解明などは今後の課題である。
(3)CCSと抽象データ型の概念に基づく並行システムの代数的仕様記述法:CCSの同期通信で受渡しされる値の空間を抽象データ型として据え、それをCCSの中へ組込んでそれを代数的に記述する方法を提案し、その意味論を状態不通信木を導入することによって与えた。
(4)McDermottの時相論理に基づくプロトコルの仕様記述の検証法:McDermottの時相論理を基礎におき、プロトコルの仕様記述とその検証のための論理体系を与え、その健全性を示すと同時に、それをPrologを用いて実現した。
(5)シストリックアレイの仕様記述ならびに自動合成法:多重ループプログラムからシストリックアルゴリズムへの自動変換アルゴリズムを開発し、シストリックアルゴリズムにおける情報の流れに関する一般理論を構成し、その設計自動化の基礎を与えた。
|
