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