nusmv模型验证器实现的分析

《nusmv模型验证器实现的分析》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、中山大学硕士论文NuS～f＼『模型验证器实现分析NuSMV模型验证器实现分析专业：计算机应用技术硕士生：张军林导’师：张治国摘要模型检测(ModelChecking)是由E．M．Clarke与E．A．Emerson提出的一种形式化验证方法。其基本思想是在有限状态转移系统上，通过穷尽搜索的方法，验证系统规范是否得到满足。它广泛用于验证数字电路系统和网络协议系统的设计是否正确。模型检测的一个基本问题是状态爆炸问题，针对这个问题，已提出多种解决方法，其中，符号模型检测技术是一个经典的缓解状态爆炸问题的方法。NuSMV是一个经典的模型检测工具，它高效地实现了符号模型检测技术

2、。NuSMV主要由意大利特兰托大学的A．Cimatti和M．Roveri所开发，它有很好的软件体系结构，易于定制和扩展。目前有关NuSMV如何实现符号模型检测技术的文献资料不多，这限制了NuSMV的应用、定制和扩展。本文主要工作就是分析和研究NuSMV的实现源码，给出NuSMV实现符号模型检测技术的方法和原理。通过分析NuSMV的整体体系结构、模块间的关系、模块内部的程序结构、模块间接口调用方法、内部数据结构和算法，获得了一份详细的分析文档。该分析文档给出了有限状态转移系统和规范用OBDD(有序二叉决策图)表示的具体方法、用OBDD实现模型检测算法的方法和NuSMV

3、的实现代码与符号模型检测技术理论层面的对应关系。论文结合大量的实例检验和说明分析结果。本文的分析结果，对NuSMV进行定制和扩展具有参考价值。关键词：模型检测，NuSMV，OBDD，实现分析，代码分析中山大学硕士论文NuSI{、r模型验证器实现分析TheImplementationAnalysisofNuSMVModelCheckerMajor：ComputerEngineeringName：ZhangJunlinSupervisor：ZhangZhiguoAbstractModelCheckingproposedbyE．M．ClarkandE．A．Emersoni

4、saformalverificationapproach．Itverifiesthatafinitestatemachine(FSM)satisfiesaspecificationbyexhaustivelysearchingtheFSM’Sstates．ModelCheckingiswidelyemployedtoverifydigitalcircuitsystemandnetworkprotocolsystem．OnebasicproblemofModelCheckingisthestateexplosionproblem．SymbolicModelChecki

5、ngisatypicalapproachtothestateexplosionproblem．NuSMVisaclassicmodelcheckingtoolitimplementsthesymbolicmodelchecking．NuSMVisdevelopedinTrentobyA．CimattiandM．Roveriandisaimedatbeingcustomizablcandextensibleandhasagoodsot}warearchitecture．ThemajorworkofthethesisistoanalyzeandresearchtheNu

6、SMVsourcecodes．Byanalyzingthearchitecture，kernelmodules，datastructuresandalgorithmsofNuSMVindetail,weobtainadetailedtechnicalreport．ThereportdescribesindetailhowOBDDtorepresentfinitestatemachineandspecificationsandhowthemodelcheckingalgorithmCanbeimplementedusingOBDDasthebasicdatastruc

7、ture．ThethesiswillbehelpfultocustomizeandextendNuSMV．KeyWords：ModelChecking，NuSMV,OBDD，Implementation,CodeAnalysis．Ill论文原创性声明本人郑重声明：+所呈交的学位论文，是本人在导师的指导下，独立进行研究工作所取得的成果。除文中已经注明引用的内容外，本论文不包含任何其他个人或集体已经发表或撰写过的作品成果。对本文的研究作出重要贡献的个人和集体，均己在文中以明确方式标明。本人完全意识到本声明的法律结果由本人承担。学位论文作者签名：至墨室查至日期：21＆