從狀態(tài)遷移圖到SMV程序自動轉(zhuǎn)換器的設(shè)計與實現(xiàn)

1、SHANGHAI UNIVERSITY畢業(yè)設(shè)計 （論文）UNDERGRADUATE PROJECT (THESIS)題目從狀態(tài)遷移圖到SMV程序自動轉(zhuǎn)換器的設(shè)計與實現(xiàn)學 院計算機工程與科學學院專 業(yè)計算機科學與技術(shù)學 號10122270學生姓名張珊珊指導教師繆淮扣起訖日期2014.2.21 -2014.5.30目錄摘要3ABSTRACT4第一章 緒論51.1 課題研究的背景及意義51.2相關(guān)課題國內(nèi)外現(xiàn)狀51.3 研究內(nèi)容6第二章 相關(guān)技術(shù)及開發(fā)工具介紹82.1畫圖工具介紹82.1.1 ArgoUML82.1.2 Jude92.2 相關(guān)開發(fā)工具介紹102.3 開發(fā)語言java介紹13第三章 系

2、統(tǒng)可行性與需求分析163.1 可行性分析163.2 功能需求分析173.2.1 系統(tǒng)更能流程設(shè)計173.2.2 操作界面的設(shè)計183.3 性能需求分析18第四章 系統(tǒng)設(shè)計與實現(xiàn)204.1 狀態(tài)遷移圖轉(zhuǎn)換為xmi（xml）204.2 對xmi（xml）進行解析204.2.1 對xmi進行解析204.2.2 對xml進行解析24 4.3 將解析后的語言轉(zhuǎn)換為smv語言264.4對smv進行驗證304.5 操作界面的設(shè)計314.5.1 打開文件功能314.5.2 保存功能324.5.3 轉(zhuǎn)換功能324.5.4 退出功能33第五章 系統(tǒng)運行演示355.1 操作界面演示355.2狀態(tài)遷移圖的解析測試與轉(zhuǎn)

3、換385.2.1 dg.xmil狀態(tài)圖和解析測試結(jié)果385.2.2 TestGenerator.xmi狀態(tài)圖和解析測試結(jié)果395.2.3 TestGenerator.xmi轉(zhuǎn)換成的smv語言415.2.4 mc-statechart.xmi狀態(tài)圖和解析測試結(jié)果455.2.5 mc-statechart.xmi轉(zhuǎn)換成的smv語言46第六章 總結(jié)與展望486.1總結(jié)486.2展望48致 謝50參考文獻51附錄 部分源代碼清單52摘要隨著Internet的迅猛發(fā)展，當今社會已逐漸步入信息時代。計算機軟硬件系統(tǒng)日益復雜，其正確性和可靠性已成為計算機領(lǐng)域中研究的熱點，在諸多方法和理論中，模型檢測以其簡潔

4、明了和自動化程度而備受關(guān)注。NuSMV作為一種有效的模型檢測工具得到了越來越廣泛的應(yīng)用。本文在介紹了將狀態(tài)遷移圖轉(zhuǎn)換為NuSMV可以識別的smv程序工具的設(shè)計與實現(xiàn)。該工具有助于理解狀態(tài)遷移圖，能靈活使用NuSMV工具，充分掌握SMV語言。開發(fā)的過程需要熟練使用java 語言和Eclipse環(huán)境。通過這個過程，設(shè)計了從狀態(tài)遷移圖表示的行為模型到NuSMV可以檢測的模型的自動轉(zhuǎn)換器，從而使NuSMV工具的使用過程更加簡單。同時提高分析實際問題、解決問題的能力。本文第一章論述了課題的研究背景和意義、國內(nèi)外研究現(xiàn)狀和本文的主要研究內(nèi)容。第二章論述了本次畢業(yè)設(shè)計運用的相關(guān)技術(shù)以及開發(fā)工具。第三章論述了

5、系統(tǒng)的可行性、需求和性能分析。第四章論述了系統(tǒng)各項功能的設(shè)計和實現(xiàn)。第五章論述了系統(tǒng)運行演示。最后一章對論文進行了總結(jié)和展望。關(guān)鍵詞：狀態(tài)遷移圖 NuSMV 轉(zhuǎn)換 檢測上海大學畢業(yè)設(shè)計(論文)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 reliabilit

6、y 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 w

7、hich 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 proce

8、ss.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 subj

9、ect 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 system's feasibility, requirements and

10、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第一章 緒論本章主要介紹課題的背景和意義以及國內(nèi)

11、外的研究現(xiàn)狀，進一步給出系統(tǒng)設(shè)計目標的實現(xiàn)效果。系統(tǒng)的實現(xiàn)將有助于NuSMV工具的方便使用。1.1 課題研究的背景及意義 在二十一世紀的今天,網(wǎng)絡(luò)的誕生，極大地方便了人們地溝通和交流。同時，驗證計算機硬件系統(tǒng)、軟件系統(tǒng)或者兩者的結(jié)合是否滿足設(shè)計要求和是否正確很有意義，特別是對安全性要求很高的系統(tǒng)和商業(yè)價值很高的系統(tǒng)。也就是說，軟件是否可信已經(jīng)成為一個國家的國防、經(jīng)濟等系統(tǒng)能否正常運轉(zhuǎn)的重要因素之一，尤其核反應(yīng)堆控制、航空航天、鐵路信號、核電站等安全攸關(guān)的領(lǐng)域更是如此，其失誤和bug甚至崩潰可能會造成生命和財產(chǎn)的無法挽回的重大損失，如何確保這些系統(tǒng)的可靠性和安全性成為計算機科學領(lǐng)域中重要研究方向

