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

点击翻译按钮获取中文摘要

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.