| 研究概要 |
本研究では,並列分散処理システムを,データの無限系列であるストリームによって相互に結合されるプロセスのネットワークとしてモデル化することにより,並行動作プログラムの開発における仕様記述,設計,テスト,デバッグを形式的手法に従って系統的に行なう方法の確立とそれを支援するシステムの開発を目的とし,今年度は以下の成果を得た.
1.並行動作プログラムの記述法の確立
関数型言語Mirandaを用いて種々の並行動作プログラムを記述し,実行可能な形式的仕様として,静的にも動的にも解析の対象とした.特に,不特定多数の並行プロセス間での共有データ空間を介した相互作用の記述を行った.
2.プログラムの検証および導出の事例研究
数学的な論証や式の展開としてのプログラムの検証および導出を伴う,並行動作プログラムの形式的開発方法論の確立のための基礎を得るために,形式的仕様記述言語Zを用いたシステム記述の事例研究を行った.
3.テスト結果自動判定機能
Mirandaで記述された実行可能仕様を実際にワークステーション上で実行させることにより,並行動作プログラムが要求される性質を満足することを自動的に判定するために,並行動作システムの振舞いを表現するストリームに関する条件として形式的に与え,それを自動的に検査する機能を考案して,実行可能仕様に付加した.
4.系統的デバッグ法に関する考察
先に我々が提示したデバッグに関する枠組みに沿って,並行動作プログラムの系統的デバッグ法を考案するために,特に,高階関数や多相型を持つMirandaプログラムにおける型誤りを型の体系に基づいて修正する方法を提案し,それを支援するツールを実現した.
|