12、。 狀態(tài)遷移圖是用來描述系統(tǒng)或?qū)ο蟮臓顟B(tài),以及導致系統(tǒng)或?qū)ο蟮臓顟B(tài)改變的事件,從而描述系統(tǒng)的行為。它具有直觀性、單純性。NuSMV作為一種常用的模型檢驗工具，它高效地實現(xiàn)了符號模型檢測技術(shù)，已廣泛應(yīng)用于對軟件、硬件系統(tǒng)的系統(tǒng)行為模型檢驗。在檢驗過程中，輸入用狀態(tài)遷移圖表示的行為模型和待檢驗性質(zhì)，NuSMV工具就可以對系統(tǒng)行為模型是否滿足系統(tǒng)性質(zhì)進行檢驗并給出檢驗結(jié)果。 此研究課題的意義就在于，通過實現(xiàn)從狀態(tài)遷移圖形式的系統(tǒng)行為模型向NuSMV工具可以識別的符合SMV語法的系統(tǒng)行為模型的轉(zhuǎn)換，從而使NuSMV工具的使用過程更加簡單。此外，該課題還可以提高我們綜合使用所學課程,實際解決問題的能力。

13、同時，自動轉(zhuǎn)換和檢測工具的實現(xiàn)技術(shù)有一定的學術(shù)價值和工程應(yīng)用價值。1.2相關(guān)課題國內(nèi)外現(xiàn)狀 20世紀80年代初提出的模型檢測屬于基于模型的形式化驗證方法，由于思想相對簡單和自動化程度高，使得它廣泛用于硬件電路和網(wǎng)絡(luò)協(xié)議系統(tǒng)的驗證，這種方法已經(jīng)成功用于許多復雜的電路設(shè)計和通信協(xié)議驗證。近年來，模型檢測在軟件驗證方面也取得了一定的成績。模型驗證器對于在學術(shù)界、產(chǎn)業(yè)界應(yīng)用模型檢測具有很大的意義。(1) 國外現(xiàn)狀SMV工具是美國CMU計算機學院的L.McMillan博士于1992年開發(fā)出的模型檢驗工具軟件，它基于“符號模型檢驗”(Symbolic Model Checking)技術(shù)，SMV因此而得名。

14、SMV早期是為了研究符號模型檢驗應(yīng)用的可能性，而開發(fā)的一種對硬件進行檢驗的實驗工具。發(fā)展到今天，SMV已成為國際上廣為流行的分析有限狀態(tài)系統(tǒng)的常用工具。SMV有多個版本，如：CMU-SMV、Cadence -SMV、NuSMV。目前，國外很多學者已經(jīng)將NuSMV應(yīng)用于爆炸系統(tǒng)的檢測、航空航天技術(shù)、國防等諸多領(lǐng)域，并且在歐美發(fā)達國家發(fā)展的比較迅速。(2) 國內(nèi)現(xiàn)狀目前，國內(nèi)對經(jīng)典的模型驗證器NuSMV的使用和研究不是很多，只在少數(shù)領(lǐng)域，如在PCI協(xié)議總線命令和總線信號的建模方面運用了NuSMV。這制約了它的應(yīng)用以及對它的擴展和定制。并且從狀態(tài)遷移圖到NuSMV可以識別的模型自動轉(zhuǎn)換是重要的工作。

15、1.3 研究內(nèi)容 本文主要工作內(nèi)容是從狀態(tài)遷移圖到SMV程序自動轉(zhuǎn)換器的設(shè)計與實現(xiàn)。 即設(shè)計一個自動轉(zhuǎn)換器，完成從狀態(tài)遷移圖表示的行為模型向SMV語言描述的行為模型的轉(zhuǎn)換工作，并用程序?qū)崿F(xiàn)設(shè)計方案。其中包括對狀態(tài)遷移圖的各表示成分有清晰的理解；對SMV的輸入語言的語法有清晰的理解; 狀態(tài)遷移圖表示的行為模型和SMV語言的對應(yīng)關(guān)系轉(zhuǎn)化關(guān)系和相關(guān)的程序?qū)崿F(xiàn)。將狀態(tài)遷移圖表示的行為模型，在NuSMV上進行驗證，從而真正理解狀態(tài)遷移圖，能靈活使用NuSMV工具，充分掌握SMV語言，同時也能熟練使用java 語言，熟悉Eclipse環(huán)境，通過這個過程，設(shè)計出從狀態(tài)遷移圖表示的行為模型到NuSMV可以檢測

16、的模型的自動轉(zhuǎn)換器，從而使NuSMV工具的使用過程更加簡單。具體過程包括在相應(yīng)的畫圖工具上畫出狀態(tài)遷移圖，導出xmi（xml）代碼，對此代碼進行解析后，可以進行解析測試，然后轉(zhuǎn)換成SMV語言，再用NuSMV 工具對轉(zhuǎn)換的語言進行驗證。在此基礎(chǔ)上再做出一個操作界面，用來方便展示自己的研究內(nèi)容。這個操作界面包括打開、轉(zhuǎn)換、保存、退出等功能。即可以打開xmi文檔或者xml文檔，查看具體的代碼，然后可以選擇轉(zhuǎn)換按鈕，對打開的xmi或者xml文檔進行轉(zhuǎn)換，將其轉(zhuǎn)換為smv程序；點擊保存按鈕，可以將轉(zhuǎn)換生成的smv程序保存在自己認為合適的位置；如果在打開文件、轉(zhuǎn)化、保存過程中，因操作有誤或者其他原因需要退

