ストリーム並列実行モデルに基づく並行動作プログラムの形式的開発法

1993 Fiscal Year Annual Research Report

• Project/Area Number: 04452196
• Research Institution: Nara Institute of Science and Technology
• Principal Investigator: 荒木 啓二郎 奈良先端科学技術大学院大学, 情報科学研究科, 教授 (40117057)
• Co-Investigator(Kenkyū-buntansha): 岡村 耕二 奈良先端科学技術大学院大学, 情報科学研究科, 助手 (70252830) ; 福田 晃 九州大学, 工学部, 助教授 (80165282)
• Keywords: 並行動作システム / ストリーム並列 / 形式的仕様 / 実行可能仕様 / 仕様記述言語Z / 仕様スライス / 並列オペレーティングシステム / 分散処理システム

Research Abstract

本研究では,並行動作プログラムの開発における仕様記述,設計,テスト,デバッグを形式的手法に基づいて系統的に行なう方法の確立とそれを支援するシステムの開発を目的とする.今年度は,仕様記述および並行動作システムの実現方式などを中心に以下の成果を得た.
1.システム記述法
システムの記述には,当初,関数型プログラミング言語Mirandaを用いた.これは,形式性と実行可能性を備えた実行可能仕様と位置付けられ,ソフトウェアシステム開発の上流工程における有用性を確認できた.更に仕様記述のレベルにおいて各種の形式的論証を行うために,形式的仕様記述言語Zも利用して,その有用性に対する見通しを得た.
2.システム記述支援
形式的仕様を作成する際には,当然それまでに記述した仕様の修正や改良や再利用を伴う.本研究では,Zによる形式的仕様に対して,仕様のスライスを提案し,これを応用することによって仕様の修正や再利用を効率よく進めるための方法を提示した.
3.並行動作システムの実現方式
本研究では,それ自体十分に解明されているわけではない並行動作システムを対象としているために,開発対象である並行動作システムの構成や処理方式に関しても研究を行った.具体的には,並列オペレーティングシステムの構成および処理方式,分散オペレーティングシステムの構成および処理方式,分散処理システムの試作と評価,マルチメディア通信システムのプロトコルおよび実現方式,コンピュータネットワーク上での分散協調作業の分析と支援ツールに対する要求分析などに関する研究を行った.ここで得られた成果や知見は,本研究の主要な課題であるシステムのモデル化や記述法に反映される.

Research Products

• [Publications] 福田晃: "並列オペレーティング・システム" 情報処理学会誌. Vol.34,No9. 1139-1149 (1993)
• [Publications] Hiroshi Maruyama: "Type Checking Slicing" Proc.InfoScience'93. 418-424 (1993)
• [Publications] Tomohiro Oda: "Specification Slicing in Formal Methods of Software Development" Proc.COMPSAC'93. 313-319 (1993)
• [Publications] Tomohiro Oda: "Application of Slicing Technique to Formal Specifications" Proc.JCSE'93. 203-210 (1993)
• [Publications] Koji Okamura: "Implementation and Study of ParaDisE on Distributed Environment" Proc.of the 8th Int'l Joint Workshop on Compuer Communication. C2-2-1-C2-2-6 (1993)
• [Publications] 古木良子: "Human-Orientedな形式的仕様記述法" ソフトウェアシンポジウム'94. (1994)