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

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

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.