17、出的，可以點擊退出按鈕，“確定”之后，即可退出。第二章 相關(guān)技術(shù)及開發(fā)工具介紹該部分主要介紹系統(tǒng)所采用的技術(shù)及開發(fā)工具，涉及畫圖的工具有ArgoUML、Jude，相關(guān)的開發(fā)工具有Eclipse，開發(fā)語言為java。2.1 畫圖工具介紹2.1.1 ArgoUMLArgoUML是一個用于繪制UML圖的應(yīng)用軟件，它用Java構(gòu)造，并遵守開源的BSD協(xié)議。 因為它本身由Java構(gòu)建的緣故，所以ArgoUML能運行在任何支持Java的平臺上。 2003年，ArgoUML獲得了軟件開發(fā)雜志的設(shè)計和分析工具類別的年度讀者選擇獎。ArgoUML沒有完全實現(xiàn)UML標準，同時它對某些圖還不能完全支持（如時序圖）。

18、當前的穩(wěn)定版0.24版式對0.22的一個bug修復版，它一共修正了0.22版本的172個bug。ArgoUML的開發(fā)因為人力缺乏而受到影響?；赝耍║ndo）功能早在2003年就已經(jīng)提出，而迄今未實現(xiàn)。從v0.20版本開始的新特點：1) 選中狀態(tài)下顯示文字編輯框，如“聯(lián)系（Associations）”等；在圖中支持數(shù)據(jù)類型（DataTypes），構(gòu)造型（Stereotypes）和枚舉（Enumerations),支持CallStates, ObjectFlowStates,允許在不選擇類（Class，亦稱型別）的情況下繪制狀態(tài)圖（Statechart）；Critics browser impro

19、vements；Clear grid selection and snap。2) UML 1.4對UML1.4的擴展特性支持增強；兼容androMDA；質(zhì)量-數(shù)百個bug得到修正；當前多數(shù)功能支持元素多選；支持從瀏覽樹到圖的拖拽操作，拖拽操作也適用于在瀏覽樹內(nèi)操作。其他特點：1）UML1.4的全部9種圖都得到支持,緊密支持UML標準；無需下載安裝，支持JWS，從瀏覽器安裝運行；支持XMI；標準的UML1.4元模型（metamodel）；可以多種格式導出UML圖：GIF，PNG，PS，EPS，PGML以及SVG ；具有圖像編輯和縮放的高級功能；平臺無關(guān)性使用Java1.5+。2）支持10種語言：

20、英語，英語（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）包括動作反應(yīng)（Reflection-in-acti

21、on）、機會主義設(shè)計（Opportunistic design）和問題理解和解決（Comprehension and Problem Solving）。其中動作反應(yīng)（Reflection-in-action）包括Design Critics、自動糾正（部分實現(xiàn)）、待做（To Do）列表、用戶模型（部分實現(xiàn)）；機會主義設(shè)計（Opportunistic design）包括待做（To Do）列表和清單（Checklists）；問題理解和解決（Comprehension and Problem Solving）包括瀏覽器視圖預覽（Explorer perspectives）和多重、交迭的視圖。弱點：1

22、) 無回退（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源文件，

23、HTML和文本格式。當然它不可能具備ROSE等大型軟件的眾多強大的功能，但絕大部分人在絕大部分時間用的僅僅是ROSE不到1%的功能，而且還存在著版權(quán)的問題。而JUDE是完全免費的，軟件發(fā)布采用的SMALL RELEASE，一到兩個星期就會發(fā)布一次，在不斷開發(fā)新功能的同時，滿足用戶所提出的新功能的要求和修復前一版本可能存在BUG。JUDE是一個中日合作采用XP開發(fā)方式純JAVA開發(fā)的軟件，也可以說是半個國產(chǎn)軟件（但是沒有中文版），它功能完善，速度快，易操作，易上手，有很多優(yōu)點?，F(xiàn)在很多國際著名的UML組織的網(wǎng)站和論壇都已經(jīng)有介紹和相關(guān)下載，但很不幸的是它在中國鮮有人知?，F(xiàn)在Jude已經(jīng)更名為：a

24、stah，包括社區(qū)版和免費版。隨著UML的擴大，UML建模工具也越來越龐大。不過，許多功能并不是用戶所尋求的。因此，Astah Professional（原名JUDE） 聽取用戶心聲，根據(jù)用戶需要打造，按照使用習慣設(shè)計，輕便簡單，友好易用，用戶可以輕松使用它來高速建模，極大的提高了效率。Astah Professional 功能強大，支持 UML1.4中所有圖和主要的圖形，元模（Meta Model）及屬性，全面滿足您建模所需，還集成了思維導圖，工程合并，協(xié)作開發(fā)等十余項特色功能，以及許多方便用戶的貼心實用的功能。Astah Professional 是100% 純 Java 應(yīng)用程序，可以跨

