限界正确性检查及相关模型检测技术

Model checking is an important approach for the verification of the correctness of software systems. The advantages of this approach include autmatic verification and that it can generate counterexamples when the verifiation fails. There are several types of model checking techniques: explicite state model checking, symbolic model checking and bounded model checking. Bounded model checking combines the advantages of symbolic models and local checking, and utilizes efficient tools developed for solving the propositional satisfiability. Initially, it aims at efficiently finding counterecamples, and is not effective for the problem instances that do not have counterecamples. In the recently years, in order use bounded models for the verification purposes, an extension of bounded model checking, called bounded correctness checking has been developed, and it is necessary to further study this approach for increasing it’s applicability. The aims of this project is to study bounded correctness checking in order to increase the applicability,and in combination with symbolic models and abstraction,to develop software tools for model checking, and to apply such an approch to program and system analysis.

模型检测是证明计算机软件系统正确性的一种重要方法。其优点在于自动化验证及对通不过验证的模型可以生成反例。模型检测方法可以分为几类：显式状态模型检测、符号模型检测，以及限界模型检测。限界模型检测结合了符号模型和可局部检测的优点，并可利用命题逻辑公式可满足性判定的高效工具。最初的限界模型检测方法本质上是一种快速寻找反例的方法，对不存在反例的验证实例难以奏效。近年提出的限界正确性检查是限界模型检测方法的扩展，其要点是在验证问题（相对于找反例问题）上也应用局部检查的理念，从而使得该方法可用于模型检测问题的快速验证和反例查找。目前限界正确性检查可应用的范围较小，因此有必要对该类方法进行深入的研究。本项目研究限界正确性检查及相关模型检测技术，分析限界正确性检查与符号模型检测的关系，研究限界正确性检查方法在更大范围的应用，结合模型的符号表示以及抽象原理等,发展模型检测工具，探讨其在程序分析等方面的应用。

项目以软件系统和计算机程序抽象模型的正确性验证方法为出发点，研究限界正确性检查方法及相关验证方法的关键技术、发展验证工具、探讨相关方法和工具在程序正确性分析验证方面的应用。项目在限界正确性检查方法与相关验证方法及关键技术方面，针对已有的限界正确性检查方法的效率问题，我们对ACTL性质的限界语义进行了改进并设计了改进的限界正确性检查算法，在我们的模型检测工具VERDS的基础上实现了该算法；针对多智能体的CTL时序算子和KEDC知识算子相结合的CTLK逻辑性质，我们提出了该逻辑的限界语义及其限界正确性检查方法，将该方法进行了实现；针对多智能体的CTL时序算子和BDI认识算子相结合的CTLBDI逻辑性质，我们提出了该逻辑的符号模型检测方法，将该方法进行了实现；针对逻辑公式可满足性问题，设计并实现了一种将模态逻辑S5公式转换为可满足性等价的SAT公式进行高效求解的算法。这些工作对所讨论的验证问题发展了新的验证方法或者改进了原有方法的效率。在探讨相关方法和工具在程序正确性分析验证方面的应用方面，针对程序推理分析的基本方法Hoare逻辑的相对完备性问题，基于断言的分类，细化了相对完备性的论述；针对并发系统的关于发散保持的互模拟语义问题，定义了一种可应用归纳原理进行验证的关于发散保持的弱互模拟语义，以更好地适用于并发系统的这种互模拟关系的验证；针对弱内存模型下的并发数据结构，证明了完全存储定序到完全存储定序可线性化问题是不可判定的；针对松散并发数据结构，提出了一种基于新的自动机的正则松散线性化，证明了正则松散线性化是可判定的而k-线性化在进程个数受限的情况下是不可判定的；这些工作提供了对所考虑的验证问题的进一步的理解和新的验证方法。