Research On Software Verification Technology Based On Model-Checking

Along with the software scale expand continually, thesoftware system are more and more complicated, and because of theabroad application of these systems in many fields such as:electron commerce, spaceflight communication and long-distancemedicine, all of these make that the system must have very highreliability, so how to ensure the correctness and the reliabilityhave became the most emergent problem in the software domain. Onthe one hand , the inherence uncertainty brought by the softwaresystem's expanding scale and its subsequent specialty,augmenting the difficulty and the expense of Verification thesystem reliability; On the other hand, for some programexploiting languages themselves have the unreliability ,such asthe c/c++ language doesn't examine the array boundary, it makesthat using traditional ways to remove the mistake in the softwaresystem is hard to satisfy the practice demands. The formalizationmethod is the important way to solve these problems. In manyformalization methods, the model checking as a kind of importantautomatization Verification technology have acquired hugesucceed in the hardware and protocol Verification domain,applying the model checking on the software Verification havebecome a hotspot in recent years, and have got some achievements.The text starts with the software error and the reason ofresulting in the error, analyzing and comparing severalmethods: debugging,checking and Verification to exclude thesoftware error, the text focus on studying the software'sformalization Verification and model Verification. The textreview the developing course of the model examine technology andthe study and application status of the technology in home andabroad, specially review the current study evolvement of themodel validate technology, and listing some typical model examinetools. The text continue discussing the basic concepts, mostlyideas of the model examine, specially discuss all kinds of methodsin the system and attributes modeling and some more typical modelexamine arithmetics.Protocol is a certain special software, the condition ofwhose state transferring has some comparability with ordinarysoftware,their process of Verification also on the whole similar,as a whole they both adopt system modeling,property expressionand model checking to structure themselves,so there are a certainextent currency between protocol Verification machine andsoftware machine. The author of this text and other schoolmatesof my issue group together study security protocol Verificationmachine:jlu _PV,there into myself mostly take on the exploitationand realization of analysis model,proposition formulaconstructing model and attack reappearance model. The jlu_PVadopt the similar method with international topping securityprotocol model checking machine SATMC,which is based on themethod of SAT. The result of experiment indicate that comparedwith SATMC,OFMC and CL-AtSe,jlu_PV can find the same attack,but fully precede SATMC in Verification speed ,and precedeanother two international topping security protocol modelchecking machines: OFMC and CL-AtSe in most problems. This textsets out from the common point of protocol Verification andsoftware Verification, at the same time it has consulted thechecking framework of jlu_PV and the method of model checkingbased on SAT , but it also bring forward new thought and new methodby contrasting the difference between them.Based on further studying thorough the model examine theoryand summarizing the experiences of realizing the protocolVerification machine jlu_PV, the text study and design a softwareVerification machine Jlu_SV prototype system based on modelchecking, and on the time-admission situation the text achievesome parts. The prototype system found the basis softwareVerification framework, translate the source codes into themiddle codes described by language C set--CL-Subset that aredesigned by myself using program code translating module, afteroptimizing and slicing the codes using the program analysis model,validate it using the model checking methods based on SAT, createthe proposition layer ,the motion layer and found the propositionformula based on the alters of the variation value in the basisprogram block, then transform the generate proposition formulato combine formula need by SAT solving implement, and give it tothe SAT solving implement, at last analysis and explain the solveresults.The primary difficulty points and innovation points ofsoftware Verification machine Slave_ ca in the text lie in:1,Based on the basic sentences of c language, Create the setof sentences: CL-Subset,take c language for example and providetransform methods of translating c programs into CL- Subse codes.For software Verification, what we care for is the alters of thevariables when the software is running, not the language that beused to implement the alter. So we classify the source codes andunify the forms, transform them into the codes which only includeinput,evaluation,offset,cycle and transfer sentences. On theone hand, it can exclude the influence to software Verificationof the sentences variety, and mostly simple our furtherexamination to the variables in the software, on the other hand,on different platforms, the source codes written with variouslanguages, can be translated into the CL-Subset code above withdifferent code-switching module. This improves the currency ofsoftware Verification manner.2,Apply the program analyzing techniques to optimizeCL-Subse codes, analyze program controlling structure. Theprogram analyzing techniques take program as object to be dealwith, according to the requirements carry through variousanalysis. It have important application in programunderstanding,program checking,program optimization,programreconstructing and so on. We apply the techniques such as bynameanalysis,information stream analysis,program slice and so onoptimize the controlling structure of the CL-Subsetcode-switching and analysis program so as to examine theconditions of how variables get values.3,Currently the development in SAT solver mostly improvesthe time and space efficiency of the model Verification methods.Making use of SAT solver to carry through model checking has beena hotspot. The text uses the technique of carrying throughabstract and attribute Verification to software. SoftwareVerification process take the conditions of how the variable getvalues when running software as system states, take the changesof it as state transition, express the Verification objectivesas Boolean expressions which satisfy Verification attributes andare abstracted by evaluation sentences, take the createdproposition formulas as objective state, start off from thebeginning state, judge if it can arrive at the objective stateto represent if the program can satisfy Verification attributes.Presently, software model Verification still lie in aunderway period, international studies about correlative theoryhave gradually started. Though some software analyzing andVerification tools have been developed and especially somecorporations such as Micro Software begin to use these tools soas to ensure the quality of software development, intotal ,however ,it need to do many works that the technique tendto real mature. Especially in our country, the studies of softwaremodel Verification haven't fully opened out. Though some expertsare committing themselves to study model checking techniques andapply them to the field of software model Verification, matureframe of software model Verification and tools which can beapplied to software model Verification haven't came out yet.As a part of the model checking group of computer institutein JILIN University, the text puts the hard basis for broader andfurther studies and analysis of software model Verification infuture. The study in the text plays vital function in how to ensurethe correctness and dependability of the software and how toimprove the quality of the software. There are broad developmentoutlooks and further study values.