Research on Formal Verification of Finite State Systems
Project/Area Number  05680285 
Research Category 
GrantinAid for Scientific Research (C).

Research Field 
計算機科学

Research Institution  Kyoto Sangyo University 
Principal Investigator 
HIRAISHI Hiromi Kyoto Sangyo Univ., Engineering, Professor, 工学部, 教授 (40093299)

Project Fiscal Year 
1993 – 1994

Project Status 
Completed(Fiscal Year 1994)

Budget Amount *help 
¥2,100,000 (Direct Cost : ¥2,100,000)
Fiscal Year 1994 : ¥800,000 (Direct Cost : ¥800,000)
Fiscal Year 1993 : ¥1,300,000 (Direct Cost : ¥1,300,000)

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 speedup compared with conventional inverse image computation algorithms. 2.TimeSpace Modal Logic : Aiming at verification of bitslice 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 bitslice circuits. As for a specification language on the transition system, I proposed timespace modal logic and showed its symbolic model checking algorithm. 3.Verification of RealTime Systems : As for basic algorithms in verification of realtime 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 realtime systems and calculations of them are important in verification of realtime 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.

Report
(4results)
Research Output
(17results)