一种自动的形式化验证技术一模型检测

《一种自动的形式化验证技术一模型检测》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、软件时空中文核心期刊《微计算机信息》(管控一体化)2007年第23卷第11-3期一种自动的形式化验证技术一模型检测Mode／一Checking—AnAutomaticF0rmalVerificationTechniq’ue(1．江西省高性能计算技术重点实验室；2．江西师范大学)化志章1,2揭安全1,2薛锦云1,2HUAZHIZHANGJIEANQUANXUEJINYUN摘要：模型检测是针对有限状态系统行为的逻辑性质的一种自动验证技术，已有许多工业应用，其主要缺陷是空间爆炸问题．本文通过一简单实例介绍其基本思想、检测步骤和相关理论，给出一些处理状态空间爆炸问题的优化

2、技术，并与其它验证方法进行了比较，最后简单介绍了软件模型检测的新进展．关键字：模型检测；形式验证；时态逻辑中图分类号：TP301．1文献标识码：AAbstract：Modelcheckingisatechniqueofautomaticallyverifyinglogicalpropertiesofthebehavioroffinitestatesystems，whichhasmanyapplicationsinindustry．Itsmaindisadvantageisstatespaceexplosionproblem．Thebasicideas，applic

3、ationstepsandrelevanttheoriesaboutmodel-checkingareoutlinedbyasimpleexample．Andsomeapproachesfordealingwiththestateexplosionproblemareintroduced，Atlast．wecomparedwithotherverificationmethods，andsomenewachievementsofsoftwaremodelcheckingaredis-cussedbriefly，KeyWords：modelchecking,forma

4、lverification,temporallogic径是计算L(Ap)nL(ACD是否为空集，不为空则反例产生；时态逻1引言辑模型检测用状态迁移系统S表示系统的行为,so是初始状态计算机软硬件系统功能日渐强大，系统更趋复杂，同时也更集(s0_cs)用模态／H寸序逻辑公式F刻画系统的性质，通过计算找脆弱，微小的错误，都可能引发灾难性的后果．对于有交互、实时、到S中所有满足F的状态组成的集合S，若S0_CS则通过验并发、分布等特色的系统，其行为有一定的不确定性，传统的测试证．由于状态空间有限，可以确保检测能够终止．一个时态逻辑公手段如跟踪调试、用例覆盖等技术难以发挥

5、效果．模型检测是针式可以转换为一个等价的自动机，Vardi和Wolper于1986年实对有限状态系统行为的逻辑性质的一种自动验证技术．模型检测现了将时态逻辑检测转变为自动机模型检测，从而把这两种方器在算法支持下可以自动执行，并能在系统不满足性质时提供反法关联起来。例路径．因此备受工业界关注．目前已成功地应用于芯片设计、通模型检测一般包含建模、规约、验证三步骤．下文将介绍时态信协议、控制系统等的分析与验证，产生了SMV、Spin、Uppaal等逻辑模型检测方式。一批工具，Intel、IBM等公司已经将模型检测技术应用于产品的2．2建模(modeling)开发过程中。

6、建模就是基于待测属性从系统中抽象出模型，作为分析和本文首先探讨模型检测基本思想，通过简单实例展现应用步检测的基础．模型一般用有限状态迁移系统表示，并使用状态变骤．之后介绍应对空间爆炸问题问题的一些优化技术，并与其他迁序列刻画系统的执行．合理的模型应完整无误地反映实际系验证方法比较，最后简要介绍了软件模型检测的新进展。统中待测属性的所有变化，同时模型规模适中．模型的状态空间是系统中所有变量值域的笛卡尔积．Kripke一结构(后文简称KS)2基本原理【7】是一种常用的模型描述形式．它是一个带标签的有向图，可定2．1思想综述义为：M：(AP1s，SO，R，L)，AP是一

7、组原子命题，S、SO表示有限状态集模型检测最早由Clark等人提出，其思想是先建立待测系统(钴点集)和初始状态集，s0_cS,R是迁移关系(边集)，R_CSxS，且R的有限状态模型，然后用算法穷尽检测模型中的状态，判断其是是完全(tota1)的，即对任意一个状态S∈S均存在一个状态S∈S，否满足待测属性．若不满足，根据反馈信息判断具体系统中是否有R(s，s)，标签函数L：s一2AP，把状态s∈S映射为在S中为真切实存在违反此属性的执行路径(即反例路径)．按模型及属性的的原子命题集合，该集合是AP的一个子集．1(S中的路径就是实描述方式不同，将其分为两类：自动机模型

8、检测和时态