1997 Fiscal Year Final Research Report Summary
Research on Specification and Verification of real-time software
| Project/Area Number |
07680341
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
YONEZAKI Naoki Tokyo Institute of Technology Graduate School of Information Science and Technology, Professor, 大学院・情報理工学研究科, 教授 (00126286)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
TOMOISHI Masahiko Tokyo Institute of Technology Graduate School of Information Science and Technol, 大学院・情報理工学研究科, 助手 (60262284)
|
|---|
| Project Period (FY) |
1995 – 1997
|
| Keywords | Real-time Software / Secification / Verification / Temporal Logic / Real-time Logic / Linear Logic / Relevant Logic |
|---|
| Research Abstract |
It became crucial issue to build correct software with real time feature for safe critical systems e.g.embedded software in control systems. In order to make these software safer and securer, we need a new software construction method based on verification technique. In this research project we had the following results.
1) Proof systems of temporal logic for various time domains
First we developed connection calculus for temporal logic with discrete time domain. To prove the validity of a formula in discrete frames, we have to check the unsatisfiability for infinite frames. This means that we need substituion for infinite length of modal operators in connection calculus. In our approach we allows self substitution for modal operators so that we can solve the problem.
Then next we studied axiomatic systems for a temporal logic with real number timed domain. We showed that it is neither possible to construct complete axiomatic system nor to give decision procedure for the validity of a formula. We restricted it to rational domain where the number of the charge of state is bounded, as a result we had decidable logic.
2) Various aspects of software verification
2-1) Differential verification method for temporal specification
We developed new tableau method for differential verification, where the verification result for the previous specification is reused with the difference between a new specification and the previous one.
2-2) Level of realizabilities of a specification and its decision procedure
We defined several concepts approaching realizability. The classification of specifications based on these concepts gives us useful information for making a specification realizable. We gave the decision procedure for the membership of the classes and also we had an idea to identify a set of the parts of the specification which is the cause of un-realizability.
|
