Static Defect Inspection Of Java Source Code Based On Model Checking

The rapid development of information industry has put forward higher requirements on the reliability of the software. As a kind of program analysis techniques which do not perform test on itself, the objective of static program analysis is to verify whether the code meets the specified testing standards, it helps to find code defects early in the project. Traditional static defects has limited defect rules and the defect detection result is not quite clear. In this paper, through researching on the principle and related technologies of formal static analysis, we present source code static analysis methods based on model checking.Taking Java as example, we define defect pattern according to grammatical features and abstracting CTL representation from defect pattern to customize the toy-brick pattern defects set. By making use of metadata, users can customize types of defect rules to detect and achieve the semi-automated extension of the defect set. 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, verification 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. Realize the prototype system and combined with testing result of open source code. It shows that the proposed method can be applied practically and effectively on Java programs’ static defect analysis, while achieving defect the semi-automatic expansion and interactive counterexample result output.