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

项目名称： 符号模型与隐式状态模型检测技术

项目编号： No.61272135

项目类型： 面上项目

立项/批准年度： 2013

项目学科： 自动化技术、计算机技术

项目作者： 张文辉

作者单位： 中国科学院软件研究所

项目金额： 82万元

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

中文关键词： 模型检测；时序逻辑；程序正确性；符号模型；

英文摘要： 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 symbol

英文关键词： Model Checking；temporal logics；program correctness；symbolic models；