| 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
|
| Project Status |
Completed (Fiscal Year 2001)
|
| Budget Amount *help |
¥1,200,000 (Direct Cost: ¥1,200,000)
Fiscal Year 2001: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 2000: ¥500,000 (Direct Cost: ¥500,000)
|
|---|
| Keywords | open distributed systems / stepwise refinement / refinement verification / timed automata / hybrid models / Assume-Guarantee / receptioneness / specification / 分散システム / 開放型システム / 実時間処理 / 計算機支援 / 時相論理 / 演繹的検証 / リアルタイム性 / receptive |
|---|
| 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.
|
