模型检测在软件方面的应用
摘要
模型检测技术是一种自动化的检测技术,该技术广泛应用于时序电路设计和通信协议设计,并取得了很大的成绩。真正将模型检测技术引入到软件的验证只有短短的几年历史,该技术目前正处于研究阶段。
本文在实验室研究成果的基础上,首先探讨了模型检测的主要思想、发展变革及最新的研究热点,重点阐述了软件模型检测的特点。最后给出对于软件源代码进行建模的过程和算法,详细阐述了几个属性检测的手段,这其中包括源代码的预处理,源代码转换为公式模型的具体方法,并设计实现一个原型系统。
本文最后还给出了几个具体程序例子的验证过程。结果表明,该系统能够应用模型检测技术自动的进行一些软件的验证,为将来更广泛和深入地研究打下了坚实的基础。
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.
本文在实验室研究成果的基础上,首先探讨了模型检测的主要思想、发展变革及最新的研究热点,重点阐述了软件模型检测的特点。最后给出对于软件源代码进行建模的过程和算法,详细阐述了几个属性检测的手段,这其中包括源代码的预处理,源代码转换为公式模型的具体方法,并设计实现一个原型系统。
本文最后还给出了几个具体程序例子的验证过程。结果表明,该系统能够应用模型检测技术自动的进行一些软件的验证,为将来更广泛和深入地研究打下了坚实的基础。
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.
引文
[1] 张家海, 胡虹, 胡恒章. 组合导航软件可靠性的评估 [J]. 哈尔滨工业大学学报,2003年03期,64-67.
[2]O.Grumberg,E.M.ClarkeandD.A.Peled,ModelChecking, TheMITPress,Cambridge,MA,2000,10-96.
[3] M. Y. Vardi and P.Wolper. An automata-theoretic approach to automaticprogram verification. In Proceedings of the First Annual Symposium onLogic in Computer Science. IEEE Compute Society Press, June 1986,213-237.
[4] 林惠民,张文辉,模型检测:理论、方法与应用. 电子学报,2002年第12期(第30卷),1907-1910.
[5] R.E.Bryant, Graph based algorithms for BooleanfunctionManipulation.IEEETransactionComputers,1986No.8,Vol.C-35,667-691.
[6] J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill and L. J. Hwa-ng.Symbolic model checking: 10^20 states andbeyond. In Proc.SymposiumonLogicinComputerScience,1990,IEEE,428–439.
[7] A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M.Roveri, R. Sebastiani, and A. Tacchella. Nusmv Version 2: AnOpenSource Tool for Symbolic Model Checking. In Proc. InternationalConference on Computer-Aided Verification(CAV 2002), July 2002,Volume2404ofLNCS,156-188.
[8]‘BLASTwebsite’.http://www-cad.eecs.berkeley.edu/~rupak/blast.
[9]‘MAGICwebsite’.http://www.cs.cmu.edu/~chaki/magic.
[10]‘SLAMwebsite’.http://research.microsoft.com/slam.
[11]‘JavaPathFinderwebsite’.http://www.research.compaq.com/SRC/esc.
[12]‘MOPSwebsite’.http://www.cs.berkeley.edu/~daw/mops/.
[13] Hao Chen, Drew Dean, and David Wagner. Model checking one millionlines of C code. In Proceeding of the 11th Annual Network andDistributed System Security Symposium (NDSS), San Diego, CA,2004,February4-6,171-185.
[14] J. R. Burch, E. M. Clarke, and D. E. Long. Symbolic model checkingwithpartitionedtransitionrelation.InA.HalaasandP.B.Denyereditors,Proceeding of the 1991 International Conference on Very Large ScaleIntegration, August 1991. Winner of the Sidney Michaelson Best PaperAward,28-56.
[15]B.Yang,Optimizingsymbolicmodel checkingforinvariant-richmodels.InProc.CAV’99,2000,No.1633inLNCS,330-350.
[16] A. Biere, E. Clarke, Bounded Model Checking,Advances inComputers,2003,Vol.58,118-149。
[17] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checkingwithout BDDs. In Proc. TACAS, 1999, Volume 1579 of LNCS,193–207.
[18] J. Hopcoft and J. Ullman. Introduction to automata theory, languages,andcomputation.Addison-Wesley,1979.
[19] Gerard J. Holzmann, Doron Peled. An Improvement in FormalVerification. Proceedings FORTE 1994 Conference, Bern, Switzerland,October1994,4-7.
[20]‘SPINwebsite’.http://spinroot.com/spin/whatispin.html.
[21] G. J. Holzmarm, The model checker SPIN, IEEE Transactions onSoftwareEngineering,1997,23(5),279-295.
[22]E.A.Emerson, A.P.Sistla.Symmetryandmodel checking[A]. LectureNotes in Computer Science 697 -5th International Conference onComputer Aided Verification (CAV 93) [C]. Berlin: Springer-verlag,1993,463-478.
[23] 林云,关于需求分析建模与模型验证技术的研究,华中师范大学硕士论文,2001年5月,4-5.
[24] 董威, 面向UML的模型检验研究, 国防科技大学博士论文, 2002年10月,3-20.
[25] Willem Visser, Klaus Havelund, Guillaume Brat, Seungjoon Prk, FlavioLerda. Model Checking Programing. Automated Software Engineering.2003,Volume10,203-232.
[26] 刘磊等,程序分析技术,机械工业出版社,2005年8月第1版,33-95.
[27] 袁志斌等,软件模型检测中的抽象,计算机科学,2006年第7期 第33卷,276-279.
[28] Sagar Chaki, Edmund Clarke, Alex Groce, Joel Ouaknine, OferStrichman, Karen Yorav,Efficient Verification of Sequential andConcurrent C Programs, Formal Methods in System Design (FMSD),Volume25,Issue2-3,129-166.
[29] Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar and GregoireSutre. lazy Abstraction. ACM SIGPLAN-SIGACT Conference onPrinciplesofProgrammingLanguages,2002,58-70.
[30] T. Ball and S. K. Rajamani. Bebop: A symbolic model checker forBoolean Programs. In SPIN 00: SPIN Workshop, LNCS 1885,Springer-Verlag,2000,113-130.
[31] Thomas Ball, Rupak Majumdar, Todd Millstein, Sriram K. Rajamani,Automatic Predicate Abstraction of C Programs. PLDI 2001, SIGPLANNotices36(5),203-213.
[32]ShobhaVasudevan,JacobA.Abraham.Staticprogramtransformationsforefficientsoftwaremodelchecking,http://www.cerc.utexas.edu/~shobha/book.pdf.
[33]B.Berard,M. Bidoit,A.Finkel,et al.SystemsandSoftwareVerification:Model-CheckingTechniquesandTools,Springer,2001(1),2-41.
[34] Joost-Pieter Katoen. Concepts, Algorithms, and Tools for ModelChecking. Lecture Notes of the Course “Mechanised Validation ofParallelSystem”,Semester,1998-1999,255-356.
[2]O.Grumberg,E.M.ClarkeandD.A.Peled,ModelChecking, TheMITPress,Cambridge,MA,2000,10-96.
[3] M. Y. Vardi and P.Wolper. An automata-theoretic approach to automaticprogram verification. In Proceedings of the First Annual Symposium onLogic in Computer Science. IEEE Compute Society Press, June 1986,213-237.
[4] 林惠民,张文辉,模型检测:理论、方法与应用. 电子学报,2002年第12期(第30卷),1907-1910.
[5] R.E.Bryant, Graph based algorithms for BooleanfunctionManipulation.IEEETransactionComputers,1986No.8,Vol.C-35,667-691.
[6] J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill and L. J. Hwa-ng.Symbolic model checking: 10^20 states andbeyond. In Proc.SymposiumonLogicinComputerScience,1990,IEEE,428–439.
[7] A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M.Roveri, R. Sebastiani, and A. Tacchella. Nusmv Version 2: AnOpenSource Tool for Symbolic Model Checking. In Proc. InternationalConference on Computer-Aided Verification(CAV 2002), July 2002,Volume2404ofLNCS,156-188.
[8]‘BLASTwebsite’.http://www-cad.eecs.berkeley.edu/~rupak/blast.
[9]‘MAGICwebsite’.http://www.cs.cmu.edu/~chaki/magic.
[10]‘SLAMwebsite’.http://research.microsoft.com/slam.
[11]‘JavaPathFinderwebsite’.http://www.research.compaq.com/SRC/esc.
[12]‘MOPSwebsite’.http://www.cs.berkeley.edu/~daw/mops/.
[13] Hao Chen, Drew Dean, and David Wagner. Model checking one millionlines of C code. In Proceeding of the 11th Annual Network andDistributed System Security Symposium (NDSS), San Diego, CA,2004,February4-6,171-185.
[14] J. R. Burch, E. M. Clarke, and D. E. Long. Symbolic model checkingwithpartitionedtransitionrelation.InA.HalaasandP.B.Denyereditors,Proceeding of the 1991 International Conference on Very Large ScaleIntegration, August 1991. Winner of the Sidney Michaelson Best PaperAward,28-56.
[15]B.Yang,Optimizingsymbolicmodel checkingforinvariant-richmodels.InProc.CAV’99,2000,No.1633inLNCS,330-350.
[16] A. Biere, E. Clarke, Bounded Model Checking,Advances inComputers,2003,Vol.58,118-149。
[17] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checkingwithout BDDs. In Proc. TACAS, 1999, Volume 1579 of LNCS,193–207.
[18] J. Hopcoft and J. Ullman. Introduction to automata theory, languages,andcomputation.Addison-Wesley,1979.
[19] Gerard J. Holzmann, Doron Peled. An Improvement in FormalVerification. Proceedings FORTE 1994 Conference, Bern, Switzerland,October1994,4-7.
[20]‘SPINwebsite’.http://spinroot.com/spin/whatispin.html.
[21] G. J. Holzmarm, The model checker SPIN, IEEE Transactions onSoftwareEngineering,1997,23(5),279-295.
[22]E.A.Emerson, A.P.Sistla.Symmetryandmodel checking[A]. LectureNotes in Computer Science 697 -5th International Conference onComputer Aided Verification (CAV 93) [C]. Berlin: Springer-verlag,1993,463-478.
[23] 林云,关于需求分析建模与模型验证技术的研究,华中师范大学硕士论文,2001年5月,4-5.
[24] 董威, 面向UML的模型检验研究, 国防科技大学博士论文, 2002年10月,3-20.
[25] Willem Visser, Klaus Havelund, Guillaume Brat, Seungjoon Prk, FlavioLerda. Model Checking Programing. Automated Software Engineering.2003,Volume10,203-232.
[26] 刘磊等,程序分析技术,机械工业出版社,2005年8月第1版,33-95.
[27] 袁志斌等,软件模型检测中的抽象,计算机科学,2006年第7期 第33卷,276-279.
[28] Sagar Chaki, Edmund Clarke, Alex Groce, Joel Ouaknine, OferStrichman, Karen Yorav,Efficient Verification of Sequential andConcurrent C Programs, Formal Methods in System Design (FMSD),Volume25,Issue2-3,129-166.
[29] Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar and GregoireSutre. lazy Abstraction. ACM SIGPLAN-SIGACT Conference onPrinciplesofProgrammingLanguages,2002,58-70.
[30] T. Ball and S. K. Rajamani. Bebop: A symbolic model checker forBoolean Programs. In SPIN 00: SPIN Workshop, LNCS 1885,Springer-Verlag,2000,113-130.
[31] Thomas Ball, Rupak Majumdar, Todd Millstein, Sriram K. Rajamani,Automatic Predicate Abstraction of C Programs. PLDI 2001, SIGPLANNotices36(5),203-213.
[32]ShobhaVasudevan,JacobA.Abraham.Staticprogramtransformationsforefficientsoftwaremodelchecking,http://www.cerc.utexas.edu/~shobha/book.pdf.
[33]B.Berard,M. Bidoit,A.Finkel,et al.SystemsandSoftwareVerification:Model-CheckingTechniquesandTools,Springer,2001(1),2-41.
[34] Joost-Pieter Katoen. Concepts, Algorithms, and Tools for ModelChecking. Lecture Notes of the Course “Mechanised Validation ofParallelSystem”,Semester,1998-1999,255-356.