关键词: 积木式模式, 形式化规约, 模型检测

Abstract: 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.

Key words: toy-brick pattern, formal specification, model checking