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

1、上海大學(xué)SHANGHAIUNIVERSITY畢業(yè)設(shè)計(jì)(論文)UNDERGRADUATEPROJECT(THESIS)題目從狀態(tài)遷移圖到SMV程序自動(dòng)轉(zhuǎn)換器的設(shè)計(jì)與實(shí)現(xiàn)學(xué)院計(jì)算機(jī)工程與科學(xué)學(xué)院專業(yè)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)號(hào)學(xué)生姓名指導(dǎo)教師繆淮扣起訖日期2014.2.212014.5.30目錄摘要3ABSTRACT4第一章緒論51.1 課題研究的背景及意義51.2 相關(guān)課題國(guó)內(nèi)外現(xiàn)狀51.3 研究?jī)?nèi)容6第二章相關(guān)技術(shù)及開發(fā)工具介紹82.1 畫圖工具介紹82.1.1 ArgoUML82.1.2 Jude92.2 相關(guān)開發(fā)工具介紹102.3 開發(fā)語(yǔ)言java介紹13第三章系統(tǒng)可行性與需求分析163.1 可行

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

3、態(tài)圖和解析測(cè)試結(jié)果385.2.2 TestGenerator.xmi狀態(tài)圖和解析測(cè)試結(jié)果395.2.3 TestGenerator.xmi轉(zhuǎn)換成的smv語(yǔ)言415.2.4 mc-statechart.xmi狀態(tài)圖和解析測(cè)試結(jié)果455.2.5 mc-statechart.xmi轉(zhuǎn)換成的smv語(yǔ)言46第六章總結(jié)與展望486.1 總結(jié)486.2 展望48致談日500參考文獻(xiàn)511附錄部分源代碼清單512摘要隨著Internet的迅猛發(fā)展，當(dāng)今社會(huì)已逐漸步入信息時(shí)代。計(jì)算機(jī)軟硬件系統(tǒng)日益復(fù)雜，其正確性和可靠性已成為計(jì)算機(jī)領(lǐng)域中研究的熱點(diǎn)，在諸多方法和理論中,模型檢測(cè)以其簡(jiǎn)潔明了和自動(dòng)化程度而備受關(guān)注。

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

5、四章論述了系統(tǒng)各項(xiàng)功能的設(shè)計(jì)和實(shí)現(xiàn)。第五章論述了系統(tǒng)運(yùn)行演示。最后一章對(duì)論文進(jìn)行了總結(jié)和展望。關(guān)鍵詞：狀態(tài)遷移圖NuSMV轉(zhuǎn)換檢測(cè)上海大學(xué)畢業(yè)設(shè)計(jì)（論文）ABSTRACTWiththerapiddevelopmentoftheInternet,Today'ssocietyisgraduallyenteringtheinformationage.Withcomputerhardwareandsoftwaresystemsmoreandmorecomplex,itsvalidityandreliabilityhasbecomeahotresearchinfieldofcomputer.In

6、manymethodsandtheories,themodelcheckingisamajorconcernforitssimplicityandautomation.NuSMV,asakindofeffectivemodelcheckingtool,hasbeenmoreandmorewidelyused.ThepaperintroducesdesignandimplementationofthetoolwhichtransformsthestatetransitiondiagramintoSMVprogramthatNuSMVcanrecognize.Thistoolmakesusunde

7、rstandthestatetransitiondiagramwell,useNuSMVtoolskillfullyandmastertheSMVlanguagefully.WeneedbefamiliarwiththeJavalanguageandEclipseenvironmentfordevelopmentprocess.Throughthisprocess,whichisthetransitionfromthestatetransitiondiagramtoSMVprogram,wecanfindthattheuseprocessofNuSMVtoolsismoresimple.Att

8、hesametime,wecanimprovetheabilitytotoanalyzeandsolveproblems.Thepaperisorganizedasfollows.Chapter1discussesthesubjectresearchsignificanceandbackground,domesticandforeignresearchstatusandthemainresearchcontentofthisarticle.Chapter2discussestheuseoftechnologiesanddevelopmenttoolswhichisrelatedtothispr

9、ojectdesign.Chapter3discussesthesystem'sfeasibility,requirementsandperformanceanalysis.Chapter4dealswiththefeaturesofthesystemdesignandimplementation.Chapter5makesanintroductionaboutthesystemdebuggingandtesting.Thelastchaptersummarizesthepaperandprospects.Keywords:Statetransitiondiagram.NuSMV、tr

10、ansform>test上海大學(xué)畢業(yè)設(shè)計(jì)（論文）第一章緒論本章主要介紹課題的背景和意義以及國(guó)內(nèi)外的研究現(xiàn)狀，進(jìn)一步給出系統(tǒng)設(shè)計(jì)目標(biāo)的實(shí)現(xiàn)效果。系統(tǒng)的實(shí)現(xiàn)將有助于NuSMV：具的方便使用。1.1 課題研究的背景及意義在二十一世紀(jì)的今天，網(wǎng)絡(luò)的誕生，極大地方便了人們地溝通和交流。同時(shí)，驗(yàn)證計(jì)算機(jī)硬件系統(tǒng)、軟件系統(tǒng)或者兩者的結(jié)合是否滿足設(shè)計(jì)要求和是否正確很有意義，特別是對(duì)安全性要求很高的系統(tǒng)和商業(yè)價(jià)值很高的系統(tǒng)。也就是說(shuō)，軟件是否可信已經(jīng)成為一個(gè)國(guó)家的國(guó)防、經(jīng)濟(jì)等系統(tǒng)能否正常運(yùn)轉(zhuǎn)的重要因素之一，尤其核反應(yīng)堆控制、航空航天、鐵路信號(hào)、核電站等安全攸關(guān)的領(lǐng)域更是如此，其失誤和bug甚至崩潰可能會(huì)造

