【作者】 黎吾平；

【导师】 欧阳丹彤；

【作者基本信息】 吉林大学 ， 计算机软件与理论， 2008， 硕士

【摘要】 模型检测技术是一种自动化的检测技术,该技术广泛应用于时序电路设计和通信协议设计,并取得了很大的成绩。真正将模型检测技术引入到软件的验证只有短短的几年历史,该技术目前正处于研究阶段。本文在实验室研究成果的基础上,首先探讨了模型检测的主要思想、发展变革及最新的研究热点,重点阐述了软件模型检测的特点。最后给出对于软件源代码进行建模的过程和算法,详细阐述了几个属性检测的手段,这其中包括源代码的预处理,源代码转换为公式模型的具体方法,并设计实现一个原型系统。本文最后还给出了几个具体程序例子的验证过程。结果表明,该系统能够应用模型检测技术自动的进行一些软件的验证,为将来更广泛和深入地研究打下了坚实的基础。更多还原

【Abstract】 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.更多还原