25、平臺在各種主流操作系統(tǒng)中使用。支持 OMG XMI標準格式，可以與其它建模工具交互模型。為方便用戶書寫 Office 文檔，軟件支持以 Microsoft EMF 增強圖元拷貝粘貼至 Microsoft Office，也可以將模型信息導出到 Office Excel。軟件提供了內(nèi)容豐富的使用手冊，全面查看 Astah Professional 所有的功能。簡單，友好，強大，輕快，高效，以人為本，這就是Astah Professional最大的特色，可以提高 UML 建模效率。2.2 相關(guān)開發(fā)工具Eclipse介紹基本介紹：Eclipse 是一個開放源代碼的、基于Java的可擴展開發(fā)平臺。就其本

26、身而言，它只是一個框架和一組服務(wù)，用于通過插件組件構(gòu)建開發(fā)環(huán)境。幸運的是，Eclipse 附帶了一個標準的插件集，包括Java開發(fā)工具（Java Development Kit，JDK）。雖然大多數(shù)用戶很樂于將 Eclipse 當作 Java 集成開發(fā)環(huán)境（IDE）來使用，但 Eclipse 的目標卻不僅限于此。Eclipse 還包括插件開發(fā)環(huán)境（Plug-in Development Environment，PDE），這個組件主要針對希望擴展 Eclipse 的軟件開發(fā)人員，因為它允許他們構(gòu)建與 Eclipse 環(huán)境無縫集成的工具。由于 Eclipse 中的每樣東西都是插件，對于給 Ecli

27、pse 提供插件，以及給用戶提供一致和統(tǒng)一的集成開發(fā)環(huán)境而言，所有工具開發(fā)人員都具有同等的發(fā)揮場所。這種平等和一致性并不僅限于 Java 開發(fā)工具。盡管 Eclipse 是使用Java語言開發(fā)的，但它的用途并不限于 Java 語言；例如，支持諸如C/C+、COBOL、PHP等編程語言的插件已經(jīng)可用，或預計將會推出。Eclipse 框架還可用來作為與軟件開發(fā)無關(guān)的其他應(yīng)用程序類型的基礎(chǔ)，比如內(nèi)容管理系統(tǒng)?；?Eclipse 的應(yīng)用程序的一個突出例子是 IBM Rational Software Architect，它構(gòu)成了 IBM Java 開發(fā)工具系列的基礎(chǔ)。語言拓展：Eclipse是著名的

28、跨平臺的自由集成開發(fā)環(huán)境（IDE）。最初主要用來Java語言開發(fā)，通過安裝不同的插件Eclipse可以支持不同的計算機語言，比如C+和Python等開發(fā)工具。Eclipse的本身只是一個框架平臺，但是眾多插件的支持使得Eclipse擁有其他功能相對固定的IDE軟件很難具有的靈活性。許多軟件開發(fā)商以Eclipse為框架開發(fā)自己的IDE。Eclipse 最初由OTI和IBM兩家公司的IDE產(chǎn)品開發(fā)組創(chuàng)建，起始于1999年4月。IBM提供了最初的Eclipse代碼基礎(chǔ)，包括Platform、JDT 和PDE。Eclipse項目IBM發(fā)起，圍繞著Eclipse項目已經(jīng)發(fā)展成為了一個龐大的Eclipse

29、聯(lián)盟，有150多家軟件公司參與到Eclipse項目中，其中包括Borland、Rational Software、Red Hat及Sybase等。Eclipse是一個開放源碼項目，它其實是Visual Age for Java的替代品，其界面跟先前的Visual Age for Java差不多，但由于其開放源碼，任何人都可以免費得到，并可以在此基礎(chǔ)上開發(fā)各自的插件，因此越來越受人們關(guān)注。隨后還有包括Oracle在內(nèi)的許多大公司也紛紛加入了該項目，Eclipse的目標是成為可進行任何語言開發(fā)的IDE集成者，使用者只需下載各種語言的插件即可。主要組成：Eclipse是一個開放源代碼的軟件開發(fā)項目，

30、專注于為高度集成的工具開發(fā)提供一個全功能的、具有商業(yè)品質(zhì)的工業(yè)平臺。它主要由Eclipse項目、Eclipse工具項目和Eclipse技術(shù)項目三個項目組成，具體包括四個部分組成Eclipse Platform、JDT、CDT和PDE。JDT支持Java開發(fā)、CDT支持C開發(fā)、PDE用來支持插件開發(fā)，Eclipse Platform則是一個開放的可擴展IDE，提供了一個通用的開發(fā)平臺。它提供建造塊和構(gòu)造并運行集成軟件開發(fā)工具的基礎(chǔ)。Eclipse Platform允許工具建造者獨立開發(fā)與他人工具無縫集成的工具從而無須分辨一個工具功能在哪里結(jié)束，而另一個工具功能在哪里開始。插件開發(fā)：Eclipse

31、的插件機制是輕型軟件組件化架構(gòu)。在客戶機平臺上，Eclipse使用插件來提供所有的附加功能，例如支持Java以外的其他語言。已有的分離的插件已經(jīng)能夠支持C/C+（CDT）、Perl、Ruby，Python、telnet和數(shù)據(jù)庫開發(fā)。插件架構(gòu)能夠支持將任意的擴展加入到現(xiàn)有環(huán)境中，例如配置管理，而決不僅僅限于支持各種編程語言。Eclipse的設(shè)計思想是：一切皆插件。Eclipse核心很小，其它所有功能都以插件的形式附加于Eclipse核心之上。Eclipse基本內(nèi)核包括：圖形API (SWT/Jface)， Java開發(fā)環(huán)境插件(JDT )，插件開發(fā)環(huán)境(PDE)等。插件安裝的方式：插件安裝的主要