11、成生命和財(cái)產(chǎn)的無(wú)法挽回的重大損失，如何確保這些系統(tǒng)的可靠性和安全性成為計(jì)算機(jī)科學(xué)領(lǐng)域中重要研究方向。狀態(tài)遷移圖是用來(lái)描述系統(tǒng)或?qū)ο蟮臓顟B(tài)，以及導(dǎo)致系統(tǒng)或?qū)ο蟮臓顟B(tài)改變的事件，從而描述系統(tǒng)的行為。它具有直觀性、單純性。NuSMV為一種常用的模型檢驗(yàn)工具，它高效地實(shí)現(xiàn)了符號(hào)模型檢測(cè)技術(shù)，已廣泛應(yīng)用于對(duì)軟件、硬件系統(tǒng)的系統(tǒng)行為模型檢驗(yàn)。在檢驗(yàn)過(guò)程中，輸入用狀態(tài)遷移圖表示的行為模型和待檢驗(yàn)性質(zhì)，NuSMVt具就可以對(duì)系統(tǒng)行為模型是否滿足系統(tǒng)性質(zhì)進(jìn)行檢驗(yàn)并給出檢驗(yàn)結(jié)果。此研究課題的意義就在于，通過(guò)實(shí)現(xiàn)從狀態(tài)遷移圖形式的系統(tǒng)行為模型向NuSMV：具可以識(shí)別的符合SMV§法的系統(tǒng)行為模型的轉(zhuǎn)換，從

12、而使NuSMVL具的使用過(guò)程更加簡(jiǎn)單。止匕外，該課題還可以提高我們綜合使用所學(xué)課程，實(shí)際解決問(wèn)題的能力。同時(shí)，自動(dòng)轉(zhuǎn)換和檢測(cè)工具的實(shí)現(xiàn)技術(shù)有一定的學(xué)術(shù)價(jià)值和工程應(yīng)用價(jià)值。1.2 相關(guān)課題國(guó)內(nèi)外現(xiàn)狀20世紀(jì)80年代初提出的模型檢測(cè)屬于基于模型的形式化驗(yàn)證方法，由于思想相對(duì)簡(jiǎn)單和自動(dòng)化程度高，使得它廣泛用于硬件電路和網(wǎng)絡(luò)協(xié)議系統(tǒng)的驗(yàn)證，上海大學(xué)畢業(yè)設(shè)計(jì)(論文)這種方法已經(jīng)成功用于許多復(fù)雜的電路設(shè)計(jì)和通信協(xié)議驗(yàn)證。近年來(lái)，模型檢測(cè)在軟件驗(yàn)證方面也取得了一定的成績(jī)。模型驗(yàn)證器對(duì)于在學(xué)術(shù)界、產(chǎn)業(yè)界應(yīng)用模型檢測(cè)具有很大的意義。(1)國(guó)外現(xiàn)狀SMV：具是美國(guó)CM肝算機(jī)學(xué)院的L.McMillan博士于1992

13、年開發(fā)出的模型檢驗(yàn)工具軟件，它基于“符號(hào)模型檢驗(yàn)”(SymbolicModelChecking)技術(shù)，SMW此而得名。SM杯期是為了研究符號(hào)模型檢驗(yàn)應(yīng)用的可能性，而開發(fā)的一種對(duì)硬件進(jìn)行檢驗(yàn)的實(shí)驗(yàn)工具。發(fā)展到今天，SM也成為國(guó)際上廣為流行的分析有限狀態(tài)系統(tǒng)的常用工具。SMVT多個(gè)版本，如：CMU-SMVCadence-SMVNuSMV目前，國(guó)外很多學(xué)者已經(jīng)將NuSM應(yīng)用于爆炸系統(tǒng)的檢測(cè)、航空航天技術(shù)、國(guó)防等諸多領(lǐng)域，并且在歐美發(fā)達(dá)國(guó)家發(fā)展的比較迅速。(2)國(guó)內(nèi)現(xiàn)狀目前，國(guó)內(nèi)對(duì)經(jīng)典的模型驗(yàn)證器NuSMVj使用和研究不是很多，只在少數(shù)領(lǐng)域，如在PCI協(xié)議總線命令和總線信號(hào)的建模方面運(yùn)用了NuSMV這

14、制約了它的應(yīng)用以及對(duì)它的擴(kuò)展和定制。并且從狀態(tài)遷移圖到NuSMVT以識(shí)別的模型自動(dòng)轉(zhuǎn)換是重要的工作。1.3 研究?jī)?nèi)容本文主要工作內(nèi)容是從狀態(tài)遷移圖到SMV程序自動(dòng)轉(zhuǎn)換器的設(shè)計(jì)與實(shí)現(xiàn)。即設(shè)計(jì)一個(gè)自動(dòng)轉(zhuǎn)換器，完成從狀態(tài)遷移圖表示的行為模型向SMVS言描述的行為模型的轉(zhuǎn)換工作，并用程序?qū)崿F(xiàn)設(shè)計(jì)方案。其中包括對(duì)狀態(tài)遷移圖的各表示成分有清晰的理解；對(duì)$乂3勺輸入語(yǔ)言的語(yǔ)法有清晰的理解；狀態(tài)遷移圖表示的行為模型和SMVS言的對(duì)應(yīng)關(guān)系轉(zhuǎn)化關(guān)系和相關(guān)的程序?qū)崿F(xiàn)。將狀態(tài)遷移圖表示的行為模型，在NuSMVh進(jìn)行驗(yàn)證，從而真正理解狀態(tài)遷移圖，能靈活使用NuSMVC具，充分掌握SMVS言，同時(shí)也能熟練使用java語(yǔ)言

