基于模型检测的uml形式化验证的研究

《基于模型检测的uml形式化验证的研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、摘要论文题目：基于模型检测的UML形式化验证的研究学科专业：计算机应用技术研究生：雷博指导教师：姚全珠教授摘要签名：UML作为一种软件面向对象分析和设计的建模语言，已经得到了广泛的应用，但是，在软件的设计过程中，难免会引入一些错误。传统的软件测试方法是在软件开发完成之后进行的，而如果能够在软件开发早期对系统设计进行形式化验证，这样既能保证软件的可靠性，还可以提高开发效率，节约开发成本。模型检测技术是一种主流的形式化验证方法，目前已经在硬件和协议验证方面取得了成功，利用模型检测技术对软件进行形式化验证成为近年来研究的一个热点。本文针对如何利用模型检测技术对软件设计阶段的

2、UML模型进行形式化验证这一问题进行了研究，在汲取前人的经验和教训的基础上，提出了一套形式化转换规则，改进了一种UML模型动态特性的一致性验证方法，主要包括三个方面的工作：首先，阐述了模型检测工具SPIN的工作原理和特点，分析了选取SPIN作为模型检测工具的优势，并且对其输入语言Promela和线性时态逻辑LTL进行了深入的分析；其次，选取了一个包括类图、状态图和协作图在内的UML子集，从中提取系统的静态和动态信息，并且提出了一套形式化转换规则，将其转换为模型检测工具SPIN所支持的Promela模型，对系统进行验证；最后，基于UML2．0顺序图所引入的交互片断，改进

3、了一种UML模型动态特性的一致性验证方法，在此方法中，对状态图的形式化转换尝试使用基于XYZ／E的中间方法，通过验证状态图所对应的Promela模型是否满足顺序图所对应的LTL公式来达到验证一致性的目的。关键词：UML：模型检测；SPIN：转换规则；一致性验证监哔簧Title：THERESEARCHOFUMLFORMALVEfUFICATIoNBASEDONMODELCHECKlNGMajor：ComputerApplicationTechnologyName：BoLEISupervisor：Prof_QuanzhuYAOSignature：堕丝Signature：脚

4、UMLhasbeenwidelyused，asasoftwareobject-orientedanalysisanddesignlanguage．ButitwillinevitablyintroducesomeerrorsinthesoRwaredesignprocess．Traditionalsoftwaretestingmethodiscarriedouta矗erthesoftwarefinished．However,wehopetobeabletoperformformalverificationintheearlystageofsoftwaredevelopm

5、em，whichCanguaranteethereliabilityofthesoftware，improvethedevelopmentefficiencyandreducethecost．ThemodelcheckingisamainstreamformalverificationmethodandhasbeengetaSUCCESSintheprotocolandverification．Ithasbecomearesearchhotspothowtoverifysoftwareusingmodelcheckingtechnologyinrecentyears．

6、ThispaperresearchestheproblemhowtoverifytheUMLmodelinthesoftwaredesignphasewiththcmodelcheckingtechnology．Basedonpreviousexperienceandlesson，weputforwardasetofformaltransformationrulesandimproveaconsistencyverificationmethodforthedynamiccharacteristicsoftheUMLmodel．Therearethreemainjobs

7、wedone．asfollows：Firstly,expoundtheworkingprincipleandcharacteristicsofmodelcheckingtoolSPIN，analysiswhywechosenSPINaSmodelcheckingtool，andstudythePromelalanguagewhichistheinputlanguageofSPINandLinear-timeTemporalLogic．Secondly,selectaUMLsubsetwhichincludesclassdiagram,statedia