32、方式有直接復制法、使用link文件法、使用eclipse自帶圖形界面安裝、使用dropins安裝插件、使用Eclipse Macketplace。軟件開發(fā)包：Eclipse SDK（軟件開發(fā)者包）是Eclipse Platform、JDT和PDE所生產(chǎn)的組件合并，它們可以一次下載。這些部分在一起提供了一個具有豐富特性的開發(fā)環(huán)境，允許開發(fā)者有效地建造可以無縫集成到Eclipse Platform中的工具。Eclipse SDK由Eclipse項目生產(chǎn)的工具和來自其它開放源代碼的第三方軟件組合而成。Eclipse項目生產(chǎn)的軟件以 GPL發(fā)布，第三方組件有各自自身的許可協(xié)議。新版本的特點：1）NLS

33、 string hover現(xiàn)在有一個Open in Properties File動作。2）在Caller模式下，調(diào)用層級（Call Hierarchy）現(xiàn)在有一個在上下文菜單中有一個Expand With Constructors動作。3）當你在編輯器中輸入的時候，Java比較編輯器會更新其結(jié)構(gòu)。4）有一個新的toString()產(chǎn)生器。5）為可覆蓋方法增加了一個Open Implementation鏈接，可以直接打開其實現(xiàn)。6）編輯器與執(zhí)行環(huán)境一致。7）Debug視圖現(xiàn)在提供了breadcrumb（面包屑），顯示了當前活動的debug上下文。8）可運行的JAR文件輸出向?qū)н€可以把所需的類庫

34、打包進一個要輸出的可運行JAR文件，或打包進與緊挨著該JAR的一個目錄中。9）當在寫一個分配表達式（allocation expression）時發(fā)生補全操作，ch內(nèi)容助手現(xiàn)在可以提示一個類的可用構(gòu)造方法。10）如果檢測到無用代碼，編譯器現(xiàn)在可以發(fā)出警告。11）類庫、變量或容器入口的路徑現(xiàn)在可以是與項目相關(guān)的任何位置。12）在Jovadoc hover的頭部及Javadoc視圖中，現(xiàn)在都提供了引用其他類型和成員的鏈接。13）隨該Eclipse發(fā)行的JUnit4版本更新為4.5。14）Javadoc視圖及hovers現(xiàn)在都支持inheritDoc標簽并給覆蓋方法增加鏈接。15）同一值的比較現(xiàn)在由

35、編譯器檢測，默認情況下會發(fā)出警告。2.3開發(fā)語言java介紹Java是由Sun Microsystems公司于 1995年5月推出的Java面向?qū)ο蟪绦蛟O(shè)計語言（以下簡稱Java語言）和Java平臺的總稱。由James Gosling和同事們共同研發(fā)，并在1995年正式推出。Java最初被稱為Oak，是1991年為消費類電子產(chǎn)品的嵌入式芯片而設(shè)計的。1995年更名為Java，并重新設(shè)計用于開發(fā)Internet應(yīng)用程序。用Java實現(xiàn)的HotJava瀏覽器（支持Java applet）顯示了Java的魅力：跨平臺、動態(tài)的Web、Internet計算。從此，Java被廣泛接受并推動了Web的迅速發(fā)

36、展，常用的瀏覽器均支持Javaapplet。另一方面，Java技術(shù)也不斷更新。特點：1）Java語言是易學的。Java語言的語法與C語言和C+語言很接近，使得大多數(shù)程序員很容易學習和使用Java。另一方面，Java丟棄了C+中很少使用的、很難理解的、令人迷惑的那些特性，如操作符重載、多繼承、自動的強制類型轉(zhuǎn)換。特別地，Java語言不使用指針，而是引用。并提供了自動的廢料收集，使得程序員不必為內(nèi)存管理而擔憂。2）Java語言是強制面向?qū)ο蟮?。Java語言提供類、接口和繼承等原語，為了簡單起見，只支持類之間的單繼承，但支持接口之間的多繼承，并支持類與接口之間的實現(xiàn)機制（關(guān)鍵字為implements

37、）。Java語言全面支持動態(tài)綁定，而C+語言只對虛函數(shù)使用動態(tài)綁定?？傊琂ava語言是一個純的面向?qū)ο蟪绦蛟O(shè)計語言。3）Java語言是分布式的。Java語言支持Internet應(yīng)用的開發(fā)，在基本的Java應(yīng)用編程接口中有一個網(wǎng)絡(luò)應(yīng)用編程接口（java net），它提供了用于網(wǎng)絡(luò)應(yīng)用編程的類庫，包括URL、URLConnection、Socket、ServerSocket等。Java的RMI（遠程方法激活）機制也是開發(fā)分布式應(yīng)用的重要手段。4）Java語言是健壯的。Java的強類型機制、異常處理、垃圾的自動收集等是Java程序健壯性的重要保證。對指針的丟棄是Java的明智選擇。Java的安全檢