15、，熟悉Eclipse環(huán)境，通過(guò)這個(gè)過(guò)程，設(shè)計(jì)出從狀態(tài)遷移圖表示的行為模型到NuSMW以檢測(cè)的模型的自動(dòng)轉(zhuǎn)換器，從而使NuSMVT具的使用過(guò)程更加簡(jiǎn)單。具體過(guò)程包括在相應(yīng)的畫圖工具上畫出狀態(tài)遷移圖，導(dǎo)出xmi(xml)代碼，對(duì)此代碼進(jìn)行解析后，可以進(jìn)行解析測(cè)試，然后轉(zhuǎn)換成SMVS言，再用NuSMVT具對(duì)轉(zhuǎn)換的語(yǔ)言進(jìn)行驗(yàn)證。在此基礎(chǔ)上再做出一個(gè)操作界面，用來(lái)方便展示自己的研究?jī)?nèi)容。這個(gè)操作界面包括打開、轉(zhuǎn)換、保存、退出等功能。即可以打開xmi文檔或者xml文上海大學(xué)畢業(yè)設(shè)計(jì)（論文）檔，查看具體的代碼，然后可以選擇轉(zhuǎn)換按鈕，對(duì)打開的xmi或者xml文檔進(jìn)行轉(zhuǎn)換，將其轉(zhuǎn)換為smv程序；點(diǎn)擊保存按鈕，可

16、以將轉(zhuǎn)換生成的smv程序保存在自己認(rèn)為合適的位置；如果在打開文件、轉(zhuǎn)化、保存過(guò)程中，因操作有誤或者其他原因需要退出的，可以點(diǎn)擊退出按鈕，“確定”之后，即可退出。上海大學(xué)畢業(yè)設(shè)計(jì)(論文)第二章相關(guān)技術(shù)及開發(fā)工具介紹該部分主要介紹系統(tǒng)所采用的技術(shù)及開發(fā)工具，涉及畫圖的工具有ArgoUML、Jude,相關(guān)的開發(fā)工具有Eclipse,開發(fā)語(yǔ)言為java。2.1 畫圖工具介紹2.1.1 ArgoUMLArgoUML一個(gè)用于繪制UMLB的應(yīng)用軟件，它用Java構(gòu)造，并遵守開源的BSM議。因?yàn)樗旧碛蒍ava構(gòu)建的緣故，所以ArgoUML運(yùn)行在任何支持Java的平臺(tái)上。2003年，ArgoUML獲得了軟件開

17、發(fā)雜志的設(shè)計(jì)和分析工具類別的年度讀者選擇獎(jiǎng)。ArgoUM段有完全實(shí)現(xiàn)UMLB準(zhǔn)，同時(shí)它對(duì)某些圖還不能完全支持(如時(shí)序圖)。當(dāng)前的穩(wěn)定版0.24版式對(duì)0.22的一個(gè)bug修復(fù)版，它一共修正了0.22版本的172個(gè)bug。ArgoUML開發(fā)因?yàn)槿肆θ狈Χ艿接绊??；赝?Undci)'功能早在2003年就已經(jīng)提出，而迄今未實(shí)現(xiàn)。從v0.20版本開始的新特點(diǎn)：1)選中狀態(tài)下顯示文字編輯框，如“聯(lián)系(Associations)”等；在圖中支持?jǐn)?shù)據(jù)類型(DataTypes),構(gòu)造型(Stereotypes)和枚舉(Enumerations),支持CallStates,ObjectFlowState

18、s,允許在不選擇類(Class,亦稱型別)的情況下繪制狀態(tài)圖(Statechart);Criticsbrowserimprovements;Cleargridselectionandsnap。2)UML1.4-對(duì)UML1.4的擴(kuò)展特性支持增強(qiáng)；兼容androMDA質(zhì)量-數(shù)百個(gè)bug得到修正；當(dāng)前多數(shù)功能支持元素多選；支持從瀏覽樹到圖的拖拽操作，拖拽操作也適用于在瀏覽樹內(nèi)操作。其他特點(diǎn)：1)UML1.4勺全部9種圖都得到支持，緊密支持UM而準(zhǔn)；無(wú)需下載安裝，支持JWS從瀏覽器安裝運(yùn)行；支持XMI；標(biāo)準(zhǔn)的UML1.航模型(metamodel);可以多種格式導(dǎo)出UMLB:GIF,PNGPS,EPSP

