1992 Fiscal Year Annual Research Report
ストリーム並列実行モデルに基づく並行動作プログラムの形式的開発法
| Project/Area Number |
04452196
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
荒木 啓二郎 九州大学, 工学部, 助教授 (40117057)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
最所 圭三 九州大学, 工学部, 講師 (50170486)
古川 善吾 九州大学, 情報処理教育センター, 助教授 (30190135)
程 京徳 九州大学, 工学部, 助教授 (30217228)
福田 晃 九州大学, 工学部, 助教授 (80165282)
|
|---|
| Keywords | 並行動作プログラム / ストリーム / 形式的仕様 / 関数型プログラミング言語 / Miranda / 仕様記述言語Z / テスト / デバッグ |
|---|
| Research Abstract |
本研究では,並列分散処理システムを,データの無限系列であるストリームによって相互に結合されるプロセスのネットワークとしてモデル化することにより,並行動作プログラムの開発における仕様記述,設計,テスト,デバッグを形式的手法に従って系統的に行なう方法の確立とそれを支援するシステムの開発を目的とし,今年度は以下の成果を得た.
1.並行動作プログラムの記述法の確立
関数型言語Mirandaを用いて種々の並行動作プログラムを記述し,実行可能な形式的仕様として,静的にも動的にも解析の対象とした.特に,不特定多数の並行プロセス間での共有データ空間を介した相互作用の記述を行った.
2.プログラムの検証および導出の事例研究
数学的な論証や式の展開としてのプログラムの検証および導出を伴う,並行動作プログラムの形式的開発方法論の確立のための基礎を得るために,形式的仕様記述言語Zを用いたシステム記述の事例研究を行った.
3.テスト結果自動判定機能
Mirandaで記述された実行可能仕様を実際にワークステーション上で実行させることにより,並行動作プログラムが要求される性質を満足することを自動的に判定するために,並行動作システムの振舞いを表現するストリームに関する条件として形式的に与え,それを自動的に検査する機能を考案して,実行可能仕様に付加した.
4.系統的デバッグ法に関する考察
先に我々が提示したデバッグに関する枠組みに沿って,並行動作プログラムの系統的デバッグ法を考案するために,特に,高階関数や多相型を持つMirandaプログラムにおける型誤りを型の体系に基づいて修正する方法を提案し,それを支援するツールを実現した.
|
Research Products
(6 results)
-
[Publications] Tomohiro Oda: "Development of Functional Programming Language Systems based on Formal Method" Proc.1992 International Computer Symposium.85-91 (1992)
-
[Publications] Hiroshi Maruyama: "Support Tool and Strategy for Type Error Correction with Polymorphic Types" Proc.COMPSAC 92. 287-293 (1992)
-
[Publications] Akira Fukuda: "Analysis of Input Control with Control Delay" J.Infomation Processing. 15. 435-443 (1992)
-
[Publications] Jingde Cheng: "The Process Dependence Net in a Practical Concurrent Programming Environment" Proc.Joint International Conterence on Software Engineering. 227-233 (1992)
-
[Publications] 古川 善吾: "並行処理プログラムにおける共有変数のデータフローテスト基準" 情報処理学会論文誌. 33. 1394-1401 (1992)
-
[Publications] Keizo Saisho: "Toward the Optimal Parallel Processing of a Single Doacross Loop on NUMA Multiprocessors" Proc.International Computer Symposium. 1320-1327 (1992)
