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

基于流并行执行模型的并行运行程序形式化开发方法

• 批准号: 04452196
• 负责人: 荒木 啓二郎
• 金额: $ 2.82万
• 依托单位: Nara Institute of Science and Technology (1993)Kyushu University (1992)
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for General Scientific Research (B)
• 财政年份: 1992
• 资助国家: 日本
• 起止时间: 1992 至 1993
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-04452196/
• 关键词: 並行動作システム; ストリーム並列; 形式的仕様; 実行可能仕様; 仕様記述言語Z; 仕様スライス; 並列オペレーティングシステム; 分散処理システム; 並行動作プログラム; ストリーム; 関数型プログラミング言語; Miranda; テスト; デバッグ

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

This study is aimed at describing, designing, developing, and supporting the development of parallel motion systems. This year, the following results were obtained from the description of the system: 1. the description of the system: 2. the description of the system: 3. the description of the system: 4. the description of the system: 5. the description of the system: 6. the description of the system: 7. the description of the system: 8. the description of the system: 9. the description of the system: 8. the system: 9. This is a formal and practical possibility. It is possible to establish a practical and practical position. It is possible to establish a practical and practical project. In addition, various forms of argumentation are described in the form of official description. 2. The description of official description is supported by the description of official description. 2. The description of official description is modified and reused. This study is aimed at solving the problem of parallel motion and improving its efficiency. The research of parallel motion of open image and its processing mode Specifically, the composition and processing method of the parallel selection system, the composition and processing method of the decentralized selection system, the trial evaluation of the decentralized processing system, the analysis and support of the decentralized coordination operation of the communication system, and the related research. The main topic of this study is to reflect the results of the research.

项目成果

福田晃: "並列オペレーティング・システム" 情報処理学会誌. Vol.34,No9. 1139-1149 (1993)

Akira Fukuda：“并行操作系统”日本信息处理学会杂志，第 34 卷，第 9 期。1139-1149 (1993)

古木良子: "Human-Orientedな形式的仕様記述法" ソフトウェアシンポジウム'94. (1994)

Yoshiko Furuki：“以人为本的形式规范描述方法”软件研讨会 94（1994）。

Akira Fukuda: "Analysis of Input Control with Control Delay" J.Infomation Processing. 15. 435-443 (1992)

Akira Fukuda：“具有控制延迟的输入控制分析”J.信息处理。

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)

Koji Okamura：“分布式环境中 ParaDisE 的实现与研究”第八届计算机通信国际联合研讨会论文集。

Hiroshi Maruyama: "Support Tool and Strategy for Type Error Correction with Polymorphic Types" Proc.COMPSAC 92. 287-293 (1992)

Hiroshi Maruyama：“多态类型类型错误校正的支持工具和策略”Proc.COMPSAC 92. 287-293 (1992)