19、GM以及SVG;具有圖像編輯和縮放的高級(jí)功能；平臺(tái)無(wú)關(guān)性使用Java1.5+o2)支持10種語(yǔ)言：英語(yǔ)，英語(yǔ)(EN-GB,德語(yǔ)，西班牙語(yǔ)，意大利語(yǔ)，俄語(yǔ)，法語(yǔ)，挪威語(yǔ)，葡萄牙語(yǔ)，漢語(yǔ)。Built-indesigncriticsprovideunobtrusive上海大學(xué)畢業(yè)設(shè)計(jì)(論文)reviewofdesignandsuggestionsforimprovements。3)有可擴(kuò)展的模型接口，支持OCL；正向工程(支持生成C+andC#,Java,PHP4,PHP5,Python,Ruby代碼，Ada,Delphi和SQL也支持，但不成熟)；逆向工程(導(dǎo)入jar包)。4)認(rèn)知支持(Cogni

20、tivesupport)包括動(dòng)作反應(yīng)(Reflection-in-action)、機(jī)會(huì)主義設(shè)計(jì)(Opportunisticdesign)和問(wèn)題理解和解決(ComprehensionandProblemSolving)。其中動(dòng)作反應(yīng)(Reflection-in-action)包括DesignCritics、自動(dòng)糾正(部分實(shí)現(xiàn))、待做(ToDo)列表、用戶模型(部分實(shí)現(xiàn))；機(jī)會(huì)主義設(shè)計(jì)(Opportunisticdesign)包括待做(ToDo)列表和清單(Checklists);問(wèn)題理解和解決(ComprehensionandProblemSolving)包括瀏覽器視圖預(yù)覽(Explorerpe

21、rspectives)和多重、交迭的視圖。弱點(diǎn)：1)無(wú)回退(undo)功能(或稱反悔操作)。2)對(duì)序列圖(Sequencediagrams)支持不好。3)不支持UML2.x。2.1.2JudeJUDE(JavaandUMLDevelopers'Environment),一個(gè)小巧實(shí)用的UML®模軟件，不到2M,絕對(duì)可以符合UML建模的要求，可以畫CLASSUSECAS,ESTATECHARTACTIVITY,OBJECTSEQUENCECOLLABORATIONCOMPONENTDEPLOYMENT可以導(dǎo)入JAVA源文件直接建模，也可以導(dǎo)入ROSE98勺MDLt件，可以將模型導(dǎo)

22、出成JAVA源文件，HTML®文本格式。當(dāng)然它不可能具備ROS野大型軟件的眾多強(qiáng)大的功能，但絕大部分人在絕大部分時(shí)間用的僅僅是ROSM到1%勺功能，而且還存在著版權(quán)的問(wèn)題。而JUDE是完全免費(fèi)的，軟件發(fā)布采用的SMALLRELEAS1到兩個(gè)星期就會(huì)發(fā)布一次，在不斷開發(fā)新功能的同時(shí)，滿足用戶所提出的新功能的要求和修復(fù)前一版本可能存在BUGJUD皿一個(gè)中日合作采用XP開發(fā)方式純JAVA開發(fā)的軟件，也可以說(shuō)是半個(gè)國(guó)產(chǎn)軟件(但是沒(méi)有中文版)，它功能完善，速度快，易操作，易上手，有很多優(yōu)點(diǎn)?，F(xiàn)在很多國(guó)際著名的UMLfi織的網(wǎng)站和論壇都已經(jīng)有介紹和相關(guān)下載，但很不幸的是它在中國(guó)鮮有人知?，F(xiàn)在Ju

23、de已經(jīng)更名為：astah,包括社區(qū)版和免費(fèi)版。隨著UML的擴(kuò)大，UML建模工具也越來(lái)越龐大。不過(guò)，許多功能并不是用戶所尋求的。因此，AstahProfessional(原名JUDE聽取用戶心聲，根據(jù)用戶9上海大學(xué)畢業(yè)設(shè)計(jì)（論文）需要打造，按照使用習(xí)慣設(shè)計(jì)，輕便簡(jiǎn)單，友好易用，用戶可以輕松使用它來(lái)高速建模，極大的提高了效率。AstahProfessional功能強(qiáng)大，支持UML1.4中所有圖和主要的圖形，元模（MetaModel）及屬性，全面滿足您建模所需，還集成了思維導(dǎo)圖，工程合并，協(xié)作開發(fā)等十余項(xiàng)特色功能，以及許多方便用戶的貼心實(shí)用的功能。AstahProfessional是100%純Ja

24、va應(yīng)用程序，可以跨平臺(tái)在各種主流操作系統(tǒng)中使用。支持OMGXMI標(biāo)準(zhǔn)格式，可以與其它建模工具交互模型。為方便用戶書寫Office文檔，軟件支持以MicrosoftEMF增強(qiáng)圖元拷貝粘貼至MicrosoftOffice,也可以將模型信息導(dǎo)出到OfficeExcel。軟件提供了內(nèi)容豐富的使用手冊(cè)，全面查看AstahProfessional所有的功能。簡(jiǎn)單，友好，強(qiáng)大，輕快，高效，以人為本，這就是AstahProfessional最大的特色，可以提高UML建模效率。2.2相關(guān)開發(fā)工具Eclipse介紹基本介紹：Eclipse是一個(gè)開放源代碼的、基于Java的可擴(kuò)展開發(fā)平臺(tái)。就其本身而言，它只是一個(gè)

25、框架和一組服務(wù)，用于通過(guò)插件組件構(gòu)建開發(fā)環(huán)境。幸運(yùn)的是，Eclipse附帶了一個(gè)標(biāo)準(zhǔn)的插件集，包括Java開發(fā)工具（JavaDevelopmentKit,JDQ。雖然大多數(shù)用戶很樂(lè)于將Eclipse當(dāng)作Java集成開發(fā)環(huán)境（IDE）來(lái)使用，但Eclipse的目標(biāo)卻不僅限于此。Eclipse還包括插件開發(fā)環(huán)境（Plug-inDevelopmentEnvironment,PDE,這個(gè)組件主要針對(duì)希望擴(kuò)展Eclipse的軟件開發(fā)人員，因?yàn)樗试S他們構(gòu)建與Eclipse環(huán)境無(wú)縫集成的工具。由于Eclipse中的每樣?xùn)|西都是插件，對(duì)于給Eclipse提供插件，以及給用戶提供一致和統(tǒng)一的集成開發(fā)環(huán)境而言，

26、所有工具開發(fā)人員都具有同等的發(fā)揮場(chǎng)所。這種平等和一致性并不僅限于Java開發(fā)工具。盡管Eclipse是使用Java語(yǔ)言開發(fā)的，但它的用途并不限于Java語(yǔ)言；例如，支持諸如C/C+、COBQLPHP等編程語(yǔ)言的插件已經(jīng)可用，或預(yù)計(jì)將會(huì)推出。Eclipse框架還可用來(lái)作為與軟件開發(fā)無(wú)關(guān)的其他應(yīng)用程序類型的基礎(chǔ)，比如內(nèi)容管理系統(tǒng)。10上海大學(xué)畢業(yè)設(shè)計(jì)（論文）基于Eclipse的應(yīng)用程序的一個(gè)突出例子是舊MRationalSoftwareArchitect,它構(gòu)成了舊MJava開發(fā)工具系列的基礎(chǔ)。語(yǔ)言拓展：Eclipse是著名的跨平臺(tái)的自由集成開發(fā)環(huán)境（IDE）。最初主要用來(lái)Java語(yǔ)言開發(fā)，通過(guò)安

