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

在这项研究中，我们通过整合现有的形式化方法，实现了我们新的分布式系统设计支持系统。我们通过实时模型或混合模型将分布式系统形式化为开放的分布式系统，并通过自动或演绎的方法对其进行验证。提出了以下四种方法：(1)基于假设-守护者方法的实时开放分布式系统的自动化设计支持：开发了开放时间自动机，并以假设-保证方式实现了对时间仿真关系和接受性的自动验证。实时开放分布式系统的演绎设计支持：开发了带时间的状态图，实现了演绎精化验证方法。基于假设保证方法的实时开放分布式系统的演绎设计支持：开发了时钟转换模块，实现了基于假设保证方法的演绎求精验证方法和接受性验证方法。混合开放分布式系统的演绎设计支持：开发了相变模块，实现了演绎精化的方法。使用这种方法，我们可以开发基于逐步求精的控制律表示的分布式系统。我们现在正在用定理证明器实现我们所提出的方法，并将其应用于大系统。

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.