38、查機制使得Java更具健壯性。5）Java語言是安全的。Java通常被用在網(wǎng)絡(luò)環(huán)境中，為此，Java提供了一個安全機制以防惡意代碼的攻擊。除了Java語言具有的許多安全特性以外，Java對通過網(wǎng)絡(luò)下載的類具有一個安全防范機制（類ClassLoader），如分配不同的名字空間以防替代本地的同名類、字節(jié)代碼檢查，并提供安全管理機制（類SecurityManager）讓Java應(yīng)用設(shè)置安全哨兵。6）Java語言是體系結(jié)構(gòu)中立的。Java程序（后綴為java的文件）在Java平臺上被編譯為體系結(jié)構(gòu)中立的字節(jié)碼格式（后綴為class的文件），然后可以在實現(xiàn)這個Java平臺的任何系統(tǒng)中運行。這種途徑適合于

39、異構(gòu)的網(wǎng)絡(luò)環(huán)境和軟件的分發(fā)。7）Java語言是可移植的。這種可移植性來源于體系結(jié)構(gòu)中立性，另外，Java還嚴格規(guī)定了各個基本數(shù)據(jù)類型的長度。Java系統(tǒng)本身也具有很強的可移植性，Java編譯器是用Java實現(xiàn)的，Java的運行環(huán)境是用ANSI C實現(xiàn)的。68）Java語言是解釋型的。如前所述，Java程序在Java平臺上被編譯為字節(jié)碼格式，然后可以在實現(xiàn)這個Java平臺的任何系統(tǒng)中運行。在運行時，Java平臺中的Java解釋器對這些字節(jié)碼進行解釋執(zhí)行，執(zhí)行過程中需要的類在聯(lián)接階段被載入到運行環(huán)境中。9）Java是性能略高的。與那些解釋型的高級腳本語言相比，Java的性能還是較優(yōu)的。10）Jav

40、a語言是原生支持多線程的。在Java語言中，線程是一種特殊的對象，它必須由Thread類或其子（孫）類來創(chuàng)建。通常有兩種方法來創(chuàng)建線程：其一，使用型構(gòu)為Thread(Runnable)的構(gòu)造子將一個實現(xiàn)了Runnable接口的對象包裝成一個線程，其二，從Thread類派生出子類并重寫run方法，使用該子類創(chuàng)建的對象即為線程。值得注意的是Thread類已經(jīng)實現(xiàn)了Runnable接口，因此，任何一個線程均有它的run方法，而run方法中包含了線程所要運行的代碼。線程的活動由一組方法來控制。Java語言支持多個線程的同時執(zhí)行，并提供多線程之間的同步機制（關(guān)鍵字為synchronized）。（11）J

41、ava語言是動態(tài)的。Java語言的設(shè)計目標之一是適應(yīng)于動態(tài)變化的環(huán)境。Java程序需要的類能夠動態(tài)地被載入到運行環(huán)境，也可以通過網(wǎng)絡(luò)來載入所需要的類。這也有利于軟件的升級。另外，Java中的類有一個運行時刻的表示，能進行運行時刻的類型檢查。第三章 系統(tǒng)可行性與需求分析在軟件工程中，需求分析是指在建立一個新的或改變一個現(xiàn)存的電腦系統(tǒng)時描寫新系統(tǒng)的目的、范圍、定義和功能時所要做的所有的工作。需求分析是軟件工程中的一個關(guān)鍵過程。通過需求分析要明確系統(tǒng)的主要功能模塊，以及各功能模塊需要完成的具體功能。可行性分析也稱為可行性研究，是在系統(tǒng)調(diào)查的基礎(chǔ)上，針對新系統(tǒng)的開發(fā)是否具備必要性和可能性，對新系統(tǒng)的開

42、發(fā)從技術(shù)、經(jīng)濟、社會的方面進行分析和研究，以避免投資失誤，保證新系統(tǒng)的開發(fā)成功。本章對系統(tǒng)的可行性、功能需求、性能需求這幾個方面進行分析。3.1 可行性分析可行性研究也稱為可行性分析，是在系統(tǒng)調(diào)查的基礎(chǔ)上，針對新系統(tǒng)的開發(fā)是否具備必要性和可能性，對新系統(tǒng)的開發(fā)從技術(shù)、經(jīng)濟、社會等方面進行分析和研究，以避免投資失誤，保證新系統(tǒng)的開發(fā)成功。可行性研究的目的就是用最小的代價在盡可能短的時間內(nèi)確定問題是否能夠解決。該系統(tǒng)的可行性分析包括以下幾個方面的內(nèi)容：1） 經(jīng)濟可行性：主要是對項目的經(jīng)濟效益進行評價，本系統(tǒng)的開發(fā)不需要額外的硬件設(shè)備，只需要一臺計算機和一些開發(fā)應(yīng)用軟件，并且本系統(tǒng)實施后可以顯著提高

