Static Code Analysis Method Based on Fault Mode and Model Check
Ruan Yuan · Jisuanji gongcheng · 2012
In order to improve the procedure accuracy and reduce software development and maintenance costs,this paper proposes a static code analysis method based on fault mode and model check.Common C program fault modes are described as CTL formulas form,and an extendable CTL formula library is established.Control Flow Graph(CFG) is generated from testing procedure,and then converted into an equivalent Kripke structure.Labeling algorithm is used to realize model check,so that the procedure can be checked whether it is correct.Experiments based on CoSy compiler platform indicate that the method can correctly find out the fault modes in procedure with good scalability.