符号模型与隐式状态模型检测技术

The correctness and reliability of software systems is an important problem. For combating this problem, the research on program properties and their verification methods has received great attention in the comoputer science community. One type of the verification methods is model checking. One weakness of the traditional explicite state model checking is that the number of the reachable states of given systems may be too large. For combating this problem, implicite state model checking uses logic formulas for representation of sets of states. The basis for this kind of approach is symbolic models and the traditional implicite state model checking approach is called symbolic model checking. The basic approach of symbolic model checking relies on a kind of global algorithms. In the recent years, it has been developed an approach called bounded model checking, that combines the advantages of symbolic models and local checking, and utilizes efficient tools developed for solving the propositional satisfiability. However, the worst case computational complexity of bounded model checking is high. Therefore it is necessary to do further reaseach on the kind of aforementioned methods. This project is on symbolic models and implicite state model checking methods and related key technologies, aiming at studying the symbolic representation of models and basic principles of bounded model checking approaches, and in addtion, studying abstraction and compositional techniques, and combine these methods with reasoning methods for increasing the applicability of implicite state model checking. On the basis of the above research effort, we will develop model checking tools and try to apply such tools in different areas including analysis of comptuer programs and electronic curcuits.

计算机软件系统的正确可靠是一个重要问题。针对这个问题，程序的性质及其验证方法的研究得到广泛重视。一类程序性质验证的方法为模型检测。传统的显式状态模型检测的不足在于系统可达状态的数目可能过于庞大。隐式状态模型检测用逻辑公式表示状态集合以试图弥补这个不足。隐式状态模型检测的基础是符号模型，其传统的方法称为符号模型检测。符号模型检测的基本算法是一种全局性算法。近年来发展起来的限界模型检测方法，结合了符号模型和可局部检测的优点，并可利用命题逻辑公式可满足性判定的高效工具。但限界模型检测最坏情况下计算复杂性高。因此有必要对该类方法进行深入的研究。本项目研究符号模型与为隐式状态模型检测方法及关键技术，旨在研究模型的符号表示和限界模型检测方法的基本原理，并研究抽象和组合技术，以及以上方法和推理方法的结合以提高隐式状态模型检测的适用范围，在此基础上发展模型检测工具，探讨其在程序分析和电路分析等方面的应用。

项目针对程序正确性及其验证方法，研究符号模型与隐式状态模型检测技术。根据项目任务书，项目的研究内容围绕符号模型与隐式状态模型检测技术，并研究以上方法和推理方法的结合以提高模型检测的适用范围，发展模型检测工具，探讨其在程序分析等方面的应用。项目的主要研究进展包括如下3个方面。在符号模型与模型检测理论方面，我们研究了有限状态模型及其时序逻辑性质的命题逻辑公式及量词命题逻辑公式表示，使得我们可以应用命题逻辑可满足性求解工具验证有限状态模型的时序逻辑性质。我们提出了计算树逻辑CTL及其称为eCTL的扩展的限界语义以及基于该语义的限界正确性检查方法，并在我们的工具VERDS上实现了该方法。限界正确性检查方法是限界模型检测思想的发展，突破了限界模型检测相对于传统符号模型检测仅在查错方面具有互补性的局限，实验数据显示限界正确性检查与传统符号模型检测不论是在验证还是在查错方面都具有互补性。与传统符号模型检测工具NuSMV相比较，VERDS所实现的限界正确性检查方法除了与NuSMV能够在以上意义下具有互补性外，在我们的限界语义框架下，还具备验证较为复杂的eCTL性质的功能。由于模型检测的效率和适用性受限于系统规模，在试图扩展模型检测的应用范围和提高对有关推理方法的认识方面，我们对推理验证方法和无穷状态系统验证方法进行了研究，对一些重要问题提高了认识、发展了相关方法和技术，特别需要指出的是我们在HOARE逻辑的完备性问题，下推多主题系统的模型检测问题，多核处理器的存储一致性模型的验证方面获得了新的成果。在模型检测技术和工具的应用方面，我们实现了一个存储一致性模型验证工具MODV并利用该工具验证Godson-T多核处理器的存储一致性模型；我们对SystemC设计的验证方法进行了研究，为SystemC子集提出了一个可执行语义，实现了该子集的SystemC设计到卫迁移系统模型的转换工具，使得我们可以应用VERDS验证SystemC设计，并在该基础上，我们结合偏序归约方法以验证SystemC设计以提高基于模型检测工具VERDS的SystemC设计的验证效率。