27、裝不同的插件Eclipse可以支持不同的計(jì)算機(jī)語(yǔ)言，比如C+拜口Python等開發(fā)工具。Eclipse的本身只是一個(gè)框架平臺(tái)，但是眾多插件的支持使得Eclipse擁有其他功能相對(duì)固定的IDE軟件很難具有的靈活性。許多軟件開發(fā)商以Eclipse為框架開發(fā)自己的IDE。Eclipse最初由OTI和IBM兩家公司的IDE產(chǎn)品開發(fā)組創(chuàng)建，起始于199/4月。IBM提供了最初的Eclipse代碼基礎(chǔ)，包括Platform、JDT和PDEEclipse項(xiàng)目舊M發(fā)起，圍繞著Eclipse項(xiàng)目已經(jīng)發(fā)展成為了一個(gè)龐大的Eclipse聯(lián)盟，有150多家軟件公司參與到Eclipse項(xiàng)目中，其中包括Borland&g

28、t;RationalSoftware、RedHat及Sybase等。Eclipse是一個(gè)開放源碼項(xiàng)目，它其實(shí)是VisualAgeforJava的替代品，其界面跟先前的VisualAgeforJava差不多，但由于其開放源碼，任何人都可以免費(fèi)得到，并可以在此基礎(chǔ)上開發(fā)各自的插件，因此越來(lái)越受人們關(guān)注。隨后還有包括Oracle在內(nèi)的許多大公司也紛紛加入了該項(xiàng)目，Eclipse的目標(biāo)是成為可進(jìn)行任何語(yǔ)言開發(fā)的IDE集成者，使用者只需下載各種語(yǔ)言的插件即可。主要組成：Eclipse是一個(gè)開放源代碼的軟件開發(fā)項(xiàng)目，專注于為高度集成的工具開發(fā)提供一個(gè)全功能的、具有商業(yè)品質(zhì)的工業(yè)平臺(tái)。它主要由Eclipse

29、項(xiàng)目、Eclipse工具項(xiàng)目和Eclipse技術(shù)項(xiàng)目三個(gè)項(xiàng)目組成，具體包括四個(gè)部分組成EclipsePlatform、JDTCD用口PDEJDT支持Java開發(fā)、CDT持C開發(fā)、PD刖來(lái)支持插件開發(fā)，EclipsePlatform則是一個(gè)開放的可擴(kuò)展IDE,提供了一個(gè)通用的開發(fā)平臺(tái)。它提供建造塊和構(gòu)造并運(yùn)行集成軟件開發(fā)工具的基礎(chǔ)。EclipsePlatform允許工具建造者獨(dú)立開發(fā)與他人工具無(wú)縫集成的工具從而無(wú)須分辨一個(gè)工具功能在哪里結(jié)束，而另一個(gè)工具功能在哪里開始。插件開發(fā)：Eclipse的插件機(jī)制是輕型軟件組件化架構(gòu)。在客戶機(jī)平臺(tái)上，Eclipse使用插件來(lái)提供所有的附加功能，例如支持Ja

30、va以外的其他語(yǔ)言。已有的分離的11上海大學(xué)畢業(yè)設(shè)計(jì)（論文）插件已經(jīng)能夠支持C/C+（CDT、Perl、Ruby,Python、telnet和數(shù)據(jù)庫(kù)開發(fā)。插件架構(gòu)能夠支持將任意的擴(kuò)展加入到現(xiàn)有環(huán)境中，例如配置管理，而決不僅僅限于支持各種編程語(yǔ)言。Eclipse的設(shè)計(jì)思想是：一切皆插件。Eclipse核心很小，其它所有功能都以插件的形式附加于Eclipse核心之上。Eclipse基本內(nèi)核包括：圖形API（SWT/Jface）,Java開發(fā)環(huán)境插件（JDT）,插件開發(fā)環(huán)境（PDE）等。插件安裝的方式：插件安裝的主要方式有直接復(fù)制法、使用link文件法、使用eclipse自帶圖形界面安裝、使用dro

31、pins安裝插件、使用EclipseMacketplace。軟件開發(fā)包：EclipseSDK（軟件開發(fā)者包）是EclipsePlatform、JDT和PDE所生產(chǎn)的組件合并，它們可以一次下載。這些部分在一起提供了一個(gè)具有豐富特性的開發(fā)環(huán)境，允許開發(fā)者有效地建造可以無(wú)縫集成到EclipsePlatform中的工具。EclipseSDKiEclipse項(xiàng)目生產(chǎn)的工具和來(lái)自其它開放源代碼的第三方軟件組合而成。Eclipse項(xiàng)目生產(chǎn)的軟件以GPL發(fā)布，第三方組件有各自自身的許可協(xié)議。新版本的特點(diǎn)：1）NLSstringhover現(xiàn)在有一個(gè)OpeninPropertiesFile動(dòng)作。2）在Caller

32、模式下，調(diào)用層級(jí)（CallHierarchy）現(xiàn)在有一個(gè)在上下文菜單中有一個(gè)ExpandWithConstructors動(dòng)作。3）當(dāng)你在編輯器中輸入的時(shí)候，Java比較編輯器會(huì)更新其結(jié)構(gòu)。4）有一個(gè)新的toString（）產(chǎn)生器。5）為可覆蓋方法增加了一個(gè)OpenImplementation鏈接，可以直接打開其實(shí)現(xiàn)。6）編輯器與執(zhí)行環(huán)境一致。7）Debug視圖現(xiàn)在提供了breadcrumb（面包屑），顯示了當(dāng)前活動(dòng)的debug上下文。8）可運(yùn)行的JAR文件輸出向?qū)н€可以把所需的類庫(kù)打包進(jìn)一個(gè)要輸出的可運(yùn)行JAR文件，或打包進(jìn)與緊挨著該JAR的一個(gè)目錄中。9）當(dāng)在寫一個(gè)分配表達(dá)式（allocat

