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

Approach of constructing defect rule base and detecting source code based on formal specification

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

There exist the problems of insufficient number of defect rules and of unclear detecting results in traditional source-code defect-analysis techniques. A toy-brick pattern defect base construction method and source code detecting method are proposed, based upon formal specification. By making use of metadata, users can customize types of defect rules to detect. Furthermore, counterexamples carrying line information of the source code are returned, thus helping program developers to quickly locate the defect roots. As a key part, rule base engine is introduced, which extracts control flow from source code and dynamically matches and labels the meta data according to Inversion of Control（IOC）mechanism. The object program is modeled with temporal logic specification and labeled control flow, and NuSMV is utilized to realize verification. A prototype is implemented, and detecting results on open source programs show that the methods are effective.