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

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

软件模型检测的主要瓶颈之一是状态爆炸问题；基于抽象的符号模型检测是克服该问题的一个重要途径。项目以支持证实和证伪的抽象模型为基础，从特定的对应于四值模型的交互迁移系统(MixTS)/超迁移系统(HTS)扩展到通用的多值模型，结合软件产品线的分析与验证，提出有效的软件系统抽象模型构造、符号模型检测及反例分析方法，提高模型检测的效率和应用范围。主要研究内容和结果包括：（1）以抽象解释理论为基础，给出对抽象模型进行分析的统一框架，包括抽象模型的逼近关系、抽象语义精度、最优模型的结构定义条件、抽象局限性以及完备性等问题。（2）以交互迁移系统的互模拟关系为基础，改进了现有的多值模型互模拟关系的理论结果，提出最通用的描述多值模型抽象逼近的交互互模拟关系，能够刻画任意多值模型上的命题时序逻辑语义，使得可以在更大的范围内选取有效的抽象模型。（3）定义了多值模型的自同构置换群，根据所提出的多值模型交互互模拟关系，将对称化简的抽象方法扩展到多值模型上。（4）将多值逻辑用于软件产品线的特征迁移系统模型，提出对于包含不确定信息的软件系统的建模方法，实现了对软件产品线的多值符号模型检测。（5）对于特征迁移系统，提出了基于特征切片的抽象方法，根据特征依赖集和排斥集，采用多值模型作为抽象模型，利用多值符号化模型检测工具进行有效验证。（6）将多值模型检测应用于系统安全性分析，定义系统故障组合与模型检测反例的对应关系，提出根据软件产品线符号模型检测产生的特征组合反例进行安全性分析的方法。