43、工作效率，有助于NuSMV工具的方便使用。所以本系統(tǒng)開發(fā)在經(jīng)濟上是可行的。2） 技術(shù)可行性：本系統(tǒng)主要使用Java語言開發(fā)系統(tǒng)，這種語言具有簡單易學的特性，把設(shè)計人員從繁瑣復雜的界面設(shè)計中解脫出來。開發(fā)環(huán)境選用Eclipse，利用它我們可以很方便地實現(xiàn)解析與轉(zhuǎn)換等功能。因此，系統(tǒng)的軟件開發(fā)平臺已成熟可行。3） 方案可行性：目前從狀態(tài)遷移圖到SMV程序自動轉(zhuǎn)換器的設(shè)計與實現(xiàn)在國內(nèi)研究的還比較少，特別是對NuSMV模型檢測工具的使用范圍還有待進一步擴大，所以此課題的研究具有深遠意義。通過實現(xiàn)從狀態(tài)遷移圖形式的系統(tǒng)行為模型向NuSMV工具可以識別的符合SMV語法的系統(tǒng)行為模型的轉(zhuǎn)換，從而使NuSMV

44、工具的使用過程更加簡單，更加迅速地普及到生活中的很多領(lǐng)域。因此，設(shè)計并實現(xiàn)從圖到代碼，再把代碼轉(zhuǎn)換成某種語言等等的能力至關(guān)重要，關(guān)系到我們是否能綜合使用所學課程,提高實際解決問題的能力。4） 操作可行性：對于從狀態(tài)遷移圖到SMV程序自動轉(zhuǎn)換器的設(shè)計與實現(xiàn)來說，在開發(fā)設(shè)計程序的過程中直觀的界面和控件的文字解釋完全能使得用戶充分理解起功能和意義。在計算機普及的今天，用戶對本系統(tǒng)的操作完全可以看作是一種簡單的，配合形式的手工操作。所以本系統(tǒng)的操作是完全可行的。綜上所述，此系統(tǒng)開發(fā)目的已明確，在技術(shù)、經(jīng)濟、方案、操作等四方面都可行，并且投入少、見效快。因此本系統(tǒng)的開發(fā)是完全可行的。3.2 功能需求分析

45、3.2.1 系統(tǒng)功能流程設(shè)計 圖3-1 系統(tǒng)功能流程圖 如圖3-1所示，本系統(tǒng)的設(shè)計流程為：先利用Jude或者ArgoUML工具畫出狀態(tài)遷移圖，該畫圖工具可以自動生成xmi或者xml文件，然后在Eclipse平臺上對已經(jīng)生成的xmi或者xml，使用java編程進行解析，找到圖中對應(yīng)的關(guān)鍵的信息，如初始狀態(tài)點集合、狀態(tài)點集合、遷移集合等等。接著將解析好的程序模型轉(zhuǎn)換成smv程序，最后用NuSMV工具對其進行驗證。具體步驟為：第一步：在Jude畫圖工具上畫出狀態(tài)遷移圖，導出xml文檔，在eclipse環(huán)境中編寫程序，對該文檔進行解析，得出解析結(jié)果。如果xml文檔有誤或者不完整，可以直接退出。這一步

46、作為一個小測驗。第二步：在ArgoUML畫圖工具上畫出狀態(tài)遷移圖，導出xmi文檔，在eclipse環(huán)境中編寫程序，對該文檔進行解析，得出解析結(jié)果，其結(jié)果包括初始狀態(tài)集合、狀態(tài)集合、遷移集合、觸發(fā)集合等。如果xmi文檔有誤或者不完整，可以直接退出。這一步作為第二個小測驗。第三步：利用操作界面，打開相應(yīng)的xmi文檔或者xml文檔，點擊“轉(zhuǎn)換”按鈕，可以將其轉(zhuǎn)換為SMV程序。第四步，對生成的SMV程序進行驗證。（通常我們要用NuSMV工具進行驗證，但是本課題將它作為后續(xù)研究內(nèi)容）。3.2.2 操作界面的設(shè)計可以利用操作界面進行打開、保存、轉(zhuǎn)換、退出等操作。轉(zhuǎn)換退出保存打開 圖3-2 操作界面的流程圖

47、 如圖3-2所示，其過程如下： 打開：可以打開計算機上的任何一個文件。本設(shè)計系統(tǒng)重點是要查找用ArgoUML和Jude畫圖工具生成的xmi和xml文檔，方便進行解析測試和轉(zhuǎn)換。轉(zhuǎn)換：當查找到xmi或者xml文檔后，點擊“轉(zhuǎn)換”，便會彈出個窗口，點擊“是”，即對上述xmi或者xml進行轉(zhuǎn)換，將其轉(zhuǎn)換為smv程序；點擊“否”，即取消轉(zhuǎn)換操作，還能再返回到打開文件的操作界面。 保存：將上述已經(jīng)轉(zhuǎn)換生成的smv程序進行保存，如果核對無誤后，可以將其保存在合適的位置，以便日后使用NuSMV工具對其進行驗證。 退出：當執(zhí)行“打來文件”、“轉(zhuǎn)換”、“保存”這些操作時，如果發(fā)現(xiàn)有誤或者有必要需要退出時，點擊“

48、退出”按鈕，會彈出個對話框，它有兩個選項，“是”和“否”。如果點擊“是”，則退出“從狀態(tài)遷移圖到SMV程序自動轉(zhuǎn)換的設(shè)計與實現(xiàn)”的整個操作界面，如果點擊“否”，則返回到上一步操作。3.3 性能需求分析實用性：提高了使用NuSMV工具使用的方便性，優(yōu)化資源，實現(xiàn)效益最大化。操作性：適用于不同水平的使用者，都可以將自己需要檢測的狀態(tài)遷移圖通過這一系列的步驟放到NuSMV工具上進行檢測。技術(shù)性：本次設(shè)計和開發(fā)應(yīng)緊跟著整個計算機發(fā)展潮流，采用先進的設(shè)計思想，利用最新的開發(fā)技術(shù)和開發(fā)工具。使系統(tǒng)能夠無論在功能設(shè)計上，還是技術(shù)實現(xiàn)上，都處于領(lǐng)先地位。適應(yīng)性良好：Java本身良好的兼容性是平臺能廣泛應(yīng)用于不

