基于形式化规约的缺陷规则库构建与检测方法

摘要：

传统的源码缺陷分析方法存在缺陷规则有限，缺陷检测结果不明确等问题。以模型检测中的形式化规约为基础，提出一种积木式缺陷规则库构建和源码检测方法。利用元数据，用户能够通过简单的CTL逻辑操作，实现自定义待检测的缺陷种类。并且，在检测到缺陷后能返回带有源程序行信息的反例路径，帮助开发人员快速定位缺陷根源。作为系统核心部分，规则库引擎从源程序中抽取控制流结构，进行符合控制反向（IOC）机制的元数据的动态匹配与标记。采用时序逻辑规约和标记后的控制流结构对程序建模，并结合NuSMV模型验证器实现验证。实现了原型系统，通过对开源程序的检测说明了该方法的有效性。

关键词：积木式模式、形式化规约、模型检测

分类号：TP31(计算技术、计算机技术)

资助基金：优秀青年教师科技支撑专项No.YX2011-29；国家自然科学基金No.61170268。

在线出版日期：2014-07-23（万方平台首次上网日期，不代表论文的发表时间）

页数：共8页

页码：66-72,102