2002 Fiscal Year Final Research Report Summary
Theory of formal specification and verification of concurrency systems and real-time systems based on linear logic
| Project/Area Number |
12480075
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Keio University |
|---|
Principal Investigator |
OKADA Mitsuhiro Keio University, Faculty of Letters, Professor, 文学部, 教授 (30224025)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
KOBAYASHI Naoki Tokyo Institute of Technology, Graduate School of Information Science and Engineering, Associate Professor, 大学院・情報理工学研究所, 助教授 (00262155)
|
|---|
| Project Period (FY) |
2000 – 2002
|
| Keywords | Linear Logic / Formal Verifieation / Formal Specification / Real-Time System |
|---|
| Research Abstract |
We gave a logical method for formal specification and formal verification of concurrent systems, in particular real-time concurrent systems, which contains quantified time constraints in the dense-time setting.
In the first half of the project we gave a concrete algorithm for verification of the basic safety and other related properties (the membership property, the appointment property, the liveness property, etc.) in the dense real-time setting. We also gave a theory of automated transformation from a specification (written in the framework of natural description language) into a linear logical specification.
Then in the second half of the project we extended our theories to dynamic real-time systems where the number of agents/participants and the form of time-constraints are dynamically changed. We also compared our linear logical method with the traditional model checking and the timed automata method.
|
