| Project/Area Number |
13558031
|
|---|
| 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, Department of Philosophy, Professor, 文学部, 教授 (30224025)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
NAKAGAWA Wataru SRA, Senior Researcher, ソフトウェア工学研究所, 部長
TAMURA Naoyuki Kobe University, Department of Computer and Systems Engineering, Professor, 工学部, 教授 (60207248)
FUTATSUGI Kokichi JAIST, Department of Information Systems, Professor, 情報科学研究科, 教授 (50251971)
|
|---|
| Project Period (FY) |
2001 – 2003
|
| Project Status |
Completed (Fiscal Year 2003)
|
| Budget Amount *help |
¥6,700,000 (Direct Cost: ¥6,700,000)
Fiscal Year 2003: ¥1,900,000 (Direct Cost: ¥1,900,000)
Fiscal Year 2002: ¥2,000,000 (Direct Cost: ¥2,000,000)
Fiscal Year 2001: ¥2,800,000 (Direct Cost: ¥2,800,000)
|
|---|
| Keywords | Real Time Systems / Formal Specification / Formal Verification / Linear Logic / Proof Search / 証明論 |
|---|
| Research Abstract |
We developed and designed a formal specification and verification tool for dynamic real-time systems in the collaboration with the French partner group (Jean-Pierre Jouannaud's group), based on linear logic. By dynamic real-time systems we mean a multi-agent systems in which the number of participating agents may be changed and the time constraints may be changed dynamically We gave an automated transformation procedure to transform a natural specification on the user-level into a linear logical specification. We also gave an elimination procedure to eliminate the dense time notions from a linear logical specification. Then, various kinds of verifications are performed in terms of the proof-search mechanism of a fragment of linear logic. The dense time elimination procedure is given by a program extraction method known in constructive logic. We also developed a logical framework for the security protocol correctness proofs, applying the same concept. We also studied some related logical research on our linear logic, which is the logical framework of our verification tool.
|
