论文研究基于形式化规约的缺陷规则库构建与检测方法.pdf

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