滕飛+楊靜
摘要摘要:統(tǒng)一建模語言UML在面向?qū)ο蟮慕<夹g(shù)中得到了廣泛應(yīng)用。但是UML模型缺乏形式化語義,難以使用數(shù)學方式對模型進行分析和驗證。B方法作為一種建立在嚴格數(shù)學機理上的形式化方法,將可視化UML模型轉(zhuǎn)換為B形式化規(guī)范,可以對模型進行形式化描述和分析,確保模型的可靠性。通過研究從UML狀態(tài)圖到B形式規(guī)范的轉(zhuǎn)換規(guī)則,提出了一種基于XMI的狀態(tài)圖到B形式化規(guī)范的自動轉(zhuǎn)換方法,并使用Java語言實現(xiàn)了自動轉(zhuǎn)換工具UML2B。
關(guān)鍵詞關(guān)鍵詞:UML狀態(tài)圖;B方法;轉(zhuǎn)換工具;UML2B
DOIDOI:10.11907/rjdk.162480
中圖分類號:TP301文獻標識碼:A文章編號文章編號:16727800(2017)001000605
0引言
需求分析是軟件定義時期的最后一個階段,工作是深入描述軟件功能和性能,確定軟件設(shè)計的限制和軟件同其它系統(tǒng)元素的接口細節(jié)[1]。統(tǒng)一建模語言(UML)是軟件分析、設(shè)計與可視化建模的工業(yè)標準[2],使用面向?qū)ο蟮母拍钸M行建模,在軟件開發(fā)中得到了廣泛應(yīng)用。UML狀態(tài)圖用來描述系統(tǒng)的動態(tài)行為,它是基于對象特征相對傳統(tǒng)狀態(tài)機的變體,主要用于捕捉來自外界對象或環(huán)境的服務(wù)請求的某對象內(nèi)部行為的動態(tài)特征[3]。UML用自然語言描述的語義不夠精確,沒有提供一種對UML模型進行推理的合理機制,無法對模型的一致性、完整性、正確性進行形式化的分析和驗證,因此有必要對UML模型進行形式化描述。B方法產(chǎn)生于20世紀80年代早期,由法國計算機科學家J-R Abrial在Z 語言的基礎(chǔ)上提出,是更加面向軟件開發(fā)過程的形式化方法。B方法作為一種形式化方法,可以對軟件系統(tǒng)提供無二義的、更精確的描述,使系統(tǒng)具有較高的可信度和正確性。在B方法的應(yīng)用和研究中,文獻[4]提出了一套從UML狀態(tài)機到B形式化規(guī)約的轉(zhuǎn)換規(guī)則。文獻[5]通過B方法和UML在問題對象域?qū)哟紊系慕Y(jié)合,給出了在軟件設(shè)計中提高軟件質(zhì)量的方法。文獻[6]做了UML狀態(tài)圖到形式化B語言轉(zhuǎn)換的實例研究。目前的研究主要以提出UML模型到B方法的轉(zhuǎn)換規(guī)則,并在案例中應(yīng)用轉(zhuǎn)換規(guī)則,驗證轉(zhuǎn)換規(guī)則的正確性,但沒有實現(xiàn)轉(zhuǎn)換工具。直接根據(jù)UML狀態(tài)圖和B方法的語法規(guī)則實現(xiàn)轉(zhuǎn)換,過程較繁瑣,需要人工干預,難以用程序?qū)崿F(xiàn)自動轉(zhuǎn)換。本文通過研究從UML狀態(tài)圖到B方法的轉(zhuǎn)換規(guī)則,提出了一種基于XMI的自動轉(zhuǎn)換方法,并在此基礎(chǔ)上使用Java語言實現(xiàn)了模型轉(zhuǎn)換的原型工具UML2B。
1UML與B方法
1.1UML簡介
統(tǒng)一建模語言UML(Unified Modeling Language)是一種由OMG(Object Management Group)提出的標準對象建模語言,作為支持模型化和軟件系統(tǒng)開發(fā)的圖形化語言,可以使用面向?qū)ο蟾拍钸M行建模。UML作為一種面向?qū)ο蟮臉藴式UZ言,在信息管理系統(tǒng)建模領(lǐng)域得到了廣泛應(yīng)用[7]。通過相關(guān)的UML建模軟件,建立系統(tǒng)模型,可以以一種可視化的方式向開發(fā)人員和客戶呈現(xiàn)系統(tǒng)設(shè)計模型。
1.2形式化B方法簡介
B方法是一種“面向模型”的數(shù)學方法,也稱B語言。利用B方法建立的模型可以使用數(shù)學方式進行分析,從而避免需求設(shè)計中的不一致、不完整。該方法使用AMN(Abstract Machine Notation )作為軟件開發(fā)過程中的規(guī)約、設(shè)計及實現(xiàn)語言,使程序和程序規(guī)約說明處于一個統(tǒng)一的數(shù)學框架之下[8]。B抽象機中主要包括變量、不變式、操作,可以從靜態(tài)行為和動態(tài)行為兩個方面描述系統(tǒng)。使用B方法創(chuàng)建的形式化模型可以使用現(xiàn)有B方法支持工具,如B-Tookit、Pro B、Atelier-B等進行分析,以提高模型的可靠性。
2模型轉(zhuǎn)換方法
2.1自動轉(zhuǎn)換框架
本文提出的自動轉(zhuǎn)換框架如圖1所示。
自動轉(zhuǎn)換過程包括4個步驟:①使用UML建模軟件(如:StartUml、Rational Rose)設(shè)計UML狀態(tài)圖,并通過建模軟件自帶的插件生成對應(yīng)的XMI文檔,命名為UMLStart.xml,將其作為自動轉(zhuǎn)換的輸入端;②設(shè)計Java類,從UMLStart.xml中提取的信息保存到對應(yīng)的Java類實例化對象中;③根據(jù)UML狀態(tài)圖和B抽象機之間的映射關(guān)系,編寫UML狀態(tài)圖到B抽象機的轉(zhuǎn)換規(guī)則,并使用Java語言實現(xiàn)轉(zhuǎn)換程序;④讀取保存在Java數(shù)據(jù)結(jié)構(gòu)中的信息,按照轉(zhuǎn)換規(guī)則生成對應(yīng)的B形式化規(guī)范,轉(zhuǎn)換結(jié)果可以在屏幕中顯示。
2.2轉(zhuǎn)換規(guī)則
UML模型與B形式化方法在語義和結(jié)構(gòu)上存在對應(yīng)關(guān)系,可以將UML狀態(tài)圖轉(zhuǎn)換為B方法中的抽象機。下面給出從狀態(tài)圖到B形式化規(guī)范的轉(zhuǎn)換規(guī)則。
規(guī)則一:狀態(tài)轉(zhuǎn)換,如表1和表2所示。狀態(tài)表示對象在生命周期的某個條件或者狀況,對象需要執(zhí)行某些活動、滿足某些條件等,當對象執(zhí)行了一系列活動,或當某個事件發(fā)生后,對象的狀態(tài)發(fā)生了變化。基本狀態(tài)指不含子狀態(tài)的狀態(tài),只有若干個轉(zhuǎn)移和可能的入口、出口動作。組合狀態(tài)指包含了若干個子狀態(tài)的狀態(tài),嵌套于組合狀態(tài)中的狀態(tài)成為子狀態(tài)[9]。本文使用抽象機中的SETS子句描述狀態(tài)圖中的狀態(tài),用一個枚舉集合STATE代表基本狀態(tài),枚舉集合SUBSTATE代表子狀態(tài)。
END;表9UML狀態(tài)圖與XMI元素映射UML狀態(tài)圖XMI元素基本狀態(tài)SimpleState組合狀態(tài)CompositeState轉(zhuǎn)移Transition監(jiān)護條件Guard動作 EffectXMI文檔通過元素的屬性或其子元素描述UML模型。每個模型元素都有工具給了它一個唯一的標識號,表示在該元素的“xmi.id” 屬性中。模型元素的命名表示在該元素的“name”屬性中[12]。通過研究,可以使用元素標簽名稱對XMI文檔進行檢索,按照轉(zhuǎn)換規(guī)則從被檢索的標簽中的屬性,或其子元素中提取轉(zhuǎn)換信息。在提取信息過程中,可以利用“xmi.id” 屬性值在XMI文檔中查找對應(yīng)元素。
3UML2B原型工具實現(xiàn)
本文采用Java語言在MyEclise平臺上實現(xiàn)轉(zhuǎn)換工具,主要技術(shù)包括解析XML、J2SE、MVC架構(gòu)。解析XML文件方面,有SAX、DOM等技術(shù)。SAX的全稱是Simple APIs for XML,也即XML簡單應(yīng)用程序接口[13]。SAX接口的基本原理是由接口的使用者提供符合定義的處理器。XML分析時遇到特定的事件,就去調(diào)用處理器中特定事件的處理函數(shù)[14]。DOM是應(yīng)用程序訪問XML文檔的編程API,該API包含了用于XML文檔節(jié)點信息,修改文檔數(shù)據(jù)信息和動態(tài)存取XML等一系列方法[15]。本文通過對比SAX和DOM的技術(shù)特點,采用DOM技術(shù)實現(xiàn)工具相關(guān)功能。DOM模式解析XML文件,可以將其整體讀入內(nèi)存,并轉(zhuǎn)化為一個樹型文檔,從而可以多次遍歷這顆樹并獲取節(jié)點信息。根據(jù)工具的業(yè)務(wù)特點,采用Java提供的XML解析器DOM API for Java處理XML文檔。工具包圖如圖2所示。
工具分為6個包,分別是Intput、View、UMLToJava、UMLToB、Dom、XMLParse包。Intput包用于讀取操作者輸入的UML模型。View是UML2B工具的視圖部分,包括StartPanel、ContextPanel、ValuePanel 3個類,StartPanel類顯示起始界面,操作者可以輸入所要轉(zhuǎn)換的UML模型地址。ContextPanel類用于顯示轉(zhuǎn)換中提取的UML模型信息。ValuePanel類用于顯示最后的轉(zhuǎn)換結(jié)果。UMLToJava包通過相應(yīng)的轉(zhuǎn)換規(guī)則和算法,從狀態(tài)圖對應(yīng)的XMI文檔中提取信息,并保存到相應(yīng)的Java對象中。Dom包中包括轉(zhuǎn)換信息的Java實現(xiàn)類,如表10所示。從UML模型對應(yīng)的XMI文檔中提取信息保存到對應(yīng)類的實例化對象中。
UMLToB包通過操作,保存轉(zhuǎn)換信息的Java數(shù)據(jù)結(jié)構(gòu),按照轉(zhuǎn)換規(guī)則生成對應(yīng)的B形式化規(guī)范,完成狀態(tài)圖到B形式化規(guī)范的轉(zhuǎn)換。UML2B工具的類圖如圖3所示。
4案例應(yīng)用
下面使用UML2B工具對實例進行轉(zhuǎn)換。這個實例是一個洗衣機的狀態(tài)圖。洗衣機的初始狀態(tài)是停止狀態(tài)(Stop),當用戶在有電的情況下按下開關(guān),洗衣機進入運行狀態(tài)(Running),首先進入稱重狀態(tài)(Weigh),當重量小于等于7KG時,洗衣機開始正常工作,依次進入清洗狀態(tài)(Washing)、漂洗狀態(tài)(Rinseing)、甩干狀態(tài)(Dry),洗滌過程結(jié)束進入等待用戶操作狀態(tài)(Waiting)。當重量大于7KG時,超過了洗衣機的運行負荷,進入警報狀態(tài)(Reporting),警報結(jié)束后進入等待用戶操作狀態(tài)(Waiting)。當洗衣機在運行狀態(tài)時,用戶發(fā)出close操作,洗衣機進入停止狀態(tài)。洗衣機狀態(tài)如圖4所示。
按照前述的轉(zhuǎn)換框架,使用StarUML建模軟件創(chuàng)建狀態(tài)圖模型并導出對應(yīng)的XMI文檔,命名為UMLStart.xml,作為UML2B工具的輸入端。UMLStart.xml可以在工具界面中顯示,如圖5所示。
UML2B工具通過程序從UMLStart.xml文件提取轉(zhuǎn)換信息,保存到Java數(shù)據(jù)結(jié)構(gòu)中。根據(jù)轉(zhuǎn)換規(guī)則,Stop是一個基本狀態(tài),Running是一個組合狀態(tài),按照規(guī)則一轉(zhuǎn)換為抽象中對應(yīng)的集合。Start是一個結(jié)束于組合狀態(tài)邊緣的轉(zhuǎn)移,按照規(guī)則三轉(zhuǎn)換為抽象機中對應(yīng)的操作。close是一個開始于組合狀態(tài)邊緣的轉(zhuǎn)移,按照規(guī)則四轉(zhuǎn)換為抽象機中對應(yīng)的操作。weighing是一個復合轉(zhuǎn)移,按照規(guī)則七轉(zhuǎn)換為抽象機中對應(yīng)的操作。Rinse、spin、stopWash、stopReport是組合狀態(tài)中子狀態(tài)間的轉(zhuǎn)移,按照規(guī)則六轉(zhuǎn)換為抽象機中對應(yīng)的操作。轉(zhuǎn)換結(jié)果在屏幕中顯示,如圖6所示。
實驗通過一個案例,使用UML2B工具實現(xiàn)了從UML狀態(tài)圖到B形式化規(guī)范的轉(zhuǎn)換。實驗結(jié)果驗證了本文提出的轉(zhuǎn)換方法可行,在此方法上開發(fā)的UML2B工具可以實現(xiàn)自動轉(zhuǎn)換功能。轉(zhuǎn)換后得到的B形式化模型可以使用現(xiàn)有的B方法工具進行分析。
5結(jié)語
本文研究了從UML狀態(tài)圖到B方法的轉(zhuǎn)換規(guī)則,在此基礎(chǔ)上,提出了一種自動轉(zhuǎn)換方法。著重介紹了從UML狀態(tài)圖到B形式化規(guī)范的轉(zhuǎn)換規(guī)則,以及轉(zhuǎn)換工具的主要設(shè)計思路,使用Java語言實現(xiàn)了模型轉(zhuǎn)換的原型工具UML2B。通過案例應(yīng)用表明本文提出的轉(zhuǎn)換方法可行,在此基礎(chǔ)上實現(xiàn)的原型工具UML2B可以實現(xiàn)轉(zhuǎn)換功能。
參考文獻參考文獻:
[1]塔維娜,何積豐.基于形式化方法的需求分析[J].計算機工程,2003,29(18):107108.
[2]許卓明,顧華建,倪玉燕,等.UML類圖向OWL本體轉(zhuǎn)換工具的設(shè)計與與實現(xiàn)[J].河海大學學報,2007,(35)4:477482.
[3]姚淑珍,金茂忠.UML狀態(tài)圖的形式化建模及其分析[J].北京航空航天大學學報,2007,(33)4:472476.
[4]肖健宇,張德云,董皓,等.UML狀態(tài)機到B形式化規(guī)約轉(zhuǎn)換[J].微電子學與計算機,2005,22(8):8084.
[5]何飛,谷建華.B方法和UML在軟件設(shè)計中的結(jié)合應(yīng)用[J].計算機工程與科學,2007,(29)1:134136.
[6]皺盛榮,孟靜,陽雪平,等.UML狀態(tài)圖到形式化B語言轉(zhuǎn)換的實例研究[J].科學技術(shù)與工程,2007,(7)24:63346338.
[7]方紅萍,陳和平.信息系統(tǒng)UML建模研究[J].計算機工程與設(shè)計,2006,(27)19:36133615.
[8]胡啟敏,薛錦云.形式化方法Designware、B的比較[J].計算機工程與應(yīng)用,2007,43(31):9699.
[9]吳帥.UML模型圖到B方法形式規(guī)約轉(zhuǎn)換研究與應(yīng)用[D].南昌:江西師范大學,2007.
[10]TIMOTHY J GROSE,GARY C DONEY,STEPHEN A BRODSKY.精通XMI——使用XMI、XML和UML進行Java編程[M].徐強,金艷紅,譯.北京:電子工業(yè)出版社,2004.
[11]熊永剛,唐慧佳.基于XMI的UML模型到XML文檔轉(zhuǎn)換實現(xiàn)[J].計算機應(yīng)用與軟件,2010,27(4):6870.
[12]黎闖.UML交互圖到Contract規(guī)格說明的轉(zhuǎn)換及其程序?qū)崿F(xiàn)[D].廣州:暨南大學,2005.
[13]趙俊嵐.XML編程中的DOM與SAX技術(shù)[J].計算機工程,2004(30)24:7072.
[14]張迪,朱敏,張凌立.基于SAX的XML解析與應(yīng)用[J].計算機與數(shù)字工程,2008(36)7:103106.
[15]李發(fā)應(yīng).基于DOM與SAX的數(shù)據(jù)存取技術(shù)研究與實現(xiàn)[J].信息技術(shù),2009(2):5154.
責任編輯(責任編輯:杜能鋼)