滕飛+楊靜

摘要摘要：統(tǒng)一建模語言UML在面向?qū)ο蟮慕＜夹g(shù)中得到了廣泛應(yīng)用。但是UML模型缺乏形式化語義，難以使用數(shù)學(xué)方式對(duì)模型進(jìn)行分析和驗(yàn)證。B方法作為一種建立在嚴(yán)格數(shù)學(xué)機(jī)理上的形式化方法，將可視化UML模型轉(zhuǎn)換為B形式化規(guī)范，可以對(duì)模型進(jìn)行形式化描述和分析，確保模型的可靠性。通過研究從UML狀態(tài)圖到B形式規(guī)范的轉(zhuǎn)換規(guī)則，提出了一種基于XMI的狀態(tài)圖到B形式化規(guī)范的自動(dòng)轉(zhuǎn)換方法，并使用Java語言實(shí)現(xiàn)了自動(dòng)轉(zhuǎn)換工具UML2B。

關(guān)鍵詞關(guān)鍵詞：UML狀態(tài)圖；B方法；轉(zhuǎn)換工具；UML2B

DOIDOI：10.11907/rjdk.162480

中圖分類號(hào)：TP301文獻(xiàn)標(biāo)識(shí)碼：A文章編號(hào)文章編號(hào)：16727800（2017）001000605

0引言

需求分析是軟件定義時(shí)期的最后一個(gè)階段，工作是深入描述軟件功能和性能，確定軟件設(shè)計(jì)的限制和軟件同其它系統(tǒng)元素的接口細(xì)節(jié)[1]。統(tǒng)一建模語言（UML）是軟件分析、設(shè)計(jì)與可視化建模的工業(yè)標(biāo)準(zhǔn)[2]，使用面向?qū)ο蟮母拍钸M(jìn)行建模，在軟件開發(fā)中得到了廣泛應(yīng)用。UML狀態(tài)圖用來描述系統(tǒng)的動(dòng)態(tài)行為，它是基于對(duì)象特征相對(duì)傳統(tǒng)狀態(tài)機(jī)的變體，主要用于捕捉來自外界對(duì)象或環(huán)境的服務(wù)請(qǐng)求的某對(duì)象內(nèi)部行為的動(dòng)態(tài)特征[3]。UML用自然語言描述的語義不夠精確，沒有提供一種對(duì)UML模型進(jìn)行推理的合理機(jī)制，無法對(duì)模型的一致性、完整性、正確性進(jìn)行形式化的分析和驗(yàn)證，因此有必要對(duì)UML模型進(jìn)行形式化描述。B方法產(chǎn)生于20世紀(jì)80年代早期，由法國計(jì)算機(jī)科學(xué)家J-R Abrial在Z 語言的基礎(chǔ)上提出，是更加面向軟件開發(fā)過程的形式化方法。B方法作為一種形式化方法，可以對(duì)軟件系統(tǒng)提供無二義的、更精確的描述，使系統(tǒng)具有較高的可信度和正確性。在B方法的應(yīng)用和研究中，文獻(xiàn)[4]提出了一套從UML狀態(tài)機(jī)到B形式化規(guī)約的轉(zhuǎn)換規(guī)則。文獻(xiàn)[5]通過B方法和UML在問題對(duì)象域?qū)哟紊系慕Y(jié)合，給出了在軟件設(shè)計(jì)中提高軟件質(zhì)量的方法。文獻(xiàn)[6]做了UML狀態(tài)圖到形式化B語言轉(zhuǎn)換的實(shí)例研究。目前的研究主要以提出UML模型到B方法的轉(zhuǎn)換規(guī)則，并在案例中應(yīng)用轉(zhuǎn)換規(guī)則，驗(yàn)證轉(zhuǎn)換規(guī)則的正確性，但沒有實(shí)現(xiàn)轉(zhuǎn)換工具。直接根據(jù)UML狀態(tài)圖和B方法的語法規(guī)則實(shí)現(xiàn)轉(zhuǎn)換，過程較繁瑣，需要人工干預(yù)，難以用程序?qū)崿F(xiàn)自動(dòng)轉(zhuǎn)換。本文通過研究從UML狀態(tài)圖到B方法的轉(zhuǎn)換規(guī)則，提出了一種基于XMI的自動(dòng)轉(zhuǎn)換方法，并在此基礎(chǔ)上使用Java語言實(shí)現(xiàn)了模型轉(zhuǎn)換的原型工具UML2B。

