模型检验综述.pdf

《模型检验综述.pdf》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、第40卷第6A期计算机科学Vo1．40No．6A2013年6月ComputerScienceJune2013模型检验综述王蓁蓁(金陵科技学院信息技术学院南京211169)摘要在软硬件验证里，模型检验是一个重要手段，至今它已经形成一个庞大的方法论体系。现在我们把模型检验内容从标准方法、抽象解释方法、综合方法3个范畴加以介绍，旨在形成人们对模型检验总的印象，从而全面理解和掌握模型检验各个方法的精神实质和具体情况，有助于将这些方法运用到实际软硬件验证中并从中受到启发，以便进一步发展模型检验理论或开发模型检验新的方法和工具。关键词时态逻辑，模型检验，抽象解释，抽象模型检验中图法分类号TP3

2、11文献标识码ASurveyofModelCheckingWANGZhen-zhen(SchoolofInformationTechnology，JinlingInstituteofTechnology，Nanjing211169，China)AbstractModelcheckingisanimportanttechniqueinsoftware／hardwareverification，andithasbecomeanenormoussystemofmethodologies．Nowweinvestigatedthecontentsofmodelcheckingfromthre

3、ecategorieswhicharestandardmethods，abstractinterpretationmethodsandintegratemethodsrespectively．Theaimofthissurveyismakingonetohaveacompleteimpressionaboutmodelchecking．Inthiswayonemayfullyunderstandandgraspthespiritsandcon—cretecontentsofeverymethodinmodelchecking．Thestudieshelpinapplyingthes

4、emethodstOthepiratica1software／hardwareverification，andfurthermore，inspiredofthis，onemaydevelopnewmodelcheckingtheoriesornewmethodsortoolsofmodelchecking．KeywordsTemporallogic，Modelchecking，Abstractinterpretation，Abstractmodelchecking功。但是完全测试是不可能的，通常测试也不能直接指出缺1引言陷存在的位置。迄今为止，软、硬件的验证技术主要有四大方法体系：

5、模形式证明，例如在软件中的正确性证明，是显示产品正确拟、测试、形式证明和模型检验[1]。模拟方法也许是人类最传的一种数学技术，它的一个重要方面是应与设计和编程结合统的一种验证自己创造的产品功效的方法。即使在最新的验进行，Dijkstra把它表达为“程序员应让程序证明和程序一起证技术里，仍然看到它渗透其中并发挥它自己的作用。例如发展”。形式证明系统比较著名的是霍尔逻辑，其中证明规则在产品寿命试验里，加速寿命试验方法的基本思想是用加大是语法制导的，其中主要精神是把证明一条复合命令的部分应力(诸如热应力、电应力、机械应力等)的办法，加快产品失正确性断言简化成证明它的直接子命令的部分正确性

6、断言。效，缩短试验时间；运用加速寿命模型，估计出产品在正常工虽然形式证明系统的优点是它能够自动证明程序的某些性作应力下的可靠性特征。在软件测验中，驱动程序和桩等技质，但是利用霍尔逻辑即使证明很小的程序的正确性也不是术也是应用模拟思想的典型方法。模拟方法具有很多优点，那么容易，例如证明“循环出口条件”和循环语句的不变式。特别是它们为产品创造了用其他方法难以创造的环境条件。因此，许多软件工程实践者提出，正确性证明不能看成是标准然而它的结论通常具有统计特性，并且依赖于一些假设和理的软件工程技术。他们认为除了证明太难以外，证明也太昂论模型。例如软件可靠性的测量和预测经典地依赖参数或可贵了，

7、没有实用性。靠性增长模型(Jelinski-Moranda模型)，因此它的准确性需要模型检验是基于有限状态空间来保证软硬件设计正确性处理。的形式化自动验证技术，基本思想是预先设定软硬件应该具测试是一个重要的方法体系，直观地说，测试是预先设计有的规格即属性，而在模型不满足规格时，给出反例，如果满出一些策略、方法、工具和用例，对产品进行试验，看其性能是足，通常都给出肯定。上述优点比其他传统方法更为突出，因否符合要求。现今软件已经渗透到我们的日常生活，它的安此日益得到人们的