滕飛+楊靜

摘要摘要：統(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ū)ο蟮臉藴式ＵZ言，在信息管理系統(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.

責任編輯（責任編輯：杜能鋼）