49、同計算機。系統(tǒng)采用模塊化設(shè)計，用戶可以根據(jù)自己的實際情況進行修改組合，使系統(tǒng)在不同硬件環(huán)境上都能得以應(yīng)用。第四章 系統(tǒng)設(shè)計與實現(xiàn)本章主要介紹了系統(tǒng)設(shè)計和系統(tǒng)主要功能的實現(xiàn)。包括系統(tǒng)的詳細設(shè)計與實現(xiàn)，包含狀態(tài)遷移圖轉(zhuǎn)化為xmi（xml）、對xmi（xml）進行解析、將解析后的模型轉(zhuǎn)換為smv程序、對smv進行驗證等主要功能的實現(xiàn)。4.1 狀態(tài)遷移圖轉(zhuǎn)換為xmi（xml）在ArgoUML(Jude)工具上畫出狀態(tài)遷移圖（兩種工具畫圖的方式有點不同），點擊“文件”或者“工具”下面的“導出xmi（xml）”選項，就會自動生成xmi或者xml的文檔，然后把它保存在合適的地方以供解析使用，這一部分不需要代

50、碼實現(xiàn)。4.2 對xmi（xml）進行解析4.2.1 對xmi進行解析 （1）State類：定義了狀態(tài)遷移圖中的狀態(tài)，包括在狀態(tài)圖中id、狀態(tài)名稱name、別名alias、incomings遷移集合incomings、outgoings遷移集合outgoings等屬性，以及得到修改以上屬性的函數(shù)。 （2）Transition類：定義了UML狀態(tài)圖中的遷移，包括在狀態(tài)圖中的id、源狀態(tài)source、目標狀態(tài)target、觸發(fā)trigger等屬性。表示圖中每個線段對應(yīng)的初始狀態(tài)點和終結(jié)狀態(tài)點，以及得到修改以上屬性的函數(shù)。 （3）Trigger類：表示UML狀態(tài)圖中的觸發(fā)，包括在狀態(tài)圖中id、tri

51、gger的名稱name、包含trigger的遷移集trans屬性，以及得到修改以上屬性的函數(shù)，表示狀態(tài)圖中的觸發(fā)集合。 （4）Var類：定義了狀態(tài)遷移圖中的name、value等屬性，以及得到修改以上屬性的函數(shù)。 （5）UMLStateChart類：表示UML狀態(tài)圖中所有信息，包括UML工程中的唯一id、UML工程中的name、UML工程的初始狀態(tài)initState、UML工程包含的所有狀態(tài)states、UML工程包含的所有遷移transitions、UML工程包含的所有觸發(fā)triggers等屬性。（6）CTLFactory類：表示性質(zhì)生成工廠，其中包括生成模型usc的可達性性質(zhì)、活性性質(zhì)、安

52、全性性質(zhì)。（7）UMLStateChartParser類：功能是對xmi進行解析。算法思想：對圖中的UML工程中的唯一id、UML工程中的name、UML工程的初始狀態(tài)initState、UML工程包含的所有狀態(tài)states、UML工程包含的所有遷移transitions、UML工程包含的所有觸發(fā)triggers、incomings遷移集合incomings、outgoings遷移集合outgoings等屬性進行遍歷。先找到incomings、outgoings信息，如果存在，說明有觸發(fā)存在，說明圖中有對應(yīng)的線段，遷移集合中的元素加1；否則，接著往下遍歷。如果存在某個狀態(tài)點的incomings

53、=0，說明它是初始狀態(tài)點，將它寫入初始狀態(tài)集合。具體實現(xiàn)為：先找到UML工程中的唯一id，確定是對目標xmi文檔的解析，然后找出所有UML工程中的name，確定狀態(tài)集合；查找usc性質(zhì)生成工廠；利用每個狀態(tài)點的別名找到相互之間的指向關(guān)系，確定它的入度狀態(tài)點和出度狀態(tài)點；遍歷每一個觸發(fā)和對應(yīng)的遷移關(guān)系，得到遷移集合和觸發(fā)集合；如果遍歷到某個狀態(tài)點的入度incomings=0，則將該狀態(tài)點寫入初始狀態(tài)集合initState。核心代碼：public static UMLStateChart parser(String uscPath) init(uscPath); Element usm = (El

54、ement) 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.setTr

55、ansitions(parseTransitions(usc); usc.setInitState(usc.getStateById(parseInitState(usm); generateAliasForState(usc.getInitState(); return usc; private static Map<String, Transition> parseTransitions(UMLStateChart usc) List<Node> transitionNodes = doc.selectNodes("/UML:Transitionxmi.i

56、d"); Map<String, Transition> trans = new HashMap<>(); for(Node node : transitionNodes) Element el = (Element) node; if(!isTransitionValid(el) continue; String id = el.attributeValue("xmi.id"); Trigger trigger = usc.getTrigerById(Element)el.selectSingleNode("UML:Transition.trigger/UML:SignalEvent").attributeValue("