论文部分内容阅读
软件已经成为国防建设与国计民生的重要组成部分,如何提高软件的正确性、可靠性和安全性是计算机软件领域面临的重要挑战。Clarke等人提出的模型检测方法被认为是迄今为止应对这一挑战的最具潜力的方法之一。模型检测方法已经成功用于对计算机软件系统的验证中,但仍存在一些不足:(1)软件模型难以提取;(2)性质描述语言的表达能力不足,部分程序性质无法描述;(3)模型和性质不在同一体系;(4)状态空间爆炸问题。为了解决模型检测中存在的问题,本文对现有的模型检测方法和动态符号执行方法进行研究,将动态符号执行技术应用于模型检测领域,给出了一种新的模型检测方法。本文的主要贡献包含以下三点。1.研究了建模、仿真和验证语言(Modeling,Simulation and Verification Language,MSVL)与命题投影时序逻辑(Propositional Projection Temporal Logic,PPTL)的语法结构、基本语义和范式理论,提出了基于动态符号执行的MSVL程序模型检测理论和方法,从四个方面来应对模型检测中存在四个问题。(1)通过MSVL程序的动态符号执行获取程序的符号执行树作为模型,利用程序执行的方式避免了程序模型提取的困难。(2)利用PPTL描述待验证的系统性质,由于PPTL的表达能力等价于完全正则语言,克服了性质描述语言表达能力不足的问题。(3)MSVL和PPTL同属投影时序逻辑(Projection Temporal Logic,PTL)系统,模型和性质在同一体系,不需要进行额外转换,验证效率高。(4)MSVL程序动态符号执行得到的符号执行树是一个抽象模型,该模型的一条路径代表了满足路径约束的所有输入对应的执行路径。这种对模型的抽象方式能够显著地压缩程序模型的状态数,有效地缓解了状态空间爆炸问题。2.基于现有的MSVL解释器,设计了基于动态符号执行的MSVL程序模型检测工具的基本框架,给出了该模型检测工具的三个主要模块的设计与实现方案,最后利用C++编程实现了该模型检测工具。3.通过“空调控制器”和“自动门控制系统”这两个实例验证了基于动态符号执行的MSVL程序模型检测工具的正确性和可用性。