33、ionexpression）時(shí)發(fā)生補(bǔ)全操作，ch內(nèi)容助手現(xiàn)在可以提示一個(gè)類的可用構(gòu)造方法。10）如果檢測(cè)到無(wú)用代碼，編譯器現(xiàn)在可以發(fā)出警告。12上海大學(xué)畢業(yè)設(shè)計(jì)（論文）11）類庫(kù)、變量或容器入口的路徑現(xiàn)在可以是與項(xiàng)目相關(guān)的任何位置。12）在Jovadochover的頭部及Javadoc視圖中，現(xiàn)在都提供了引用其他類型和成員的鏈接。13）隨該Eclipse發(fā)行的JUnit4版本更新為4.5。14）Javadoc視圖及hovers現(xiàn)在都支持inheritDoc標(biāo)簽并給覆蓋方法增加鏈接。15）同一值的比較現(xiàn)在由編譯器檢測(cè)，默認(rèn)情況下會(huì)發(fā)出警告。2.3開發(fā)語(yǔ)言java介紹Java是由SunMicros

34、ystems公司于1995年5月推出的Java面向?qū)ο蟪绦蛟O(shè)計(jì)語(yǔ)言（以下簡(jiǎn)稱Java語(yǔ)言）和Java平臺(tái)的總稱。由JamesGosling和同事們共同研發(fā)，并在1995年正式推出。Java最初被稱為Oak,是1991年為消費(fèi)類電子產(chǎn)品的嵌入式芯片而設(shè)計(jì)的。1995年更名為Java,并重新設(shè)計(jì)用于開發(fā)Internet應(yīng)用程序。用Java實(shí)現(xiàn)的HotJava瀏覽器（支持Javaapplet）顯示了Java的魅力：跨平臺(tái)、動(dòng)態(tài)的WebInternet計(jì)算。從此，Java被廣泛接受并推動(dòng)了Web的迅速發(fā)展，常用的瀏覽器均支持Javaapplet。另一方面，Java技術(shù)也不斷更新。特點(diǎn)：1） Java語(yǔ)

35、言是易學(xué)的。Java語(yǔ)言的語(yǔ)法與C語(yǔ)言和C+1言很接近，使得大多數(shù)程序員很容易學(xué)習(xí)和使用Java。另一方面，Java丟棄了C+”很少使用的、很難理解的、令人迷惑的那些特性，如操作符重載、多繼承、自動(dòng)的強(qiáng)制類型轉(zhuǎn)換。特別地，Java語(yǔ)言不使用指針，而是引用。并提供了自動(dòng)的廢料收集，使得程序員不必為內(nèi)存管理而擔(dān)憂。2） Java語(yǔ)言是強(qiáng)制面向?qū)ο蟮?。Java語(yǔ)言提供類、接口和繼承等原語(yǔ)，為了簡(jiǎn)單起見(jiàn)，只支持類之間的單繼承，但支持接口之間的多繼承，并支持類與接口之間的實(shí)現(xiàn)機(jī)制（關(guān)鍵字為implements）。Java語(yǔ)言全面支持動(dòng)態(tài)綁定，而C+叫言只對(duì)虛函數(shù)使用動(dòng)態(tài)綁定?？傊?，Java語(yǔ)言是一個(gè)純的

36、面向?qū)ο蟪绦蛟O(shè)計(jì)語(yǔ)言。3） Java語(yǔ)言是分布式的。Java語(yǔ)言支持Internet應(yīng)用的開發(fā)，在基本的Java應(yīng)用編程接口中有一個(gè)網(wǎng)絡(luò)應(yīng)用編程接口（javanet）,它提供了用于網(wǎng)絡(luò)應(yīng)用編程的類庫(kù)，包括URLURLConnection、Socket>ServerSocket等。Java的RMI（遠(yuǎn)程方法激活）機(jī)制也是開發(fā)分布式應(yīng)用的重要手段。13上海大學(xué)畢業(yè)設(shè)計(jì)（論文）4） Java語(yǔ)言是健壯的。Java的強(qiáng)類型機(jī)制、異常處理、垃圾的自動(dòng)收集等是Java程序健壯性的重要保證。對(duì)指針的丟棄是Java的明智選擇。Java的安全檢查機(jī)制使得Java更具健壯性。5） Java語(yǔ)言是安全的。Ja

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

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

39、種特殊的對(duì)象，它必須由Thread類或其子（孫）類來(lái)創(chuàng)建。通常有兩種方法來(lái)創(chuàng)建線程：其一，使用型構(gòu)為Thread（Runnable）的構(gòu)造子將一個(gè)實(shí)現(xiàn)了Runnable接口的對(duì)象包裝成一個(gè)線程，其二，從Thread類派生出子類并重寫run方法，使用該子類創(chuàng)建的對(duì)象即為線程。值得注意的是Thread類已經(jīng)實(shí)現(xiàn)了Runnable接口，因此，任何一個(gè)線程均有它的run方法，而run方法中包含了線程所要運(yùn)行的代碼。線程的活動(dòng)由一組方法來(lái)控制。Java語(yǔ)言支持多個(gè)線程的同時(shí)執(zhí)行，并提供多線程之間的同步機(jī)制（關(guān)鍵字為synchronized）。14上海大學(xué)畢業(yè)設(shè)計(jì)(論文)(11)Java語(yǔ)言是動(dòng)態(tài)的。Ja

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

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

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

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

