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

SHANGHAI UNIVERSITY毕业设计 （论文）UNDERGRADUATE PROJECT (THESIS)题目从状态迁移图到SMV程序自动转换器的设计与实现学 院计算机工程与科学学院专 业计算机科学与技术学 号10122270学生姓名张珊珊指导教师缪淮扣起讫日期2014.2.21 -2014.5.30目录摘要3ABSTRACT4第一章 绪论51.1 课题研究的背景及意义51.2相关课题国内外现状51.3 研究内容6第二章 相关技术及开发工具介绍82.1画图工具介绍82.1.1 ArgoUML82.1.2 Jude92.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进行解析24 4.3 将解析后的语言转换为smv语言264.4对smv进行验证304.5 操作界面的设计314.5.1 打开文件功能314.5.2 保存功能324.5.3 转换功能324.5.4 退出功能33第五章 系统运行演示355.1 操作界面演示355.2状态迁移图的解析测试与转换385.2.1 dg.xmil状态图和解析测试结果385.2.2 TestGenerator.xmi状态图和解析测试结果395.2.3 TestGenerator.xmi转换成的smv语言415.2.4 mc-statechart.xmi状态图和解析测试结果455.2.5 mc-statechart.xmi转换成的smv语言46第六章 总结与展望486.1总结486.2展望48致 谢50参考文献51附录 部分源代码清单52摘要随着Internet的迅猛发展，当今社会已逐渐步入信息时代。计算机软硬件系统日益复杂，其正确性和可靠性已成为计算机领域中研究的热点，在诸多方法和理论中，模型检测以其简洁明了和自动化程度而备受关注。NuSMV作为一种有效的模型检测工具得到了越来越广泛的应用。本文在介绍了将状态迁移图转换为NuSMV可以识别的smv程序工具的设计与实现。该工具有助于理解状态迁移图，能灵活使用NuSMV工具，充分掌握SMV语言。开发的过程需要熟练使用java 语言和Eclipse环境。通过这个过程，设计了从状态迁移图表示的行为模型到NuSMV可以检测的模型的自动转换器，从而使NuSMV工具的使用过程更加简单。同时提高分析实际问题、解决问题的能力。本文第一章论述了课题的研究背景和意义、国内外研究现状和本文的主要研究内容。第二章论述了本次毕业设计运用的相关技术以及开发工具。第三章论述了系统的可行性、需求和性能分析。第四章论述了系统各项功能的设计和实现。第五章论述了系统运行演示。最后一章对论文进行了总结和展望。关键词：状态迁移图 NuSMV 转换 检测上海大学毕业设计(论文)ABSTRACTWith the rapid development of the Internet, Todays society is gradually entering the information age. With computer hardware and software systems more and more complex, its validity and reliability has become a hot research in field of computer. In many methods and theories, the model checking is a major concern for its simplicity and automation . NuSMV, as a kind of effective model checking tool, has been more and more widely used.The paper introduces design and implementation of the tool which transforms the state transition diagram into SMV program that NuSMV can recognize.This tool makes us understand the state transition diagram well, use NuSMV tool skillfully and master the SMV language fully.We need be familiar with the Java language and Eclipse environment for development process.Through this process,which is the transition from the state transition diagram to SMV program,we can find that the use process of NuSMV tools is more simple.At the same time,we can improve the ability to to analyze and solve problems.The paper is organized as follows. Chapter 1 discusses the subject research significance and background, domestic and foreign research status and the main research content of this article. Chapter 2 discusses the use of technologies and development tools which is related to this project design. Chapter 3 discusses the systems feasibility, requirements and performance analysis. Chapter 4 deals with the features of the system design and implementation. Chapter 5 makes an introduction about the system debugging and testing. The last chapter summarizes the paper and prospects.Keywords :State transition diagram、NuSMV、transform、test第一章 绪论本章主要介绍课题的背景和意义以及国内外的研究现状，进一步给出系统设计目标的实现效果。系统的实现将有助于NuSMV工具的方便使用。1.1 课题研究的背景及意义 在二十一世纪的今天,网络的诞生，极大地方便了人们地沟通和交流。同时，验证计算机硬件系统、软件系统或者两者的结合是否满足设计要求和是否正确很有意义，特别是对安全性要求很高的系统和商业价值很高的系统。也就是说，软件是否可信已经成为一个国家的国防、经济等系统能否正常运转的重要因素之一，尤其核反应堆控制、航空航天、铁路信号、核电站等安全攸关的领域更是如此，其失误和bug甚至崩溃可能会造成生命和财产的无法挽回的重大损失，如何确保这些系统的可靠性和安全性成为计算机科学领域中重要研究方向。 状态迁移图是用来描述系统或对象的状态,以及导致系统或对象的状态改变的事件,从而描述系统的行为。它具有直观性、单纯性。NuSMV作为一种常用的模型检验工具，它高效地实现了符号模型检测技术，已广泛应用于对软件、硬件系统的系统行为模型检验。在检验过程中，输入用状态迁移图表示的行为模型和待检验性质，NuSMV工具就可以对系统行为模型是否满足系统性质进行检验并给出检验结果。 此研究课题的意义就在于，通过实现从状态迁移图形式的系统行为模型向NuSMV工具可以识别的符合SMV语法的系统行为模型的转换，从而使NuSMV工具的使用过程更加简单。此外，该课题还可以提高我们综合使用所学课程,实际解决问题的能力。同时，自动转换和检测工具的实现技术有一定的学术价值和工程应用价值。1.2相关课题国内外现状 20世纪80年代初提出的模型检测属于基于模型的形式化验证方法，由于思想相对简单和自动化程度高，使得它广泛用于硬件电路和网络协议系统的验证，这种方法已经成功用于许多复杂的电路设计和通信协议验证。近年来，模型检测在软件验证方面也取得了一定的成绩。模型验证器对于在学术界、产业界应用模型检测具有很大的意义。(1) 国外现状SMV工具是美国CMU计算机学院的L.McMillan博士于1992年开发出的模型检验工具软件，它基于“符号模型检验”(Symbolic Model Checking)技术，SMV因此而得名。SMV早期是为了研究符号模型检验应用的可能性，而开发的一种对硬件进行检验的实验工具。发展到今天，SMV已成为国际上广为流行的分析有限状态系统的常用工具。SMV有多个版本，如：CMU-SMV、Cadence -SMV、NuSMV。目前，国外很多学者已经将NuSMV应用于爆炸系统的检测、航空航天技术、国防等诸多领域，并且在欧美发达国家发展的比较迅速。(2) 国内现状目前，国内对经典的模型验证器NuSMV的使用和研究不是很多，只在少数领域，如在PCI协议总线命令和总线信号的建模方面运用了NuSMV。这制约了它的应用以及对它的扩展和定制。并且从状态迁移图到NuSMV可以识别的模型自动转换是重要的工作。1.3 研究内容 本文主要工作内容是从状态迁移图到SMV程序自动转换器的设计与实现。 即设计一个自动转换器，完成从状态迁移图表示的行为模型向SMV语言描述的行为模型的转换工作，并用程序实现设计方案。其中包括对状态迁移图的各表示成分有清晰的理解；对SMV的输入语言的语法有清晰的理解; 状态迁移图表示的行为模型和SMV语言的对应关系转化关系和相关的程序实现。将状态迁移图表示的行为模型，在NuSMV上进行验证，从而真正理解状态迁移图，能灵活使用NuSMV工具，充分掌握SMV语言，同时也能熟练使用java 语言，熟悉Eclipse环境，通过这个过程，设计出从状态迁移图表示的行为模型到NuSMV可以检测的模型的自动转换器，从而使NuSMV工具的使用过程更加简单。具体过程包括在相应的画图工具上画出状态迁移图，导出xmi（xml）代码，对此代码进行解析后，可以进行解析测试，然后转换成SMV语言，再用NuSMV 工具对转换的语言进行验证。在此基础上再做出一个操作界面，用来方便展示自己的研究内容。这个操作界面包括打开、转换、保存、退出等功能。即可以打开xmi文档或者xml文档，查看具体的代码，然后可以选择转换按钮，对打开的xmi或者xml文档进行转换，将其转换为smv程序；点击保存按钮，可以将转换生成的smv程序保存在自己认为合适的位置；如果在打开文件、转化、保存过程中，因操作有误或者其他原因需要退出的，可以点击退出按钮，“确定”之后，即可退出。第二章 相关技术及开发工具介绍该部分主要介绍系统所采用的技术及开发工具，涉及画图的工具有ArgoUML、Jude，相关的开发工具有Eclipse，开发语言为java。2.1 画图工具介绍2.1.1 ArgoUMLArgoUML是一个用于绘制UML图的应用软件，它用Java构造，并遵守开源的BSD协议。 因为它本身由Java构建的缘故，所以ArgoUML能运行在任何支持Java的平台上。 2003年，ArgoUML获得了软件开发杂志的设计和分析工具类别的年度读者选择奖。ArgoUML没有完全实现UML标准，同时它对某些图还不能完全支持（如时序图）。当前的稳定版0.24版式对0.22的一个bug修复版，它一共修正了0.22版本的172个bug。ArgoUML的开发因为人力缺乏而受到影响。回退（Undo）功能早在2003年就已经提出，而迄今未实现。从v0.20版本开始的新特点：1) 选中状态下显示文字编辑框，如“联系（Associations）”等；在图中支持数据类型（DataTypes），构造型（Stereotypes）和枚举（Enumerations),支持CallStates, ObjectFlowStates,允许在不选择类（Class，亦称型别）的情况下绘制状态图（Statechart）；Critics browser improvements；Clear grid selection and snap。2) UML 1.4对UML1.4的扩展特性支持增强；兼容androMDA；质量-数百个bug得到修正；当前多数功能支持元素多选；支持从浏览树到图的拖拽操作，拖拽操作也适用于在浏览树内操作。其他特点：1）UML1.4的全部9种图都得到支持,紧密支持UML标准；无需下载安装，支持JWS，从浏览器安装运行；支持XMI；标准的UML1.4元模型（metamodel）；可以多种格式导出UML图：GIF，PNG，PS，EPS，PGML以及SVG ；具有图像编辑和缩放的高级功能；平台无关性使用Java1.5+。2）支持10种语言：英语，英语（EN-GB），德语，西班牙语，意大利语，俄语，法语，挪威语，葡萄牙语，汉语。Built-in design critics provide unobtrusive review of design and suggestions for improvements。3) 有可扩展的模型接口，支持OCL ；正向工程（支持生成C+ and C#, Java, PHP4, PHP5, Python, Ruby代码，Ada, Delphi和SQL也支持，但不成熟）；逆向工程（导入jar包）。4) 认知支持（Cognitive support）包括动作反应（Reflection-in-action）、机会主义设计（Opportunistic design）和问题理解和解决（Comprehension and Problem Solving）。其中动作反应（Reflection-in-action）包括Design Critics、自动纠正（部分实现）、待做（To Do）列表、用户模型（部分实现）；机会主义设计（Opportunistic design）包括待做（To Do）列表和清单（Checklists）；问题理解和解决（Comprehension and Problem Solving）包括浏览器视图预览（Explorer perspectives）和多重、交迭的视图。弱点：1) 无回退（undo）功能（或称反悔操作）。2) 对序列图（Sequence diagrams）支持不好 。3) 不支持UML 2.x 。2.1.2 JudeJUDE(Java and UML Developers Environment)，一个小巧实用的UML建模软件，不到2M，绝对可以符合UML建模的要求，可以画CLASS，USECASE，STATECHART，ACTIVITY，OBJECT，SEQUENCE，COLLABORATION，COMPONENT和DEPLOYMENT图，可以导入JAVA源文件直接建模，也可以导入ROSE98的MDL文件，可以将模型导出成JAVA源文件，HTML和文本格式。当然它不可能具备ROSE等大型软件的众多强大的功能，但绝大部分人在绝大部分时间用的仅仅是ROSE不到1%的功能，而且还存在着版权的问题。而JUDE是完全免费的，软件发布采用的SMALL RELEASE，一到两个星期就会发布一次，在不断开发新功能的同时，满足用户所提出的新功能的要求和修复前一版本可能存在BUG。JUDE是一个中日合作采用XP开发方式纯JAVA开发的软件，也可以说是半个国产软件（但是没有中文版），它功能完善，速度快，易操作，易上手，有很多优点。现在很多国际著名的UML组织的网站和论坛都已经有介绍和相关下载，但很不幸的是它在中国鲜有人知。现在Jude已经更名为：astah，包括社区版和免费版。随着UML的扩大，UML建模工具也越来越庞大。不过，许多功能并不是用户所寻求的。因此，Astah Professional（原名JUDE） 听取用户心声，根据用户需要打造，按照使用习惯设计，轻便简单，友好易用，用户可以轻松使用它来高速建模，极大的提高了效率。Astah Professional 功能强大，支持 UML1.4中所有图和主要的图形，元模（Meta Model）及属性，全面满足您建模所需，还集成了思维导图，工程合并，协作开发等十余项特色功能，以及许多方便用户的贴心实用的功能。Astah Professional 是100% 纯 Java 应用程序，可以跨平台在各种主流操作系统中使用。支持 OMG XMI标准格式，可以与其它建模工具交互模型。为方便用户书写 Office 文档，软件支持以 Microsoft EMF 增强图元拷贝粘贴至 Microsoft Office，也可以将模型信息导出到 Office Excel。软件提供了内容丰富的使用手册，全面查看 Astah Professional 所有的功能。简单，友好，强大，轻快，高效，以人为本，这就是Astah Professional最大的特色，可以提高 UML 建模效率。2.2 相关开发工具Eclipse介绍基本介绍：Eclipse 是一个开放源代码的、基于Java的可扩展开发平台。就其本身而言，它只是一个框架和一组服务，用于通过插件组件构建开发环境。幸运的是，Eclipse 附带了一个标准的插件集，包括Java开发工具（Java Development Kit，JDK）。虽然大多数用户很乐于将 Eclipse 当作 Java 集成开发环境（IDE）来使用，但 Eclipse 的目标却不仅限于此。Eclipse 还包括插件开发环境（Plug-in Development Environment，PDE），这个组件主要针对希望扩展 Eclipse 的软件开发人员，因为它允许他们构建与 Eclipse 环境无缝集成的工具。由于 Eclipse 中的每样东西都是插件，对于给 Eclipse 提供插件，以及给用户提供一致和统一的集成开发环境而言，所有工具开发人员都具有同等的发挥场所。这种平等和一致性并不仅限于 Java 开发工具。尽管 Eclipse 是使用Java语言开发的，但它的用途并不限于 Java 语言；例如，支持诸如C/C+、COBOL、PHP等编程语言的插件已经可用，或预计将会推出。Eclipse 框架还可用来作为与软件开发无关的其他应用程序类型的基础，比如内容管理系统。基于 Eclipse 的应用程序的一个突出例子是 IBM Rational Software Architect，它构成了 IBM Java 开发工具系列的基础。语言拓展：Eclipse是著名的跨平台的自由集成开发环境（IDE）。最初主要用来Java语言开发，通过安装不同的插件Eclipse可以支持不同的计算机语言，比如C+和Python等开发工具。Eclipse的本身只是一个框架平台，但是众多插件的支持使得Eclipse拥有其他功能相对固定的IDE软件很难具有的灵活性。许多软件开发商以Eclipse为框架开发自己的IDE。Eclipse 最初由OTI和IBM两家公司的IDE产品开发组创建，起始于1999年4月。IBM提供了最初的Eclipse代码基础，包括Platform、JDT 和PDE。Eclipse项目IBM发起，围绕着Eclipse项目已经发展成为了一个庞大的Eclipse联盟，有150多家软件公司参与到Eclipse项目中，其中包括Borland、Rational Software、Red Hat及Sybase等。Eclipse是一个开放源码项目，它其实是Visual Age for Java的替代品，其界面跟先前的Visual Age for Java差不多，但由于其开放源码，任何人都可以免费得到，并可以在此基础上开发各自的插件，因此越来越受人们关注。随后还有包括Oracle在内的许多大公司也纷纷加入了该项目，Eclipse的目标是成为可进行任何语言开发的IDE集成者，使用者只需下载各种语言的插件即可。主要组成：Eclipse是一个开放源代码的软件开发项目，专注于为高度集成的工具开发提供一个全功能的、具有商业品质的工业平台。它主要由Eclipse项目、Eclipse工具项目和Eclipse技术项目三个项目组成，具体包括四个部分组成Eclipse Platform、JDT、CDT和PDE。JDT支持Java开发、CDT支持C开发、PDE用来支持插件开发，Eclipse Platform则是一个开放的可扩展IDE，提供了一个通用的开发平台。它提供建造块和构造并运行集成软件开发工具的基础。Eclipse Platform允许工具建造者独立开发与他人工具无缝集成的工具从而无须分辨一个工具功能在哪里结束，而另一个工具功能在哪里开始。插件开发：Eclipse的插件机制是轻型软件组件化架构。在客户机平台上，Eclipse使用插件来提供所有的附加功能，例如支持Java以外的其他语言。已有的分离的插件已经能够支持C/C+（CDT）、Perl、Ruby，Python、telnet和数据库开发。插件架构能够支持将任意的扩展加入到现有环境中，例如配置管理，而决不仅仅限于支持各种编程语言。Eclipse的设计思想是：一切皆插件。Eclipse核心很小，其它所有功能都以插件的形式附加于Eclipse核心之上。Eclipse基本内核包括：图形API (SWT/Jface)， Java开发环境插件(JDT )，插件开发环境(PDE)等。插件安装的方式：插件安装的主要方式有直接复制法、使用link文件法、使用eclipse自带图形界面安装、使用dropins安装插件、使用Eclipse Macketplace。软件开发包：Eclipse SDK（软件开发者包）是Eclipse Platform、JDT和PDE所生产的组件合并，它们可以一次下载。这些部分在一起提供了一个具有丰富特性的开发环境，允许开发者有效地建造可以无缝集成到Eclipse Platform中的工具。Eclipse SDK由Eclipse项目生产的工具和来自其它开放源代码的第三方软件组合而成。Eclipse项目生产的软件以 GPL发布，第三方组件有各自自身的许可协议。新版本的特点：1）NLS string hover现在有一个Open in Properties File动作。2）在Caller模式下，调用层级（Call Hierarchy）现在有一个在上下文菜单中有一个Expand With Constructors动作。3）当你在编辑器中输入的时候，Java比较编辑器会更新其结构。4）有一个新的toString()产生器。5）为可覆盖方法增加了一个Open Implementation链接，可以直接打开其实现。6）编辑器与执行环境一致。7）Debug视图现在提供了breadcrumb（面包屑），显示了当前活动的debug上下文。8）可运行的JAR文件输出向导还可以把所需的类库打包进一个要输出的可运行JAR文件，或打包进与紧挨着该JAR的一个目录中。9）当在写一个分配表达式（allocation expression）时发生补全操作，ch内容助手现在可以提示一个类的可用构造方法。10）如果检测到无用代码，编译器现在可以发出警告。11）类库、变量或容器入口的路径现在可以是与项目相关的任何位置。12）在Jovadoc hover的头部及Javadoc视图中，现在都提供了引用其他类型和成员的链接。13）随该Eclipse发行的JUnit4版本更新为4.5。14）Javadoc视图及hovers现在都支持inheritDoc标签并给覆盖方法增加链接。15）同一值的比较现在由编译器检测，默认情况下会发出警告。2.3开发语言java介绍Java是由Sun Microsystems公司于 1995年5月推出的Java面向对象程序设计语言（以下简称Java语言）和Java平台的总称。由James Gosling和同事们共同研发，并在1995年正式推出。Java最初被称为Oak，是1991年为消费类电子产品的嵌入式芯片而设计的。1995年更名为Java，并重新设计用于开发Internet应用程序。用Java实现的HotJava浏览器（支持Java applet）显示了Java的魅力：跨平台、动态的Web、Internet计算。从此，Java被广泛接受并推动了Web的迅速发展，常用的浏览器均支持Javaapplet。另一方面，Java技术也不断更新。特点：1）Java语言是易学的。Java语言的语法与C语言和C+语言很接近，使得大多数程序员很容易学习和使用Java。另一方面，Java丢弃了C+中很少使用的、很难理解的、令人迷惑的那些特性，如操作符重载、多继承、自动的强制类型转换。特别地，Java语言不使用指针，而是引用。并提供了自动的废料收集，使得程序员不必为内存管理而担忧。2）Java语言是强制面向对象的。Java语言提供类、接口和继承等原语，为了简单起见，只支持类之间的单继承，但支持接口之间的多继承，并支持类与接口之间的实现机制（关键字为implements）。Java语言全面支持动态绑定，而C+语言只对虚函数使用动态绑定。总之，Java语言是一个纯的面向对象程序设计语言。3）Java语言是分布式的。Java语言支持Internet应用的开发，在基本的Java应用编程接口中有一个网络应用编程接口（java net），它提供了用于网络应用编程的类库，包括URL、URLConnection、Socket、ServerSocket等。Java的RMI（远程方法激活）机制也是开发分布式应用的重要手段。4）Java语言是健壮的。Java的强类型机制、异常处理、垃圾的自动收集等是Java程序健壮性的重要保证。对指针的丢弃是Java的明智选择。Java的安全检查机制使得Java更具健壮性。5）Java语言是安全的。Java通常被用在网络环境中，为此，Java提供了一个安全机制以防恶意代码的攻击。除了Java语言具有的许多安全特性以外，Java对通过网络下载的类具有一个安全防范机制（类ClassLoader），如分配不同的名字空间以防替代本地的同名类、字节代码检查，并提供安全管理机制（类SecurityManager）让Java应用设置安全哨兵。6）Java语言是体系结构中立的。Java程序（后缀为java的文件）在Java平台上被编译为体系结构中立的字节码格式（后缀为class的文件），然后可以在实现这个Java平台的任何系统中运行。这种途径适合于异构的网络环境和软件的分发。7）Java语言是可移植的。这种可移植性来源于体系结构中立性，另外，Java还严格规定了各个基本数据类型的长度。Java系统本身也具有很强的可移植性，Java编译器是用Java实现的，Java的运行环境是用ANSI C实现的。68）Java语言是解释型的。如前所述，Java程序在Java平台上被编译为字节码格式，然后可以在实现这个Java平台的任何系统中运行。在运行时，Java平台中的Java解释器对这些字节码进行解释执行，执行过程中需要的类在联接阶段被载入到运行环境中。9）Java是性能略高的。与那些解释型的高级脚本语言相比，Java的性能还是较优的。10）Java语言是原生支持多线程的。在Java语言中，线程是一种特殊的对象，它必须由Thread类或其子（孙）类来创建。通常有两种方法来创建线程：其一，使用型构为Thread(Runnable)的构造子将一个实现了Runnable接口的对象包装成一个线程，其二，从Thread类派生出子类并重写run方法，使用该子类创建的对象即为线程。值得注意的是Thread类已经实现了Runnable接口，因此，任何一个线程均有它的run方法，而run方法中包含了线程所要运行的代码。线程的活动由一组方法来控制。Java语言支持多个线程的同时执行，并提供多线程之间的同步机制（关键字为synchronized）。（11）Java语言是动态的。Java语言的设计目标之一是适应于动态变化的环境。Java程序需要的类能够动态地被载入到运行环境，也可以通过网络来载入所需要的类。这也有利于软件的升级。另外，Java中的类有一个运行时刻的表示，能进行运行时刻的类型检查。第三章 系统可行性与需求分析在软件工程中，需求分析是指在建立一个新的或改变一个现存的电脑系统时描写新系统的目的、范围、定义和功能时所要做的所有的工作。需求分析是软件工程中的一个关键过程。通过需求分析要明确系统的主要功能模块，以及各功能模块需要完成的具体功能。可行性分析也称为可行性研究，是在系统调查的基础上，针对新系统的开发是否具备必要性和可能性，对新系统的开发从技术、经济、社会的方面进行分析和研究，以避免投资失误，保证新系统的开发成功。本章对系统的可行性、功能需求、性能需求这几个方面进行分析。3.1 可行性分析可行性研究也称为可行性分析，是在系统调查的基础上，针对新系统的开发是否具备必要性和可能性，对新系统的开发从技术、经济、社会等方面进行分析和研究，以避免投资失误，保证新系统的开发成功。可行性研究的目的就是用最小的代价在尽可能短的时间内确定问题是否能够解决。该系统的可行性分析包括以下几个方面的内容：1） 经济可行性：主要是对项目的经济效益进行评价，本系统的开发不需要额外的硬件设备，只需要一台计算机和一些开发应用软件，并且本系统实施后可以显著提高工作效率，有助于NuSMV工具的方便使用。所以本系统开发在经济上是可行的。2） 技术可行性：本系统主要使用Java语言开发系统，这种语言具有简单易学的特性，把设计人员从繁琐复杂的界面设计中解脱出来。开发环境选用Eclipse，利用它我们可以很方便地实现解析与转换等功能。因此，系统的软件开发平台已成熟可行。3） 方案可行性：目前从状态迁移图到SMV程序自动转换器的设计与实现在国内研究的还比较少，特别是对NuSMV模型检测工具的使用范围还有待进一步扩大，所以此课题的研究具有深远意义。通过实现从状态迁移图形式的系统行为模型向NuSMV工具可以识别的符合SMV语法的系统行为模型的转换，从而使NuSMV工具的使用过程更加简单，更加迅速地普及到生活中的很多领域。因此，设计并实现从图到代码，再把代码转换成某种语言等等的能力至关重要，关系到我们是否能综合使用所学课程,提高实际解决问题的能力。4） 操作可行性：对于从状态迁移图到SMV程序自动转换器的设计与实现来说，在开发设计程序的过程中直观的界面和控件的文字解释完全能使得用户充分理解起功能和意义。在计算机普及的今天，用户对本系统的操作完全可以看作是一种简单的，配合形式的手工操作。所以本系统的操作是完全可行的。综上所述，此系统开发目的已明确，在技术、经济、方案、操作等四方面都可行，并且投入少、见效快。因此本系统的开发是完全可行的。3.2 功能需求分析3.2.1 系统功能流程设计 图3-1 系统功能流程图 如图3-1所示，本系统的设计流程为：先利用Jude或者ArgoUML工具画出状态迁移图，该画图工具可以自动生成xmi或者xml文件，然后在Eclipse平台上对已经生成的xmi或者xml，使用java编程进行解析，找到图中对应的关键的信息，如初始状态点集合、状态点集合、迁移集合等等。接着将解析好的程序模型转换成smv程序，最后用NuSMV工具对其进行验证。具体步骤为：第一步：在Jude画图工具上画出状态迁移图，导出xml文档，在eclipse环境中编写程序，对该文档进行解析，得出解析结果。如果xml文档有误或者不完整，可以直接退出。这一步作为一个小测验。第二步：在ArgoUML画图工具上画出状态迁移图，导出xmi文档，在eclipse环境中编写程序，对该文档进行解析，得出解析结果，其结果包括初始状态集合、状态集合、迁移集合、触发集合等。如果xmi文档有误或者不完整，可以直接退出。这一步作为第二个小测验。第三步：利用操作界面，打开相应的xmi文档或者xml文档，点击“转换”按钮，可以将其转换为SMV程序。第四步，对生成的SMV程序进行验证。（通常我们要用NuSMV工具进行验证，但是本课题将它作为后续研究内容）。3.2.2 操作界面的设计可以利用操作界面进行打开、保存、转换、退出等操作。转换退出保存打开 图3-2 操作界面的流程图 如图3-2所示，其过程如下： 打开：可以打开计算机上的任何一个文件。本设计系统重点是要查找用ArgoUML和Jude画图工具生成的xmi和xml文档，方便进行解析测试和转换。转换：当查找到xmi或者xml文档后，点击“转换”，便会弹出个窗口，点击“是”，即对上述xmi或者xml进行转换，将其转换为smv程序；点击“否”，即取消转换操作，还能再返回到打开文件的操作界面。 保存：将上述已经转换生成的smv程序进行保存，如果核对无误后，可以将其保存在合适的位置，以便日后使用NuSMV工具对其进行验证。 退出：当执行“打来文件”、“转换”、“保存”这些操作时，如果发现有误或者有必要需要退出时，点击“退出”按钮，会弹出个对话框，它有两个选项，“是”和“否”。如果点击“是”，则退出“从状态迁移图到SMV程序自动转换的设计与实现”的整个操作界面，如果点击“否”，则返回到上一步操作。3.3 性能需求分析实用性：提高了使用NuSMV工具使用的方便性，优化资源，实现效益最大化。操作性：适用于不同水平的使用者，都可以将自己需要检测的状态迁移图通过这一系列的步骤放到NuSMV工具上进行检测。技术性：本次设计和开发应紧跟着整个计算机发展潮流，采用先进的设计思想，利用最新的开发技术和开发工具。使系统能够无论在功能设计上，还是技术实现上，都处于领先地位。适应性良好：Java本身良好的兼容性是平台能广泛应用于不同计算机。系统采用模块化设计，用户可以根据自己的实际情况进行修改组合，使系统在不同硬件环境上都能得以应用。第四章 系统设计与实现本章主要介绍了系统设计和系统主要功能的实现。包括系统的详细设计与实现，包含状态迁移图转化为xmi（xml）、对xmi（xml）进行解析、将解析后的模型转换为smv程序、对smv进行验证等主要功能的实现。4.1 状态迁移图转换为xmi（xml）在ArgoUML(Jude)工具上画出状态迁移图（两种工具画图的方式有点不同），点击“文件”或者“工具”下面的“导出xmi（xml）”选项，就会自动生成xmi或者xml的文档，然后把它保存在合适的地方以供解析使用，这一部分不需要代码实现。4.2 对xmi（xml）进行解析4.2.1 对xmi进行解析 （1）State类：定义了状态迁移图中的状态，包括在状态图中id、状态名称name、别名alias、incomings迁移集合incomings、outgoings迁移集合outgoings等属性，以及得到修改以上属性的函数。 （2）Transition类：定义了UML状态图中的迁移，包括在状态图中的id、源状态source、目标状态target、触发trigger等属性。表示图中每个线段对应的初始状态点和终结状态点，以及得到修改以上属性的函数。 （3）Trigger类：表示UML状态图中的触发，包括在状态图中id、trigger的名称name、包含trigger的迁移集trans属性，以及得到修改以上属性的函数，表示状态图中的触发集合。 （4）Var类：定义了状态迁移图中的name、value等属性，以及得到修改以上属性的函数。 （5）UMLStateChart类：表示UML状态图中所有信息，包括UML工程中的唯一id、UML工程中的name、UML工程的初始状态initState、UML工程包含的所有状态states、UML工程包含的所有迁移transitions、UML工程包含的所有触发triggers等属性。（6）CTLFactory类：表示性质生成工厂，其中包括生成模型usc的可达性性质、活性性质、安全性性质。（7）UMLStateChartParser类：功能是对xmi进行解析。算法思想：对图中的UML工程中的唯一id、UML工程中的name、UML工程的初始状态initState、UML工程包含的所有状态states、UML工程包含的所有迁移transitions、UML工程包含的所有触发triggers、incomings迁移集合incomings、outgoings迁移集合outgoings等属性进行遍历。先找到incomings、outgoings信息，如果存在，说明有触发存在，说明图中有对应的线段，迁移集合中的元素加1；否则，接着往下遍历。如果存在某个状态点的incomings=0，说明它是初始状态点，将它写入初始状态集合。具体实现为：先找到UML工程中的唯一id，确定是对目标xmi文档的解析，然后找出所有UML工程中的name，确定状态集合；查找usc性质生成工厂；利用每个状态点的别名找到相互之间的指向关系，确定它的入度状态点和出度状态点；遍历每一个触发和对应的迁移关系，得到迁移集合和触发集合；如果遍历到某个状态点的入度incomings=0，则将该状态点写入初始状态集合initState。核心代码：public static UMLStateChart parser(String uscPath) init(uscPath); Element usm = (Element) doc.selectSingleNode(/UML:StateMachine); if(null = usm) return null; UMLStateChart usc = new UMLStateChart(); usc.setId(usm.attributeValue(xmi.id); usc.setName(usm.attributeValue(name); usc.setTriggers(parseTriggers(); usc.setStates(parseStates(); usc.setTransitions(parseTransitions(usc); usc.setInitState(usc.getStateById(parseInitState(usm); generateAliasForState(usc.getInitState(); return usc; private static Map parseTransitions(UMLStateChart usc) List transitionNodes = doc.selectNodes(/UML:Transitionxmi.id); Map trans = new HashMap(); for(Node node : transitionNodes) Element el = (Element) node; if(!isTransitionValid(el) continue; String id = el.