Application Of Model Checking To Software

Critical infrastructures in several domains, such as medicine, power,telecommunications, transportation and finance are highly dependent oncomputers. Disruption or malfunction of services due to software failures(accidental or malicious) can have catastrophic effects, including loss ofhuman life, disruption of commercial activities, and huge financial losses.The increased reliance of critical services on software infrastructure and thedire consequences of software failures have high-lighted the importance ofsoftware reliability, and motivated systematic approaches for assertingsoftware correctness. While testing is very successful for finding simple,relatively shallow errors, testing cannot guarantee that a program conformsto its specification. Consequently, testing by itself is inadequate for criticalapplicationsandneedstobecomplementedbyautomatedverification.Model checking technology which is a formal verification technologyfor concurrent systems with limited states has a historyabout 30 years. It isproposed in order to overcome the disadvantage of simulation and theoremproving in verification. Recently, it has achieved tremendous success inhardware and protocol verification domain. Model checking software hasbecomeahottopicinrecentyears,andhasachievedsomesuccess.Because of involving the computation in infinite domain, softwareoften contains infinite states. Model checking is technology which oftentakes an exhaustive search in a limited state space, thus how to map infinitestates to a finite state set is very important. Abstraction technology canremove the unconcerned details in order to reduce the scale of the checkedsystem. It may be the most important technology for model checking. Thispaper analyses the common abstract technology, such as state merging, dataabstraction, and predicate abstraction. At the end of this paper, we describe a different abstraction technology according to the knowledge we master,andalso refertosomeothermodel checkingtools. It canabstract thesourcecode to formula, and then we can use SAT based technology to finishchecking.Many of the existing software, partly due to the performancerequirements, are written in low level language such ANSI-C. C languageitself contains some unsafe features, for example, it doesn't examine thearrayboundary.InthisarticlewechoosetheClanguageasaresearchobject,and tryto transform the C source code to a formula. Finally, it can use SATtechnology to solve the satisfiability of this formula, so as to determinewhether the current system meets the required properties. This paperdescribestheabstractionprocessofsourcecodewritteninClanguage.Firstly, the various statements of C language will be transformed into afew types of statements in order to deal with them simply. For morecomplicated assignments, such as containing side effects, we split them intoseveral simple assignments by introducing temporary variables. Loopconstructswillbeunwoundusingmultipleifstatements.Functioncallwillbeexpanded. The final program only contains a simple procedure, and onlycontains if statements, assignments, assertions, and goto instructions. It canreduce the influence of the diversity of statements to software checking, andthe process also can be extended to handle other languages. In this process,variable renaming is very important to ensure that the result program isequivalenttooriginalprogram.Secondly, program may include some redundant statements, as they donot affect the satisfiability of the properties we want to check. We haveintroduced program analysis technology, especially chip technology, toremove unwanted statements, simplify procedures structure, and reduce thestate space. Software verification process uses the values of variables as thesystem states. The change of variable values will be used to representtransitionrelations.Thispaperdescribeshowtoabstractthesestatementsinto formula including pointer handling, and then also present several inspectionmethods.Compared to some other static source code detection tools, this paperattempts to use model checkingtechnologyto detect the emergences of somecommon mistakes in source code. First of all, model checking is a formalverification technology, if the verification process terminates normally andreports the program is correct, there are no errors we need to check. Inaddition,whenthepropertiesarenotsatisfied,modelcheckingwillreportsananti-path, which is very convenient for programmers to trace and debugerrors in the code. However, due to lack of time, we only support just a fewpropertiesandtheprocedureonlycandetectcodeinverylimitedscale.Allofthese need further research to expand more properties and improve newabstracttechnologytoimprovethecapabilitiesofsoftwaremodelchecking.Presently, software model checking is still at the fledgling stage, someinternational communities graduallybegin tostudyits theory.Althoughsomesoftware analyzing and verification tools have been developed, in particular,Microsoft and other companies have began to use these tools to ensure thequality of software development, it needs to do more works before it can beused in the real software engineering. Particularly, the research of softwaremodel checking has not been fully under way in our country. Though someexperts dedicate themselves to the research of this technology, ripe softwaremodelcheckingtoolshavenotyetappeared.