44、完全可行的。3.2 功能需求分析3.2.1 系統(tǒng)功能流程設(shè)計(jì)結(jié)束是測(cè)試狀態(tài)遷移圖測(cè)試結(jié)果解析出初始狀態(tài)集合、狀態(tài)集合、遷移集合“3種&能性質(zhì)轉(zhuǎn)換測(cè)試測(cè)試結(jié)果圖3-1系統(tǒng)功能流程圖如圖3-1所示，本系統(tǒng)的設(shè)計(jì)流程為：先利用Jude或者ArgoUMLX具畫出狀態(tài)遷移圖，該畫圖工具可以自動(dòng)生成xmi或者xml文件，然后在Eclipse平臺(tái)上對(duì)已經(jīng)生成的xmi或者xml,使用java編程進(jìn)行解析，找到圖中對(duì)應(yīng)的關(guān)鍵的信息，如初始狀態(tài)點(diǎn)集合、狀態(tài)點(diǎn)集合、遷移集合等等。接著將解析好的程序模型轉(zhuǎn)換成smv程序，最后用NuSMVC具對(duì)其進(jìn)行驗(yàn)證。具體步驟為：17上海大學(xué)畢業(yè)設(shè)計(jì)（論文）第一步：在Jud

45、e畫圖工具上畫出狀態(tài)遷移圖，導(dǎo)出xml文檔，在eclipse環(huán)境中編寫程序，對(duì)該文檔進(jìn)行解析，得出解析結(jié)果。如果xml文檔有誤或者不完整，可以直接退出。這一步作為一個(gè)小測(cè)驗(yàn)。第二步：在ArgoUMUB圖工具上畫出狀態(tài)遷移圖，導(dǎo)出xmi文檔，在eclipse環(huán)境中編寫程序，對(duì)該文檔進(jìn)行解析，得出解析結(jié)果，其結(jié)果包括初始狀態(tài)集合、狀態(tài)集合、遷移集合、觸發(fā)集合等。如果xmi文檔有誤或者不完整，可以直接退出。這一步作為第二個(gè)小測(cè)驗(yàn)。第三步：利用操作界面，打開相應(yīng)的xmi文檔或者xml文檔，點(diǎn)擊“轉(zhuǎn)換”按鈕，可以將其轉(zhuǎn)換為SMV?序。第四步，對(duì)生成的SMV?序進(jìn)行驗(yàn)證。（通常我們要用NuSM"

46、具進(jìn)行驗(yàn)證,但是本課題將它作為后續(xù)研究?jī)?nèi)容）。3.2.2 操作界面的設(shè)計(jì)可以利用操作界面進(jìn)行打開、保存、轉(zhuǎn)換、退出等操作。打開圖3-2操作界面的流程圖如圖3-2所示，其過(guò)程如下：打開：可以打開計(jì)算機(jī)上的任何一個(gè)文件。本設(shè)計(jì)系統(tǒng)重點(diǎn)是要查找用ArgoUMLF口Jude畫圖工具生成的xmi和xml文檔，方便進(jìn)行解析測(cè)試和轉(zhuǎn)換。轉(zhuǎn)換：當(dāng)查找到xmi或者xml文檔后，點(diǎn)擊“轉(zhuǎn)換”，便會(huì)彈出個(gè)窗口，點(diǎn)擊“是”，即對(duì)上述xmi或者xml進(jìn)行轉(zhuǎn)換，將其轉(zhuǎn)換為smv程序；點(diǎn)擊“否”，即取消轉(zhuǎn)換操作，還能再返回到打開文件的操作界面。保存：將上述已經(jīng)轉(zhuǎn)換生成的smv程序進(jìn)行保存，如果核對(duì)無(wú)誤后，可以將其保存在合適

47、的位置，以便日后使用NuSMV：具對(duì)其進(jìn)行驗(yàn)證。退出：當(dāng)執(zhí)行“打來(lái)文件”、“轉(zhuǎn)換”、“保存”這些操作時(shí)，如果發(fā)現(xiàn)有誤或者有必要需要退出時(shí)，點(diǎn)擊“退出”按鈕，會(huì)彈出個(gè)對(duì)話框，它有兩個(gè)選項(xiàng)，“是”和“否”。如果點(diǎn)擊“是”，則退出“從狀態(tài)遷移圖到SMV?序自動(dòng)轉(zhuǎn)換的設(shè)計(jì)與實(shí)現(xiàn)”的整個(gè)操作界面，如果點(diǎn)擊“否”，則返回到上一步操作。3.3 性能需求分析實(shí)用性：提高了使用NuSMV工具使用的方便性，優(yōu)化資源，實(shí)現(xiàn)效益最大18上海大學(xué)畢業(yè)設(shè)計(jì)（論文）化。操作性：適用于不同水平的使用者，都可以將自己需要檢測(cè)的狀態(tài)遷移圖通過(guò)這一系列的步驟放到NuSMV工具上進(jìn)行檢測(cè)。技術(shù)性：本次設(shè)計(jì)和開發(fā)應(yīng)緊跟著整個(gè)計(jì)算機(jī)發(fā)展

48、潮流，采用先進(jìn)的設(shè)計(jì)思想，利用最新的開發(fā)技術(shù)和開發(fā)工具。使系統(tǒng)能夠無(wú)論在功能設(shè)計(jì)上，還是技術(shù)實(shí)現(xiàn)上，都處于領(lǐng)先地位。適應(yīng)性良好：Java本身良好的兼容性是平臺(tái)能廣泛應(yīng)用于不同計(jì)算機(jī)。系統(tǒng)采用模塊化設(shè)計(jì)，用戶可以根據(jù)自己的實(shí)際情況進(jìn)行修改組合，使系統(tǒng)在不同硬件環(huán)境上都能得以應(yīng)用。19上海大學(xué)畢業(yè)設(shè)計(jì)(論文)第四章系統(tǒng)設(shè)計(jì)與實(shí)現(xiàn)本章主要介紹了系統(tǒng)設(shè)計(jì)和系統(tǒng)主要功能的實(shí)現(xiàn)。包括系統(tǒng)的詳細(xì)設(shè)計(jì)與實(shí)現(xiàn)，包含狀態(tài)遷移圖轉(zhuǎn)化為xmi(xml)、對(duì)xmi(xml)進(jìn)行解析、將解析后的模型轉(zhuǎn)換為smv程序、對(duì)smv進(jìn)行驗(yàn)證等主要功能的實(shí)現(xiàn)。4.1 狀態(tài)遷移圖轉(zhuǎn)換為xmi(xml)在ArgoUML(Jude)工具

