UML狀態圖到B形式化規范的轉換實現

滕飛+楊靜

摘要摘要：統一建模語言UML在面向對象的建模技術中得到了廣泛應用。但是UML模型缺乏形式化語義，難以使用數學方式對模型進行分析和驗證。B方法作為一種建立在嚴格數學機理上的形式化方法，將可視化UML模型轉換為B形式化規范，可以對模型進行形式化描述和分析，確保模型的可靠性。通過研究從UML狀態圖到B形式規范的轉換規則，提出了一種基于XMI的狀態圖到B形式化規范的自動轉換方法，并使用Java語言實現了自動轉換工具UML2B。

關鍵詞關鍵詞：UML狀態圖；B方法；轉換工具；UML2B

DOIDOI：10.11907/rjdk.162480

中圖分類號：TP301文獻標識碼：A文章編號文章編號：16727800（2017）001000605

0引言

需求分析是軟件定義時期的最后一個階段，工作是深入描述軟件功能和性能，確定軟件設計的限制和軟件同其它系統元素的接口細節[1]。統一建模語言（UML）是軟件分析、設計與可視化建模的工業標準[2]，使用面向對象的概念進行建模，在軟件開發中得到了廣泛應用。UML狀態圖用來描述系統的動態行為，它是基于對象特征相對傳統狀態機的變體，主要用于捕捉來自外界對象或環境的服務請求的某對象內部行為的動態特征[3]。UML用自然語言描述的語義不夠精確，沒有提供一種對UML模型進行推理的合理機制，無法對模型的一致性、完整性、正確性進行形式化的分析和驗證，因此有必要對UML模型進行形式化描述。B方法產生于20世紀80年代早期，由法國計算機科學家J-R Abrial在Z 語言的基礎上提出，是更加面向軟件開發過程的形式化方法。B方法作為一種形式化方法，可以對軟件系統提供無二義的、更精確的描述，使系統具有較高的可信度和正確性。在B方法的應用和研究中，文獻[4]提出了一套從UML狀態機到B形式化規約的轉換規則。文獻[5]通過B方法和UML在問題對象域層次上的結合，給出了在軟件設計中提高軟件質量的方法。文獻[6]做了UML狀態圖到形式化B語言轉換的實例研究。目前的研究主要以提出UML模型到B方法的轉換規則，并在案例中應用轉換規則，驗證轉換規則的正確性，但沒有實現轉換工具。直接根據UML狀態圖和B方法的語法規則實現轉換，過程較繁瑣，需要人工干預，難以用程序實現自動轉換。本文通過研究從UML狀態圖到B方法的轉換規則，提出了一種基于XMI的自動轉換方法，并在此基礎上使用Java語言實現了模型轉換的原型工具UML2B。

1UML與B方法

1.1UML簡介

統一建模語言UML（Unified Modeling Language）是一種由OMG（Object Management Group）提出的標準對象建模語言，作為支持模型化和軟件系統開發的圖形化語言，可以使用面向對象概念進行建模。UML作為一種面向對象的標準建模語言，在信息管理系統建模領域得到了廣泛應用[7]。通過相關的UML建模軟件，建立系統模型，可以以一種可視化的方式向開發人員和客戶呈現系統設計模型。

1.2形式化B方法簡介

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

2模型轉換方法

2.1自動轉換框架

本文提出的自動轉換框架如圖1所示。

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

2.2轉換規則

UML模型與B形式化方法在語義和結構上存在對應關系，可以將UML狀態圖轉換為B方法中的抽象機。下面給出從狀態圖到B形式化規范的轉換規則。

規則一：狀態轉換，如表1和表2所示。狀態表示對象在生命周期的某個條件或者狀況，對象需要執行某些活動、滿足某些條件等，當對象執行了一系列活動，或當某個事件發生后，對象的狀態發生了變化。基本狀態指不含子狀態的狀態，只有若干個轉移和可能的入口、出口動作。組合狀態指包含了若干個子狀態的狀態，嵌套于組合狀態中的狀態成為子狀態[9]。本文使用抽象機中的SETS子句描述狀態圖中的狀態，用一個枚舉集合STATE代表基本狀態，枚舉集合SUBSTATE代表子狀態。