1UML與B方法

1.1UML簡(jiǎn)介

統(tǒng)一建模語言UML（Unified Modeling Language）是一種由OMG（Object Management Group）提出的標(biāo)準(zhǔn)對(duì)象建模語言，作為支持模型化和軟件系統(tǒng)開發(fā)的圖形化語言，可以使用面向?qū)ο蟾拍钸M(jìn)行建模。UML作為一種面向?qū)ο蟮臉?biāo)準(zhǔn)建模語言，在信息管理系統(tǒng)建模領(lǐng)域得到了廣泛應(yīng)用[7]。通過相關(guān)的UML建模軟件，建立系統(tǒng)模型，可以以一種可視化的方式向開發(fā)人員和客戶呈現(xiàn)系統(tǒng)設(shè)計(jì)模型。

1.2形式化B方法簡(jiǎn)介

B方法是一種“面向模型”的數(shù)學(xué)方法，也稱B語言。利用B方法建立的模型可以使用數(shù)學(xué)方式進(jìn)行分析，從而避免需求設(shè)計(jì)中的不一致、不完整。該方法使用AMN（Abstract Machine Notation ）作為軟件開發(fā)過程中的規(guī)約、設(shè)計(jì)及實(shí)現(xiàn)語言，使程序和程序規(guī)約說明處于一個(gè)統(tǒng)一的數(shù)學(xué)框架之下[8]。B抽象機(jī)中主要包括變量、不變式、操作，可以從靜態(tài)行為和動(dòng)態(tài)行為兩個(gè)方面描述系統(tǒng)。使用B方法創(chuàng)建的形式化模型可以使用現(xiàn)有B方法支持工具，如B-Tookit、Pro B、Atelier-B等進(jìn)行分析，以提高模型的可靠性。

2模型轉(zhuǎn)換方法

2.1自動(dòng)轉(zhuǎn)換框架

本文提出的自動(dòng)轉(zhuǎn)換框架如圖1所示。

自動(dòng)轉(zhuǎn)換過程包括4個(gè)步驟：①使用UML建模軟件（如：StartUml、Rational Rose）設(shè)計(jì)UML狀態(tài)圖，并通過建模軟件自帶的插件生成對(duì)應(yīng)的XMI文檔，命名為UMLStart.xml，將其作為自動(dòng)轉(zhuǎn)換的輸入端；②設(shè)計(jì)Java類，從UMLStart.xml中提取的信息保存到對(duì)應(yīng)的Java類實(shí)例化對(duì)象中；③根據(jù)UML狀態(tài)圖和B抽象機(jī)之間的映射關(guān)系，編寫UML狀態(tài)圖到B抽象機(jī)的轉(zhuǎn)換規(guī)則，并使用Java語言實(shí)現(xiàn)轉(zhuǎn)換程序；④讀取保存在Java數(shù)據(jù)結(jié)構(gòu)中的信息，按照轉(zhuǎn)換規(guī)則生成對(duì)應(yīng)的B形式化規(guī)范，轉(zhuǎn)換結(jié)果可以在屏幕中顯示。

2.2轉(zhuǎn)換規(guī)則

UML模型與B形式化方法在語義和結(jié)構(gòu)上存在對(duì)應(yīng)關(guān)系，可以將UML狀態(tài)圖轉(zhuǎn)換為B方法中的抽象機(jī)。下面給出從狀態(tài)圖到B形式化規(guī)范的轉(zhuǎn)換規(guī)則。

