基于抽象的软件符号模型检测研究

项目名称： 基于抽象的软件符号模型检测研究

项目编号： No.61170043

项目类型： 面上项目

立项/批准年度： 2012

项目学科： 计算机科学学科

项目作者： 魏欧

作者单位： 南京航空航天大学

项目金额： 56万元

中文摘要： 软件模型检测的主要瓶颈之一是状态爆炸问题，基于抽象的符号模型检测是克服该问题的一个重要途径。近年来关于支持证实与证伪的抽象研究提供了验证系统正确性和错误的统一框架，避免了传统的自上或自下近似的局限性。但在与符号模型检测结合上，现有的方法存在着精度不高，导致过多求精迭代过程等关键问题。本项目旨在提出新的方法，通过综合支持证实与证伪抽象的交互迁移系统(MixTS)和超迁移系统(HTS)这两类模型的优点，解决现有的支持证实与证伪的抽象软件符号模型检测中的问题。主要的研究内容和目标为1)在MixTS上定义一种新的时序逻辑的归纳语义，使其具有HTS上的最优抽象精度；2）为该语义提供符号模型检测算法，以综合MixTS的有效符号表示和HTS的分析精度；3）设计在新的符号模型检测中产生反例和求精的方法，克服HTS中树形反例难以理解和分析的障碍；4）将上述结果用于动态构造软件抽象模型技术，提高软件验证效率。

中文关键词： 抽象方法；模型检测；多值模型；形式化验证；

英文摘要：

英文关键词： Abstraction；Model Checking；Multi-valued Models；Formal Verification；