2001 Fiscal Year Final Research Report Summary
Design Support of Autonomous Distributed Systems by Integratig Temporal Logic, Concurrency Theny, Autom
| Project/Area Number |
11680360
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Kanazawa University (2001)
Kagoshima University (1999-2000) |
|---|
Principal Investigator |
YAMANE Satoshi Kanazawa Univ. Information Eng., Associate Prof., 工学部, 助教授 (70263506)
|
|---|
| Project Period (FY) |
1999 – 2001
|
| Keywords | open distributed systems / stepwise refinement / refinement verification / timed automata / hybrid models / Assume-Guarantee / receptioneness / specification |
|---|
| Research Abstract |
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.
|
