プロセス代数の応用に関する研究

过程代数应用研究

• 批准号: 05750326
• 负责人: 神長 裕明
• 金额: $ 0.58万
• 依托单位: Yamagata University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Encouragement of Young Scientists (A)
• 财政年份: 1993
• 资助国家: 日本
• 起止时间: 1993 至 无数据
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-05750326/
• 关键词: 検証; 等価性

プロセス代数は,特に同期型通信システムのモデルとして有効であることが認識されているにもかかわらず,LOTOS以外実用面にまだほとんど応用されていない.本研究では,プロセス代数の理論を特に等価性に基づいて,同期型通信システムの検証などに応用するとともに,その応用面での可能性について考察した.通信システムの検証においては,対象とする状態数が爆発的に増加してしまうという大きな問題点が従来から指摘されて未解決となっている.本研究では,この問題に対する一つのアプローチとして,等価性の概念を用いて状態空間をそれと等価な状態数の少ないものへと変換し,変換後の状態空間に対して従来の検証法を適用することにより効率的に検証を行う手法を開発した.さらに,この変換を自動的に行うアルゴリズムを開発し,そのシステムを開発中である.また,大規模な仕様に関してはそれを適切にモジュール化することが重要な問題であるが,この問題に関しても等価性の立場から,複雑な仕様を簡単な幾つかの仕様が結合した形式に等価変換するための手法について考察した.その結果,強bisimulation等価の概念を用いると複雑な仕様をある程度自動的にモジュール化することが可能であった.しかし,強bisimulation等価の概念は等価性としては制限が強すぎ,仕様に柔軟性が失われるため,もう少し制限の緩い等価性を用いた融通性のある変換法の開発が今後の課題である.

In addition to LOTOS,LOTOS is also used in applications other than LOTOS. In this paper, we investigate the theoretical basis of the equivalence of the synchronous communication system, and the feasibility of its application. During the verification of the communication system, the number of object states has increased and problems have been identified but remain unresolved. In this paper, we propose a new method for the identification of equivalence in state space. In this case, the automatic change of the system is under way. For example, large-scale enterprises are concerned with the appropriate forms of integration and transformation of important problems, problems of equal nature, complex problems, simple and simple forms of integration and transformation of methods. As a result, strong bisimulation and other concepts are used in complex systems to a certain extent automatically. The concept of strong bisimulation and so on is equal to the nature of the strong, the soft and the soft, and the soft and the soft.