权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Research on Formal Verification of Finite State Systems

有限状态系统的形式化验证研究

基本信息

批准号：
05680285
负责人：
HIRAISHI Hiromi
金额：
$ 1.34万
依托单位：
Kyoto Sangyo University
依托单位国家：
日本
项目类别：
Grant-in-Aid for General Scientific Research (C)
财政年份：
1993
资助国家：
日本
起止时间：
1993 至 1994
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-05680285/
关键词：
Formal Design Verification Finite State Systems Temporal Logic Symbolic Model Checking Logic Design Verification 設計検証形式的検証分散アルゴリズム抽象化

项目摘要

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.

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