Research on a Software Verification Method at Source Program Level
Software quality have deep influence on all walks of life that use software,so verifying if a software meets the required properties has become a key issue. A verification method at source program level based on C program is proposed in this paper. The main idea of the method is to translate C source program into Kripke structure that is equivalent to control flow graph,use the Kripke structure as an abstract model of the program,describe desired program properties in CTL formula,and use model checker NuSMV to verify the model so as to verify w hether the program satisfies the properties. Based on this idea,an environment prototype is designed and implemented that automatically translates C source program and properties into the NuSMV input file to verify it.