| 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)
米崎 直樹 東京工業大学, 大学院・情報理工学研究科, 教授 (00126286)
林 晋 神戸大学, 工学部・情報知能工学科, 教授 (40156443)
|
|---|
| Project Period (FY) |
2000 – 2002
|
| Project Status |
Completed (Fiscal Year 2002)
|
| Budget Amount *help |
¥7,500,000 (Direct Cost: ¥7,500,000)
Fiscal Year 2002: ¥2,300,000 (Direct Cost: ¥2,300,000)
Fiscal Year 2001: ¥2,200,000 (Direct Cost: ¥2,200,000)
Fiscal Year 2000: ¥3,000,000 (Direct Cost: ¥3,000,000)
|
|---|
| 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.
|
