基于模型检测的软件可靠性验证方法

摘要

随着信息技术的快速发展，计算机软件的应用领域不断扩大，其功能和规模也日益复杂。这些软件系统运行时如果出现故障，将造成不可估量的损失。如何有效保证软件系统的可靠性，成为一个十分紧迫而且严峻的问题。模型检测作为一种重要的形式化验证技术，已逐渐应用于软件可靠性验证中。本课题基于模型检测技术，重点针对复杂软件建模困难、状态空间爆炸等实际问题，对软件可靠性验证方法展开研究。
　　首先，将模型检测技术用于软件系统设计阶段。提出了一种基于状态变迁矩阵的软件设计建模方法，阐述了其形式化定义和动态行为描述方法。并引入时间和概率因子对状态变迁矩阵模型进行扩展，以解决具有实时特性和随机行为特性的复杂软件系统建模困难问题。基于扩展的时间状态变迁矩阵模型，提出了实时软件设计验证的符号化编码方法和性质描述方法，并采用限界模型检测技术和可满足性模理论进行设计规范验证。实验结果证明了该方法在软件设计可靠性验证方面的有效性。
　　其次，将模型检测技术用于代码开发阶段。提出了一种基于程序骨架的软件源代码抽象方法与性质验证加速方法。通过对程序源代码进行合理剪枝和循环路径压缩，提取软件源代码的程序骨架。利用Hoare逻辑研究了循环节点不变式求解方法，用不变式替代复杂的循环结构，大大缩短了程序路径编码公式长度，在一定程度上缓解状态空间爆炸问题。最后通过设计对比实验，证明了基于程序骨架的方法能够显著提高软件源代码可靠性验证效率。