| 研究分担者 |
岡村 耕二 奈良先端科学技術大学院大学, 情報科学研究科, 助手 (70252830)
福田 晃 九州大学, 工学部, 助教授 (80165282)
最所 圭三 九州大学, 工学部, 講師 (50170486)
古川 善吾 九州大学, 情報処理教育センター, 助教授 (30190135)
程 京徳 九州大学, 工学部, 助教授 (30217228)
|
|---|
| 研究概要 |
本研究では,並行動作プログラムの開発における仕様記述,設計,テスト,デバッグを形式的手法に基づいて系統的に行なう方法の確立とそれを支援するシステムの開発を目的とする.今年度は,仕様記述および並行動作システムの実現方式などを中心に以下の成果を得た.
1.システム記述法
システムの記述には,当初,関数型プログラミング言語Mirandaを用いた.これは,形式性と実行可能性を備えた実行可能仕様と位置付けられ,ソフトウェアシステム開発の上流工程における有用性を確認できた.更に仕様記述のレベルにおいて各種の形式的論証を行うために,形式的仕様記述言語Zも利用して,その有用性に対する見通しを得た.
2.システム記述支援
形式的仕様を作成する際には,当然それまでに記述した仕様の修正や改良や再利用を伴う.本研究では,Zによる形式的仕様に対して,仕様のスライスを提案し,これを応用することによって仕様の修正や再利用を効率よく進めるための方法を提示した.
3.並行動作システムの実現方式
本研究では,それ自体十分に解明されているわけではない並行動作システムを対象としているために,開発対象である並行動作システムの構成や処理方式に関しても研究を行った.具体的には,並列オペレーティングシステムの構成および処理方式,分散オペレーティングシステムの構成および処理方式,分散処理システムの試作と評価,マルチメディア通信システムのプロトコルおよび実現方式,コンピュータネットワーク上での分散協調作業の分析と支援ツールに対する要求分析などに関する研究を行った.ここで得られた成果や知見は,本研究の主要な課題であるシステムのモデル化や記述法に反映される.
|
