Research on Formal Verification of Finite State Systems

为了建立实际规模有限状态系统的基本形式化验证方法，本文主要研究了基于时态逻辑符号模型检测的形式化设计验证。1.符号模型检测算法：由于逆图像计算是时态逻辑符号模型检测的基本运算之一，本文提出了一种新的高效的逆图像计算算法。将该算法应用于8位微处理器的验证，结果表明，与传统的逆图像计算算法相比，新算法的速度提高了约60倍。2.时空模式逻辑：针对位片结构的验证，提出了一种新的转换系统，它有两种转换类型：一种用于时间转换，另一种用于空间转换。该转换系统可以作为位片电路的模型。对于转换系统的描述语言，提出了时空模态逻辑，并给出了其符号模型检验算法。3.实时系统的验证：对于实时系统验证的基本算法，提出了几种符号算法。通过使用这些算法，我们可以得到两类事件之间的时间上界和下界，以及给定时间段内事件发生的上界和下界。这些都是实时系统的基本特征，它们的计算在实时系统的验证中是非常重要的。4.16位微处理器的形式化验证：为了使16位微处理器的验证成为可能，研究了各种抽象方法。其中，数据宽度提取到8位和信号固定是非常有效的。通过这两种方法的结合，我们成功地验证了16位微处理器。

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.