Design Support of Autonomous Distributed Systems by Integratig Temporal Logic, Concurrency Theny, Autom

集成时态逻辑、并发 Theny、Autom 的自治分布式系统设计支持

• 批准号: 11680360
• 负责人: YAMANE Satoshi
• 金额: $ 0.77万
• 依托单位: Kanazawa University (2001)Kagoshima University (1999-2000)
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 1999
• 资助国家: 日本
• 起止时间: 1999 至 2001
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-11680360/
• 关键词: open distributed systems; stepwise refinement; refinement verification; timed automata; hybrid models; Assume-Guarantee; receptioneness; specification; 分散システム; 開放型システム; 実時間処理; 計算機支援; 時相論理; 演繹的検証; リアルタイム性; receptive

In this study, we realize our new design support system of distributed systems by-integrating existing formal methods. We formalize distributed systems as open distributed systems by real-time models or hybrid models, and verify them by automatic or deductive methods. We have developed the following four methods :(1)Automatic design support of real-time open distributed systems by Assume-guararnee methods : We have developed open timed automata and realized automatic verification of timed simulation relations and receptiveness by Assume-guarantee styles. Using this method, we can develop real distributed systems based on stepwise refinements.(2) Deductive design support of real-time open distributed systems : We have developed timed stateoharts and realized deductive refinement verification methods. Using this method, we can develop distributed systems represented by infinite states systems based on stepwise refinements.(3) Deductive design support of real-time open distributed systems by Assume-guarantee methods : We have developed clocked transition modules and realized deductive refinement verification methods and receptiveness verification methods by Assume-guarantee methods. Using this method, we can develop real distributed systems based on stepwise refinements.(4) Deductive design support of hybrid open distributed systems : We have developed phase transition | modules and realized deductive refinement derification methods. Using this method, we can develop I distributed systems represented by control laws based on stepwise refinements.We are now implementing our proposed methods by theorem provers and applying it to large systems.

在这项研究中，我们实现了我们的新的分布式系统的设计支持系统，通过整合现有的形式化方法。我们通过实时模型或混合模型将分布式系统形式化为开放的分布式系统，并通过自动或演绎的方法对其进行验证。（1）基于假设-保证的实时开放分布式系统的自动设计支持：开发了开放时间自动机，实现了基于假设-保证的时间仿真关系和可接受性的自动验证。使用这种方法，我们可以基于逐步改进来开发真实的分布式系统。(2)实时开放分布式系统的演绎设计支持：我们已经开发了定时状态图，并实现了演绎细化验证方法。使用这种方法，我们可以开发分布式系统表示的无限状态系统的基础上逐步细化。(3)假设保证方法对实时开放分布式系统的演绎设计支持：开发了时钟转换模块，实现了基于假设保证方法的演绎精化验证方法和接受性验证方法。使用这种方法，我们可以开发真实的分布式系统的基础上逐步细化。(4)混合开放分布式系统的演绎设计支持：我们开发了相变|模块，实现了演绎求精的证明方法。使用这种方法，我们可以开发I分布式系统表示的控制律的基础上逐步refinements.We现在实现我们提出的方法定理证明器和应用到大型系统。

项目成果

山根智,山ノ口崇: "AND構造とOR構造の分解による実時間ソフトウェアの安全性の演繹的検証"レクチャーノート(近代科学社). 25. 237-248 (2000)

Satoshi Yamane、Takashi Yamanoguchi：“通过分解 AND 和 OR 结构进行实时软件安全性的演绎验证”讲义（Kinda Kagakusha）（Kinda Kagakusha）。

山根智,山ノ口崇: "実時間システムの演繹的検証"電子情報通信学会研究報告SS2000. 2000・6. 1-8 (2000)

Satoshi Yamane、Takashi Yamanoguchi：“实时系统的演绎验证”IEICE 研究报告 SS2000・6.1-8 (2000)。

山根智,山ノ口崇: "実時間システムの演繹的検証と自動演繹的検証"情報処理学会研究報告MPS2000. 2000・29. 5-8 (2000)

Satoshi Yamane、Takashi Yamanoguchi：“实时系统的演绎验证和自动演绎验证”日本信息处理学会研究报告MPS2000・29.5-8（2000）。

山根 智: "時間ステートチャートによる仕様記述と演繹的検証"電子情報通信学会技術研究報告(SS). 99・547. 33-40 (2000)

Satoshi Yamane：“使用时间状态图的规范描述和演绎验证”IEICE 技术报告 (SS) 33-40 (2000)。

山根 智: "ハイブリッドシステムの構成的証明とその計算機実験"電子情報通信学会研究報告. SS2001-49. 25-32 (2002)

Satoshi Yamane：“混合系统的构造性证明及其计算机实验”IEICE 研究报告 SS2001-49 (2002)。