1994 Fiscal Year Final Research Report Summary
Research on Formal Verification of Finite State Systems
| Project/Area Number |
05680285
|
|---|
| Research Category |
Grant-in-Aid for General Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Kyoto Sangyo University |
|---|
Principal Investigator |
HIRAISHI Hiromi Kyoto Sangyo Univ., Engineering, Professor, 工学部, 教授 (40093299)
|
|---|
| Project Period (FY) |
1993 – 1994
|
| Keywords | Formal Design Verification / Finite State Systems / Temporal Logic / Symbolic Model Checking / Logic Design Verification |
|---|
| Research Abstract |
Aiming at establishment of fundamental formal verification methodology for finite state systems of practical size, I mainly investigated formal design verification based on symbolic model checking of temporal logic. The major results of this research are summarized below :
1.Symbolic Model Checking Algorithm : Since an inverse image computation is one of the basic operations in symbolic model checking of temporal logic, I proposed an efficient new inverse image computation algorithm. The proposed algorithm was applied to a verification of 8 bit microprocessor, and the result showed that the new algorithm achieved around 60 times speed-up compared with conventional inverse image computation algorithms.
2.Time-Space Modal Logic : Aiming at verification of bit-slice architecture, I proposed a new transition system that has tow types of transition ; one for time transitions and the others for space transitions. The transition system cab be used as a model of a bit-slice circuits. As for a specification language on the transition system, I proposed time-space modal logic and showed its symbolic model checking algorithm.
3.Verification of Real-Time Systems : As for basic algorithms in verification of real-time systems, a couple of symbolic algorithms have been proposed. By using these algorithms, we can obtain upper bound and lower bound of time between two types of events and upper bound and lower bound of event occurrences in a given time period. These are basic characteristics of real-time systems and calculations of them are important in verification of real-time systems.
4.Formal Verification of 16 bit microprocessor : Various abstract methods were investigated to make verification of 16 bit microprocessor possible. Among them, abstraction of data width to 8 bit and signal fixing were very effective. By combining these two methods, we succeeded to verify 16 bit microprocessor.
|