規(guī)則一：狀態(tài)轉(zhuǎn)換，如表1和表2所示。狀態(tài)表示對(duì)象在生命周期的某個(gè)條件或者狀況，對(duì)象需要執(zhí)行某些活動(dòng)、滿足某些條件等，當(dāng)對(duì)象執(zhí)行了一系列活動(dòng)，或當(dāng)某個(gè)事件發(fā)生后，對(duì)象的狀態(tài)發(fā)生了變化?；緺顟B(tài)指不含子狀態(tài)的狀態(tài)，只有若干個(gè)轉(zhuǎn)移和可能的入口、出口動(dòng)作。組合狀態(tài)指包含了若干個(gè)子狀態(tài)的狀態(tài)，嵌套于組合狀態(tài)中的狀態(tài)成為子狀態(tài)[9]。本文使用抽象機(jī)中的SETS子句描述狀態(tài)圖中的狀態(tài)，用一個(gè)枚舉集合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)護(hù)條件Guard動(dòng)作 EffectXMI文檔通過元素的屬性或其子元素描述UML模型。每個(gè)模型元素都有工具給了它一個(gè)唯一的標(biāo)識(shí)號(hào)，表示在該元素的“xmi.id” 屬性中。模型元素的命名表示在該元素的“name”屬性中[12]。通過研究，可以使用元素標(biāo)簽名稱對(duì)XMI文檔進(jìn)行檢索，按照轉(zhuǎn)換規(guī)則從被檢索的標(biāo)簽中的屬性，或其子元素中提取轉(zhuǎn)換信息。在提取信息過程中，可以利用“xmi.id” 屬性值在XMI文檔中查找對(duì)應(yīng)元素。

3UML2B原型工具實(shí)現(xiàn)

本文采用Java語言在MyEclise平臺(tái)上實(shí)現(xiàn)轉(zhuǎn)換工具，主要技術(shù)包括解析XML、J2SE、MVC架構(gòu)。解析XML文件方面，有SAX、DOM等技術(shù)。SAX的全稱是Simple APIs for XML，也即XML簡(jiǎn)單應(yīng)用程序接口[13]。SAX接口的基本原理是由接口的使用者提供符合定義的處理器。XML分析時(shí)遇到特定的事件，就去調(diào)用處理器中特定事件的處理函數(shù)[14]。DOM是應(yīng)用程序訪問XML文檔的編程API，該API包含了用于XML文檔節(jié)點(diǎn)信息，修改文檔數(shù)據(jù)信息和動(dòng)態(tài)存取XML等一系列方法[15]。本文通過對(duì)比SAX和DOM的技術(shù)特點(diǎn)，采用DOM技術(shù)實(shí)現(xiàn)工具相關(guān)功能。DOM模式解析XML文件，可以將其整體讀入內(nèi)存，并轉(zhuǎn)化為一個(gè)樹型文檔，從而可以多次遍歷這顆樹并獲取節(jié)點(diǎn)信息。根據(jù)工具的業(yè)務(wù)特點(diǎn)，采用Java提供的XML解析器DOM API for Java處理XML文檔。工具包圖如圖2所示。

工具分為6個(gè)包，分別是Intput、View、UMLToJava、UMLToB、Dom、XMLParse包。Intput包用于讀取操作者輸入的UML模型。View是UML2B工具的視圖部分，包括StartPanel、ContextPanel、ValuePanel 3個(gè)類，StartPanel類顯示起始界面，操作者可以輸入所要轉(zhuǎn)換的UML模型地址。ContextPanel類用于顯示轉(zhuǎn)換中提取的UML模型信息。ValuePanel類用于顯示最后的轉(zhuǎn)換結(jié)果。UMLToJava包通過相應(yīng)的轉(zhuǎn)換規(guī)則和算法，從狀態(tài)圖對(duì)應(yīng)的XMI文檔中提取信息，并保存到相應(yīng)的Java對(duì)象中。Dom包中包括轉(zhuǎn)換信息的Java實(shí)現(xiàn)類，如表10所示。從UML模型對(duì)應(yīng)的XMI文檔中提取信息保存到對(duì)應(yīng)類的實(shí)例化對(duì)象中。