END；表9UML狀態圖與XMI元素映射UML狀態圖XMI元素基本狀態SimpleState組合狀態CompositeState轉移Transition監護條件Guard動作 EffectXMI文檔通過元素的屬性或其子元素描述UML模型。每個模型元素都有工具給了它一個唯一的標識號，表示在該元素的“xmi.id” 屬性中。模型元素的命名表示在該元素的“name”屬性中[12]。通過研究，可以使用元素標簽名稱對XMI文檔進行檢索，按照轉換規則從被檢索的標簽中的屬性，或其子元素中提取轉換信息。在提取信息過程中，可以利用“xmi.id” 屬性值在XMI文檔中查找對應元素。

3UML2B原型工具實現

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

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

UMLToB包通過操作，保存轉換信息的Java數據結構，按照轉換規則生成對應的B形式化規范，完成狀態圖到B形式化規范的轉換。UML2B工具的類圖如圖3所示。

4案例應用

下面使用UML2B工具對實例進行轉換。這個實例是一個洗衣機的狀態圖。洗衣機的初始狀態是停止狀態（Stop），當用戶在有電的情況下按下開關，洗衣機進入運行狀態（Running），首先進入稱重狀態（Weigh），當重量小于等于7KG時，洗衣機開始正常工作，依次進入清洗狀態（Washing）、漂洗狀態（Rinseing）、甩干狀態（Dry），洗滌過程結束進入等待用戶操作狀態（Waiting）。當重量大于7KG時，超過了洗衣機的運行負荷，進入警報狀態（Reporting），警報結束后進入等待用戶操作狀態（Waiting）。當洗衣機在運行狀態時，用戶發出close操作，洗衣機進入停止狀態。洗衣機狀態如圖4所示。

按照前述的轉換框架，使用StarUML建模軟件創建狀態圖模型并導出對應的XMI文檔，命名為UMLStart.xml，作為UML2B工具的輸入端。UMLStart.xml可以在工具界面中顯示，如圖5所示。

UML2B工具通過程序從UMLStart.xml文件提取轉換信息，保存到Java數據結構中。根據轉換規則，Stop是一個基本狀態，Running是一個組合狀態，按照規則一轉換為抽象中對應的集合。Start是一個結束于組合狀態邊緣的轉移，按照規則三轉換為抽象機中對應的操作。close是一個開始于組合狀態邊緣的轉移，按照規則四轉換為抽象機中對應的操作。weighing是一個復合轉移，按照規則七轉換為抽象機中對應的操作。Rinse、spin、stopWash、stopReport是組合狀態中子狀態間的轉移，按照規則六轉換為抽象機中對應的操作。轉換結果在屏幕中顯示，如圖6所示。

實驗通過一個案例，使用UML2B工具實現了從UML狀態圖到B形式化規范的轉換。實驗結果驗證了本文提出的轉換方法可行，在此方法上開發的UML2B工具可以實現自動轉換功能。轉換后得到的B形式化模型可以使用現有的B方法工具進行分析。

5結語

本文研究了從UML狀態圖到B方法的轉換規則，在此基礎上，提出了一種自動轉換方法。著重介紹了從UML狀態圖到B形式化規范的轉換規則，以及轉換工具的主要設計思路，使用Java語言實現了模型轉換的原型工具UML2B。通過案例應用表明本文提出的轉換方法可行，在此基礎上實現的原型工具UML2B可以實現轉換功能。

參考文獻參考文獻：

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

[2]許卓明，顧華建，倪玉燕，等.UML類圖向OWL本體轉換工具的設計與與實現[J].河海大學學報，2007，（35）4：477482.

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

[4]肖健宇，張德云，董皓，等.UML狀態機到B形式化規約轉換[J].微電子學與計算機，2005，22（8）：8084.

[5]何飛，谷建華.B方法和UML在軟件設計中的結合應用[J].計算機工程與科學，2007，（29）1：134136.

[6]皺盛榮，孟靜，陽雪平，等.UML狀態圖到形式化B語言轉換的實例研究[J].科學技術與工程，2007，（7）24：63346338.

[7]方紅萍，陳和平.信息系統UML建模研究[J].計算機工程與設計，2006，（27）19：36133615.

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

[9]吳帥.UML模型圖到B方法形式規約轉換研究與應用[D].南昌：江西師范大學，2007.

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

[11]熊永剛，唐慧佳.基于XMI的UML模型到XML文檔轉換實現[J].計算機應用與軟件，2010，27（4）：6870.

[12]黎闖.UML交互圖到Contract規格說明的轉換及其程序實現[D].廣州：暨南大學，2005.

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

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

[15]李發應.基于DOM與SAX的數據存取技術研究與實現[J].信息技術，2009（2）：5154.

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