Research On Model Checking Based Software Analysis

The use of computers is becoming increasingly popular,so people relied on computers more and more seriously.Computer hardware has been under researched for a long time,so testing methods are rich,mature,and their safety level is much higher than the safety of the computer software.At the same time,the popularization of information technology enhance people's dependence on software,people required better quality of the software.How to improve software quality has become the focus of the study.Traditional software testing methods can point out that the software has flaws,but can not prove the correctness of software.Formal methods can prove the correctness and safety of software systems.Model checking,being high-performance and automation,becomes a research hotspot.Since it's born,lots of techniques and theories are proposed in Model checking domain.With Applying successfully in hardware and protocols development,people focus on software systems now.The steps of usage of model checking can be divided to:translating the system to abstract model,describing the system property using certain system language,checking that if the model satisfies the properties.Now,the basic research has been focusing on:1) how to increase the scope of model checking can apply;2) How to disciple system property more convenient and flexibly.3) How to improve the efficiency of the model checking.The state explosion problem is the bottleneck of model checking tools in the software system.This paper presents a model checking-based software analysis method.The method combines information flow analysis technology,uses CTL language to describe system properties and model checker tool NuSMV to check the system.This method can determine that whether a given C/C + + source code meets our pre-defined properties. These properties include:1) not existing uninitialized variable;2) malloc and free should match;3) not existing unused variable;4) not existing wild pointer.Using the model checker NuSMV,combined with model checking technique and software analysis technique,analysis the software properties.The main works include the following:1.Translating control flow chart to the equivalent Kripke structure,using this Kripke structure as the abstract model for model checking.This method simplified modeling work. 2.Expanding the concepts of abstract syntax tree and control flow chart,designing rules for translating control flow chart to equivalent Kripke structure,proving the equivalence of Kripke control flow chart and source code.3.Developed rules for translating abstract model and description of CTL formula into the input of model checker NuSMV.