UMLToB包通過操作，保存轉(zhuǎn)換信息的Java數(shù)據(jù)結(jié)構(gòu)，按照轉(zhuǎn)換規(guī)則生成對(duì)應(yīng)的B形式化規(guī)范，完成狀態(tài)圖到B形式化規(guī)范的轉(zhuǎn)換。UML2B工具的類圖如圖3所示。

4案例應(yīng)用

下面使用UML2B工具對(duì)實(shí)例進(jìn)行轉(zhuǎn)換。這個(gè)實(shí)例是一個(gè)洗衣機(jī)的狀態(tài)圖。洗衣機(jī)的初始狀態(tài)是停止?fàn)顟B(tài)（Stop），當(dāng)用戶在有電的情況下按下開關(guān)，洗衣機(jī)進(jìn)入運(yùn)行狀態(tài)（Running），首先進(jìn)入稱重狀態(tài)（Weigh），當(dāng)重量小于等于7KG時(shí)，洗衣機(jī)開始正常工作，依次進(jìn)入清洗狀態(tài)（Washing）、漂洗狀態(tài)（Rinseing）、甩干狀態(tài)（Dry），洗滌過程結(jié)束進(jìn)入等待用戶操作狀態(tài)（Waiting）。當(dāng)重量大于7KG時(shí)，超過了洗衣機(jī)的運(yùn)行負(fù)荷，進(jìn)入警報(bào)狀態(tài)（Reporting），警報(bào)結(jié)束后進(jìn)入等待用戶操作狀態(tài)（Waiting）。當(dāng)洗衣機(jī)在運(yùn)行狀態(tài)時(shí)，用戶發(fā)出close操作，洗衣機(jī)進(jìn)入停止?fàn)顟B(tài)。洗衣機(jī)狀態(tài)如圖4所示。

