从状态迁移图到SMV程序自动转换器的设计与实现

《从状态迁移图到SMV程序自动转换器的设计与实现》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、SHANGHAIUNIVERSITY毕业设计（论文）UNDERGRADUATEPROJECT(THESIS)题目从状态迁移图到SMV程序自动转换器的设计与实现学院计算机工程与科学学院专业计算机科学与技术学号10122270学生姓名张珊珊指导教师缪淮扣起讫日期2014.2.21-2014.5.30目录摘要3ABSTRACT4第一章绪论51.1课题研究的背景及意义51.2相关课题国内外现状51.3研究内容6第二章相关技术及开发工具介绍82.1画图工具介绍82.1.1ArgoUML82.1.2Jude92

2、.2相关开发工具介绍102.3开发语言java介绍13第三章系统可行性与需求分析163.1可行性分析163.2功能需求分析173.2.1系统更能流程设计173.2.2操作界面的设计183.3性能需求分析18第四章系统设计与实现204.1状态迁移图转换为xmi（xml）204.2对xmi（xml）进行解析204.2.1对xmi进行解析204.2.2对xml进行解析244.3将解析后的语言转换为smv语言264.4对smv进行验证304.5操作界面的设计314.5.1打开文件功能314.5.2保存功能3

3、24.5.3转换功能324.5.4退出功能33第五章系统运行演示355.1操作界面演示355.2状态迁移图的解析测试与转换385.2.1dg.xmil状态图和解析测试结果385.2.2TestGenerator.xmi状态图和解析测试结果395.2.3TestGenerator.xmi转换成的smv语言415.2.4mc-statechart.xmi状态图和解析测试结果455.2.5mc-statechart.xmi转换成的smv语言46第六章总结与展望486.1总结486.2展望48致谢50参考文

4、献51附录部分源代码清单52摘要随着Internet的迅猛发展，当今社会已逐渐步入信息时代。计算机软硬件系统日益复杂，其正确性和可靠性已成为计算机领域中研究的热点，在诸多方法和理论中，模型检测以其简洁明了和自动化程度而备受关注。NuSMV作为一种有效的模型检测工具得到了越来越广泛的应用。本文在介绍了将状态迁移图转换为NuSMV可以识别的smv程序工具的设计与实现。该工具有助于理解状态迁移图，能灵活使用NuSMV工具，充分掌握SMV语言。开发的过程需要熟练使用java语言和Eclipse环境。通过这个

5、过程，设计了从状态迁移图表示的行为模型到NuSMV可以检测的模型的自动转换器，从而使NuSMV工具的使用过程更加简单。同时提高分析实际问题、解决问题的能力。本文第一章论述了课题的研究背景和意义、国内外研究现状和本文的主要研究内容。第二章论述了本次毕业设计运用的相关技术以及开发工具。第三章论述了系统的可行性、需求和性能分析。第四章论述了系统各项功能的设计和实现。第五章论述了系统运行演示。最后一章对论文进行了总结和展望。关键词：状态迁移图NuSMV转换检测上海大学毕业设计(论文)ABSTRACTWith

6、therapiddevelopmentoftheInternet,Today’ssocietyisgraduallyenteringtheinformationage.Withcomputerhardwareandsoftwaresystemsmoreandmorecomplex,itsvalidityandreliabilityhasbecomeahotresearchinfieldofcomputer.Inmanymethodsandtheories,themodelcheckingisamaj

7、orconcernforitssimplicityandautomation.NuSMV,asakindofeffectivemodelcheckingtool,hasbeenmoreandmorewidelyused.ThepaperintroducesdesignandimplementationofthetoolwhichtransformsthestatetransitiondiagramintoSMVprogramthatNuSMVcanrecognize.Thistoolmakesusu

8、nderstandthestatetransitiondiagramwell,useNuSMVtoolskillfullyandmastertheSMVlanguagefully.WeneedbefamiliarwiththeJavalanguageandEclipseenvironmentfordevelopmentprocess.Throughthisprocess,whichisthetransitionfromthestatetransitiondiagram