49、上畫出狀態(tài)遷移圖(兩種工具畫圖的方式有點(diǎn)不同)，點(diǎn)擊“文件”或者“工具”下面的“導(dǎo)出xmi(xml)”選項(xiàng)，就會(huì)自動(dòng)生成xmi或者xml的文檔，然后把它保存在合適的地方以供解析使用，這一部分不需要代碼實(shí)現(xiàn)。4.2 對(duì)xmi(xml)進(jìn)行解析4.2.1 對(duì)xmi進(jìn)行解析(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目標(biāo)狀

50、態(tài)target觸發(fā)trigger等屬性。表示圖中每個(gè)線段對(duì)應(yīng)的初始狀態(tài)點(diǎn)和終結(jié)狀態(tài)點(diǎn)，以及得到修改以上屬性的函數(shù)。(3) Trigger類：表示UML犬態(tài)圖中的觸發(fā)，包括在狀態(tài)圖中idtrigger的名稱name包含trigger的遷移集trans屬性，以及得到修改以上屬性的函數(shù)，表示狀態(tài)圖中的觸發(fā)集合。(4) Var類：定義了狀態(tài)遷移圖中的namevalue等屬性，以及得到修改以上屬性的函數(shù)。(5) UMLStateChart類：表示UML犬態(tài)圖中所有信息，包括UMLX程中的唯一id、UMLX程中的nameUMLX程的初始狀態(tài)initState、UMLT程包含的所有狀態(tài)states、UML工

51、程包含的所有遷移transitions、UML工程包含的所有觸發(fā)triggers等屬性。(6) CTLFactory類：表示性質(zhì)生成工廠，其中包括生成模型usc的可達(dá)性性質(zhì)、活性性質(zhì)、安全性性質(zhì)。UMLStateChartParser類：功能是對(duì)xmi進(jìn)行解析。20上海大學(xué)畢業(yè)設(shè)計(jì)(論文)算法思想：對(duì)圖中的UMLX程中白唯一id、UMLX程中的nameUMLX程的初始狀態(tài)initState、UMLT程包含的所有狀態(tài)states、UMLX程包含的所有遷移transitions、UML工程包含的所有觸發(fā)triggers、incomings遷移集合incomings、outgoings遷移集合out

52、goings等屬性進(jìn)行遍歷。先找至Uincomings、outgoings信息，如果存在，說(shuō)明有觸發(fā)存在，說(shuō)明圖中有對(duì)應(yīng)的線段，遷移集合中的元素加1;否則，接著往下遍歷。如果存在某個(gè)狀態(tài)點(diǎn)的incomings=0,說(shuō)明它是初始狀態(tài)點(diǎn)，將它寫入初始狀態(tài)集合。具體實(shí)現(xiàn)為：先找到UMLX程中白唯一id,確定是對(duì)目標(biāo)xmi文檔的解析，然后找出所有UMLX程中的name確定狀態(tài)集合；查找usc性質(zhì)生成工廠；利用每個(gè)狀態(tài)點(diǎn)的別名找到相互之間的指向關(guān)系，確定它的入度狀態(tài)點(diǎn)和出度狀態(tài)點(diǎn)；遍歷每一個(gè)觸發(fā)和對(duì)應(yīng)的遷移關(guān)系，得到遷移集合和觸發(fā)集合；如果遍歷到某個(gè)狀態(tài)點(diǎn)的入度incomings=0,則將該狀態(tài)點(diǎn)寫入初

53、始狀態(tài)集合initState。核心代碼：publicstaticUMLStateChartparser(StringuscPath)init(uscPath);Elementusm=(Element)doc.selectSingleNode("UML:StateMachine");if(null=usm)returnnull;UMLStateChartusc=newUMLStateChart();usc.setId(usm.attributeValue("xmi.id");usc.setName(usm.attributeValue("name

54、");usc.setTriggers(parseTriggers();usc.setStates(parseStates();usc.setTransitions(parseTransitions(usc);usc.setInitState(usc.getStateById(parseInitState(usm);generateAliasForState(usc.getInitState();returnusc;privatestaticMap<String,Transition>parseTransitions(UMLStateChart21上海大學(xué)畢業(yè)設(shè)計(jì)（論文）u

55、sc)List<Node>transitionNodesdoc.selectNodes("/UML:Transitionxmi.id");Map<String,Transition>trans=newHashMap<>();for(Nodenode:transitionNodes)Elementel=(Element)node;if(!isTransitionValid(el)continue;Stringid=el.attributeValue("xmi.id");Triggertriggerusc.getTrige

56、rById(Element)el.selectSingleNode("UML:Transition.trigger/UML:SignalEvent").attributeValue("xmi.idref");Statesourceusc.getStateById(getFirstStateIdInCompositeState(Node)el.element("Transition.source").elements().get(0);Statetargetusc.getStateById(getFirstStateIdInCompos

57、iteState(Node)el.element("Transition.target").elements().get(0);Transitiont=newTransition();t.setId(id);t.setTrigger(trigger);t.setSource(source);t.setTarget(target);trigger.addTransition(t);source.addOutgoing(t);target.addIncomings(t);trans.put(id,t);returntrans;22上海大學(xué)畢業(yè)設(shè)計(jì)(論文)privatestati

58、cMap<String,State>parseStates()List<Node>singleStateNodesdoc.selectNodes("/UML:SimpleStatexmi.id");Map<String,State>states=newHashMap<>();for(Nodenode:singleStateNodes)Statestate=newState();Elementel=(Element)node;Stringid=el.attributeValue("xmi.id");state.setId(id);state.setName(el.attributeValue("name");state.setIncomings(newHashSet<Transition>(