按照前述的轉(zhuǎn)換框架，使用StarUML建模軟件創(chuàng)建狀態(tài)圖模型并導(dǎo)出對(duì)應(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是一個(gè)基本狀態(tài)，Running是一個(gè)組合狀態(tài)，按照規(guī)則一轉(zhuǎn)換為抽象中對(duì)應(yīng)的集合。Start是一個(gè)結(jié)束于組合狀態(tài)邊緣的轉(zhuǎn)移，按照規(guī)則三轉(zhuǎn)換為抽象機(jī)中對(duì)應(yīng)的操作。close是一個(gè)開始于組合狀態(tài)邊緣的轉(zhuǎn)移，按照規(guī)則四轉(zhuǎn)換為抽象機(jī)中對(duì)應(yīng)的操作。weighing是一個(gè)復(fù)合轉(zhuǎn)移，按照規(guī)則七轉(zhuǎn)換為抽象機(jī)中對(duì)應(yīng)的操作。Rinse、spin、stopWash、stopReport是組合狀態(tài)中子狀態(tài)間的轉(zhuǎn)移，按照規(guī)則六轉(zhuǎn)換為抽象機(jī)中對(duì)應(yīng)的操作。轉(zhuǎn)換結(jié)果在屏幕中顯示，如圖6所示。

實(shí)驗(yàn)通過一個(gè)案例，使用UML2B工具實(shí)現(xiàn)了從UML狀態(tài)圖到B形式化規(guī)范的轉(zhuǎn)換。實(shí)驗(yàn)結(jié)果驗(yàn)證了本文提出的轉(zhuǎn)換方法可行，在此方法上開發(fā)的UML2B工具可以實(shí)現(xiàn)自動(dòng)轉(zhuǎn)換功能。轉(zhuǎn)換后得到的B形式化模型可以使用現(xiàn)有的B方法工具進(jìn)行分析。

5結(jié)語

本文研究了從UML狀態(tài)圖到B方法的轉(zhuǎn)換規(guī)則，在此基礎(chǔ)上，提出了一種自動(dòng)轉(zhuǎn)換方法。著重介紹了從UML狀態(tài)圖到B形式化規(guī)范的轉(zhuǎn)換規(guī)則，以及轉(zhuǎn)換工具的主要設(shè)計(jì)思路，使用Java語言實(shí)現(xiàn)了模型轉(zhuǎn)換的原型工具UML2B。通過案例應(yīng)用表明本文提出的轉(zhuǎn)換方法可行，在此基礎(chǔ)上實(shí)現(xiàn)的原型工具UML2B可以實(shí)現(xiàn)轉(zhuǎn)換功能。

參考文獻(xiàn)參考文獻(xiàn)：

[1]塔維娜，何積豐.基于形式化方法的需求分析[J].計(jì)算機(jī)工程，2003，29（18）：107108.

[2]許卓明，顧華建，倪玉燕，等.UML類圖向OWL本體轉(zhuǎn)換工具的設(shè)計(jì)與與實(shí)現(xiàn)[J].河海大學(xué)學(xué)報(bào)，2007，（35）4：477482.

[3]姚淑珍，金茂忠.UML狀態(tài)圖的形式化建模及其分析[J].北京航空航天大學(xué)學(xué)報(bào)，2007，（33）4：472476.

[4]肖健宇，張德云，董皓，等.UML狀態(tài)機(jī)到B形式化規(guī)約轉(zhuǎn)換[J].微電子學(xué)與計(jì)算機(jī)，2005，22（8）：8084.

[5]何飛，谷建華.B方法和UML在軟件設(shè)計(jì)中的結(jié)合應(yīng)用[J].計(jì)算機(jī)工程與科學(xué)，2007，（29）1：134136.

[6]皺盛榮，孟靜，陽雪平，等.UML狀態(tài)圖到形式化B語言轉(zhuǎn)換的實(shí)例研究[J].科學(xué)技術(shù)與工程，2007，（7）24：63346338.

[7]方紅萍，陳和平.信息系統(tǒng)UML建模研究[J].計(jì)算機(jī)工程與設(shè)計(jì)，2006，（27）19：36133615.

[8]胡啟敏，薛錦云.形式化方法Designware、B的比較[J].計(jì)算機(jī)工程與應(yīng)用，2007，43（31）：9699.

[9]吳帥.UML模型圖到B方法形式規(guī)約轉(zhuǎn)換研究與應(yīng)用[D].南昌：江西師范大學(xué)，2007.

[10]TIMOTHY J GROSE，GARY C DONEY，STEPHEN A BRODSKY.精通XMI——使用XMI、XML和UML進(jìn)行Java編程[M].徐強(qiáng)，金艷紅，譯.北京：電子工業(yè)出版社，2004.

[11]熊永剛，唐慧佳.基于XMI的UML模型到XML文檔轉(zhuǎn)換實(shí)現(xiàn)[J].計(jì)算機(jī)應(yīng)用與軟件，2010，27（4）：6870.

[12]黎闖.UML交互圖到Contract規(guī)格說明的轉(zhuǎn)換及其程序?qū)崿F(xiàn)[D].廣州：暨南大學(xué)，2005.

[13]趙俊嵐.XML編程中的DOM與SAX技術(shù)[J].計(jì)算機(jī)工程，2004（30）24：7072.

[14]張迪，朱敏，張凌立.基于SAX的XML解析與應(yīng)用[J].計(jì)算機(jī)與數(shù)字工程，2008（36）7：103106.

[15]李發(fā)應(yīng).基于DOM與SAX的數(shù)據(jù)存取技術(shù)研究與實(shí)現(xiàn)[J].信息技術(shù)，2009（2）：5154.

責(zé)任編輯（責(zé)任編輯：杜能鋼）