UML到Event-B的系統化轉換方法

耿 雪,鄒盛榮,劉曉瑩,姚聚義

(揚州大學 信息工程學院,江蘇 揚州 225009)

0 引 言

UML在軟件建模行業應用普及[1],以圖形化的方式幫助開發人員直觀地理解系統的需求。在面向對象的軟件開發中,UML已經成為事實上的建模標準[2]。但是,實際上UML是一種半形式化的建模語言,存在不精確性[3],無法進行形式化的驗證[4]。而形式化方法是一種嚴格基于數學的特種技術,可以在安全性要求較高的系統中進行驗證。形式化方法的研究有很多。例如Z方法、B方法、Event-B方法等[5]。B方法是比較熱門和易于使用的形式化方法[6],Event-B是最新的B方法[7],具有精確的語義[8]。但是Event-B形式化方法基于大量的數學邏輯謂詞,對于軟件需求分析人員來說難以理解和應用。鑒于UML不精確而Event-B方法雖精確不太易懂,將UML與Event-B相結合是一直以來研究的課題[9]。

1 研究現狀

UML與形式化方法的結合已有一些研究。例如,文獻[10]中評估了B模型和UML-B模型,UML-B模型與Event-B模型的可理解性,評估結果表明半形式化和形式化方法的結合促進了參與者對于模型問題域的理解。Event-B形式化方法到UML的一些轉換方法已經被提出[11]。UML到Event-B形式化方法的轉換方法也有一些被提出。例如,文獻[12]提出了在元模型層自動地將UML圖轉換成Event-B形式化方法。文獻[13]提出了活動圖到Event-B形式化方法的轉換。根據類圖到Event-B形式化方法的轉換,該方法被應用在了歐洲鐵路信號系統中[14]。文獻[15-16]提出了順序圖到Event-B形式化方法的轉換。文獻[17]提出了協作圖、狀態圖到B形式化方法的轉換。但是上述所提到的轉換方法都是基于UML 14種圖的零散個別圖到Event-B形式化方法的轉換,沒有形成系統的轉換方法。基于上述UML 14種圖的零散的轉換方法,在轉換的過程中,可能會存在轉換的不一致問題[18]和轉換沖突問題,難以應用在實際的軟件開發過程中。因此,對于UML到Event-B形式化方法的轉換有必要加以系統化的研究。筆者認為系統化地將UML轉換成Event-B形式化方法存在許多優點:一方面,軟件開發人員不僅可以依據圖形化的方式直觀理解系統的需求,而且可以使得UML精確化,易于軟件從業人員的使用;另一方面,將UML轉換成Event-B形式化方法,可以在軟件設計的早期進行形式化的驗證,提高軟件設計的可靠性,降低在軟件開發后期因解決缺陷和錯誤所需付出的高額代價和成本。同時,也有利于形式化方法的普及和應用。

2 抽象轉換方法

一般的軟件系統是中型系統,代碼量在5 000行到5萬行之間,這種中型系統完全可以只選擇UML的用例圖、類圖、順序圖和狀態圖這四種圖就能夠很好地表達出來[19]。在軟件的需求分析階段,用例圖抽象地描述了系統的功能,對系統中的哪些用戶實現系統中的哪些功能進行建模,即為軟件產品本身和軟件產品的使用者之間建模。類圖是使用最廣泛的UML圖,可以應用于軟件開發的各個階段,在每個階段的抽象程度和詳細程度不同。類圖為系統的靜態結構進行建模,描述了系統中的元素以及這些元素之間的關系。UML中的狀態圖不僅可以詳細描述實體對象和整個系統的狀態,同時也可以描述狀態轉換過程中觸發狀態轉換的事件,以及系統中的實體對象在每個狀態中表現出的行為。UML中的順序圖描述了系統中實體對象之間的交互過程。可以對用例圖中用例的詳細執行過程進行描述,即對系統中的復雜功能模塊的具體交互實現過程進行詳細的展示。有了上述的四種圖,軟件生命周期的需求獲取、分析、設計、詳細設計就完全表達清楚。為了系統地將UML轉換成Event-B形式化方法,基于上述所提到的四種UML圖,該文提出了一種UML到Event-B形式化方法的轉換方法。以表格的形式展示了UML圖中的各元素與Event-B中的各元素之間的對應關系,并給出了UML到Event-B形式化方法的轉換步驟。最后通過將該系統化的轉換方法應用到電梯控制系統中,實現了電梯控制系統的UML圖到Event-B形式化方法的轉換,并基于Rodin平臺為電梯控制系統建模,對于模型中產生的證明義務進行解除。使用ProB提供的證明器對所創建的模型進行檢驗,確保沒有死鎖、不變量違規等問題。基于該電梯系統的實例研究,證明了該系統性的轉換方法的可行性和有效性。

2.1 用例圖

用例圖到Event-B形式化方法的一些轉換方法已經被提出。例如,文獻[20]介紹了將UML用例圖轉換成Event-B方法的轉換步驟。基于以上的轉換方法,該文基于關系的角度改進了UML用例圖到Event-B的轉換方法,對用例圖中的元素實現了更全面的翻譯。

用例圖中的參與者和用例轉換成上下文中的常量。用例圖中的各種關系則轉換為Event-B中的事件。其中,關聯關系和擴展關系轉換成抽象機器中的事件。泛化關系和包含關系則通過Event-B的精化機制實現。特別的,如果是參與者元素構成的泛化關系,則在擴展的上下文中添加公理表示參與者之間的泛化關系。如果是用例元素構成的泛化關系,則在精化的機器中添加事件表示用例之間的泛化關系。表1展示了用例圖到Event-B方法的轉換規則。

表1 用例圖轉換規則

2.1.1 參與者和用例

將用例圖中的參與者和用例轉換成Event-B中的常量,并在上下文中分別創建表示參與者和用例的集合ACTOR,USECASE。添加公理聲明上述的常量的類型。

CONSTANTS

actor1

usecase1

…

AXIOMS

axm1 : partition(ACTOR,{actor1}…)

axm2 : partition(USECASE,{usecase1}...)

END

2.1.2 關 系

用例圖中的關系都可以轉換成Event-B中的事件。用例圖中的關聯關系轉換成Event-B事件的具體過程展示如下:首先,抽象機器中需要創建變量actor,usecase以及basic_relation分別表示用例圖中的參與者、用例和關聯關系。其次,在不變量中聲明上述三個變量的類型,其中,basic_relation聲明為actor到usecase之間的映射關系,表示構成該關聯關系的參與者和用例。Event-B的機器中表示關聯關系的變量聲明如下所示:

INVARIANTS

inv1 : actor∈ACTOR

inv2 : usecase∈USECASE

inv3 : basic_relation∈{actor}→{usecase}

最后,在Event-B中的機器中創建事件表示關聯關系。如下所示的usecase1事件表示參與者actor1和用例usecase1之間的關聯關系。事件的動作模塊act1-act3對表示參與者、用例以及關聯關系的變量賦值。用例圖中的其他關系與關聯關系轉換成Event-B形式化方法類似。特別的,由參與者構成的關聯關系在上下文中添加公理進行表示。

BEGIN

act1 : actor : =actor1

act2 : usecase : =usecase1

act3 : basic_relation:∈{actor1}→{usecase1}

END

2.2 類 圖

iUML-B是一個“類似UML”的圖形前端,用于為Event-B形式化方法的面向對象概念建模。iUML-B支持類圖和狀態機圖的建模[21],在Rodin平臺中可以實現自動地將UML中的類圖和狀態機圖轉換成Event-B形式化方法。iUML-B應用廣泛,許多使用iUML-B建模的研究實例已經給出。例如,文獻[22]使用iUML-B中的類圖和狀態機圖為歐洲鐵路控制系統建模;文獻[23]使用iUML-B為血液透析機建模。

iUML-B中的類圖提供了可視化建模數據關系的方法。類圖中的類、屬性和關系與Event-B中的常量、變量等元素相關聯。特別的,類圖中的類還可以與Event-B中的集合元素相關聯。在轉換的過程中,可以對這些轉換而來的元素添加公理或不變量進行約束。類中的方法轉換成Event-B中的事件,事件的動作模塊表示了方法的具體執行過程。表2展示了iUML-B中類圖到Event-B形式化方法的轉換規則。

表2 類圖轉換規則

2.3 順序圖

順序圖到Event-B形式化方法的一些轉換方法已經被提出[16]。基于以上的轉換方法中,順序圖在轉換成Event-B方法時,順序圖中的通信對象和消息轉換成上下文中的常量,機器中添加變量控制順序圖中消息的傳遞順序,消息傳遞的源對象以及目標對象。消息的具體傳遞過程則在機器中的事件進行展現。表3展示了順序圖到Event-B形式化方法的轉換規則。

表3 順序圖轉換規則

2.3.1 通信對象和消息

順序圖中的消息轉換成上下文中的常量,上下文中添加表示消息的集合MESSAGE,公理中聲明表示消息的常量為集合MESSAGE中的元素,轉換過程如下所示。類似的,通信對象也轉換成上下文中的常量。

SETS

MESSAGE

CONSTANTS

message1

…

AXIOMS

partition : partition(MESSAGE,{message1},…)

END

2.3.2 交互過程

機器中創建變量source_obj,target_obj,message和order分別表示消息傳遞的源對象、目標對象、待傳遞的消息以及消息的傳遞順序。機器中上述變量的類型聲明如下所示:

INVARIANTS

inv1 : source_obj∈OBJECT

inv2 : target_obj∈OBJECT

inv3 : message∈MESSAGE

inv4 : order∈N1

順序圖中對象之間消息的傳遞過程轉換成Event-B中的事件。順序圖中message1消息的傳遞過程轉換的事件如下所示。守衛條件grd1通過判斷變量order的值確定消息的傳遞順序是否正確。動作模塊act1-act4明確了消息傳遞的源對象、目標對象和待傳遞的消息。

WHEN

grd1 : order=1

THEN

act1 : message: =message1

act2 : source_obj: =object1

act3 : target_obj: =object2

act4 : order: =order+1

END

2.4 狀態圖

iUML-B同樣也支持狀態機圖建模。狀態機圖轉換成Event-B方法時,存在兩種轉換方式。一種是基于Enumeration translation的轉換方式;另一種是基于variables translation的轉換方式[24]。兩種轉換方式最大的區別在于是否自動產生上下文,由于產生上下文的轉換方式更容易理解,因此,該文選擇的是基于Enumeration translation的轉換方式以便于理解和應用。

在使用iUML-B為狀態機圖建模時。狀態機圖中的狀態轉換成常量,轉換可以鏈接到Event-B中的事件,事件的發生會觸發狀態的改變,動作語句表示系統的具體操作。狀態機圖中的復合狀態則通過Event-B的精化機制實現,抽象的上下文會通過Event-B方法中的擴展關系擴展出新的上下文,復合狀態在擴展后的上下文中轉換成常量。表4中明確了狀態機圖到Event-B方法的轉換規則。

表4 狀態圖轉換規則

3 轉換方法的應用

電梯是對可靠性和安全性要求較高的實時硬件系統。電梯控制系統是安全領域最常見的例子[25],大批學者在安全控制領域中常常以電梯控制系統作為研究實例[26-27],而且電梯是一個中型化的系統[28],適合于該系統化的轉換方法。本節將以電梯控制系統作為實例應用在該系統化的轉換方法中,以驗證該方法的可行性和可靠性。用戶請求使用電梯時,電梯控制器根據用戶請求的樓層信息調度電梯向上或向下運行,電梯運行過程中,傳感器始終處于感應狀態。電梯控制器在接收到傳感器發送的傳感信息后,控制電梯停止在相應樓層,電梯停止在該樓層后,電梯門將在一定的時間間隔內處于打開狀態,等待用戶進出電梯。

3.1 用例圖

根據電梯控制系統的需求描述,得到電梯控制系統的用例圖,如圖1所示。

圖1 電梯模型用例圖

根據上述UML用例圖到Event-B的轉換方法。抽象機器m0中的RequestElevator事件由用例圖中ElevatorUser參與者和RequestElevator用例轉換而來。在RequestElevator事件中,表示用戶請求狀態的參數any_request被創建,動作模塊act1-act4為表示關聯關系的變量和參數賦值。

ANY

any_request

WHERE

grd1 : any_request∈ BOOL

THEN

act1 : actor: =ElevatorUser

act2 : usecase: =RequestElevator

act3 : association :∈ {ElevatorUser} → {RequestElevator}

act4 : control_request: =any_request

END

3.2 類 圖

類圖到Event-B形式化方法的轉換,抽象電梯模型中不再進行展示,具體轉換過程將在精化模型的類圖中進行描述。精化電梯模型的類圖如圖2所示。根據電梯模型需求的描述,精化的電梯模型中抽象出電梯用戶類和維修人員,這兩個類在轉換時,則轉換成上下文中的常量,這與用例圖中類之間的泛化關系相一致。

圖2 電梯模型類圖

User類中的RequestMaintenance方法表示用戶請求維修電梯,轉換成的事件如下所示。該事件的動作模塊act1-act2語句對變量control_request, Elevator_state進行賦值,表示電梯處于故障狀態且無法響應用戶的請求。

ANY

this_User // generated class instance

WHERE

instanceType_this_User_User : this_User ∈ User

THEN

act1 : control_request :∈ Elevator → {FALSE}

act2 : Elevator_state :∈ Elevator → {fault}

END

3.3 順序圖

圖3描述了電梯響應用戶請求的執行過程。用戶向電梯發送請求后,電梯控制器會根據電梯的狀態判斷是否對用戶的請求進行響應。電梯處于非故障狀態,電梯控制器調度電梯運行,各樓層的傳感器持續感應電梯,電梯控制器在接收到傳感信息后,將電梯停止在相應的樓層。

圖3 電梯模型順序圖

JudgeRequest消息的傳遞過程轉換成的事件如下所示。首先,守衛條件grd1會根據變量order的值判斷消息的傳遞順序。其次,動作act1-act3明確了傳遞的消息為JudgeRequest,消息傳遞的源對象和目標對象都是電梯控制器。最終,act4將order的值增一,表示順序圖中該消息傳遞過程的結束。

WHEN

grd1 : order = 3

THEN

act1 : source_obj: =ElevatorController

act2 : message: =JudgeRequest

act3 : target_obj: =ElevatorController

act4 : order: =order + 1

END

3.4 狀態圖

精化的電梯模型狀態機圖如圖4所示,主要對運行狀態和故障狀態進行精化。電梯在運行過程中,電梯控制器調度電梯向上或向下運行,傳感器始終在感應電梯是否到達相應的樓層。所以,running狀態中添加了dispatch和induce狀態。電梯處于故障狀態時,安保人員在接收到維修請求后會進行維修。因此,在故障狀態中,添加了maintenance狀態表示電梯被安保人員維修。

圖4 電梯模型狀態機圖

根據前面介紹的轉換規則,狀態圖中的InduceElevator事件轉換的Event-B方法中的事件如下所示:

ANY

any_Induce

WHERE

isin_running : Elevator_Statemachine = running

any_Induce_type : any_Induce∈ BOOL

THEN

act1 : isInduce : =any_Induce

enter_induce : Elevator_running: =induce

END

電梯在運行過程中,電梯傳感器始終處于感應狀態,以此感應電梯是否到達該樓層。該事件中添加了BOOL類型的參數any_Induce,以參數any_Induce的值判斷電梯傳感器是否感應到電梯的到達,事件的守衛條件isin_running和動作act1明確了電梯處于被感應狀態。

4 模型驗證方法

4.1 驗證方法

該文使用了上述所提到的UML到Event-B的系統轉換方法在Rodin平臺中為電梯控制系統建模。Rodin平臺中自帶的證明器和Atelier B等提供的外部證明器對模型中產生的證明義務進行解除。但是盡管模型中產生的證明義務全部得到了解除,這也并不能保證模型中的事件在動態的運行過程中不會出現死鎖問題。因此,又使用了ProB[29]提供的模型檢查工具,補充驗證了模型的定理證明技術,提高了模型的可靠性和精確性。此外,ProB還提供了一個動畫模擬的功能,可以動態地模擬模型中事件的執行過程,以驗證模型中可能會出現的問題,增強模型的可讀性和可理解性。因此,借助于ProB的動畫模擬功能,動態地模擬了電梯模型中事件的執行過程。

4.2 自動證明結果

基于Rodin平臺將電梯控制系統的UML圖轉換成Event-B形式化方法后,模型中產生的證明結果如圖5所示。圖5(a)中顯示抽象機器m0中共產生了26條證明義務,圖5(b)中顯示精化機器m1中產生了17條證明義務,這些證明義務均已通過自動證明和交互式證明得到了解除,模型證明的結果驗證了抽象轉換方法的可行性。

圖5 模型證明結果

4.3 ProB驗證結果

圖5(c)中展示了電梯模型中的事件在動態執行過程中,共經歷了45個變遷,在這些變遷轉換的過程中,ProB證明器排除了模型中可能會出現的死鎖等相關問題,提高了模型的精確性,驗證了抽象轉換方法的正確性。

4.4 動畫模擬

ProB可以動態地模擬模型中事件的執行過程以及系統當前所處的狀態,能夠被觸發的事件以加粗的箭頭顯示,加粗顯示的狀態表示系統當前的狀態。圖6(a)中顯示系統當前的狀態為idle,加粗顯示的事件為RequestElevator,即用戶可以請求使用電梯,但是由于維修保養等其他外部因素,電梯可能無法響應用戶的請求,因此,ReponseRequest事件觸發的前提是ReuqestElevator事件以參數TRUE觸發。ReponseRequest事件被觸發后,圖6(b)中顯示running,dispatch和induce狀態均被選中,其中,running狀態中添加了不變量Elevator_door=FALSE,保證電梯門在電梯運行過程中處于關閉狀態。電梯控制器在收到了傳感器發送的感應信息后,控制電梯停止在該樓層。因此,StopElevatorAtFloor事件觸發的前提是InduceElevator事件以參數TRUE觸發。電梯停止后,即StopElevatorAtFloor事件觸發后,圖6(c)中顯示電梯處于stop狀態。由于電梯發生故障的不確定性,所以RequestMaintenance事件在任何狀態下都可以被觸發,圖6(d)中顯示了該事件被觸發后,fault狀態被選中,變量control_request的值為FALSE,表示電梯處于故障狀態下,無法響應用戶的請求。

圖6 ProB動畫模擬狀態圖

5 結束語

該文提出的轉換方法系統地將半形式化建模語言(UML)轉換成Event-B形式化方法。該轉換方法將UML與Event-B形式化方法結合帶來了許多優點。一方面,使UML精確化,可以在軟件設計的早期對所建立的模型進行形式化的驗證,提高軟件設計的可靠性和準確性,有利于軟件從業人員的使用。另一方面,增強了形式化方法的可理解性和可讀性,有利于形式化方法的推廣和應用。采用了四種圖系統地將UML轉換成Event-B形式化方法,一般的中型系統采用這四種圖就可以很好地表達清楚。對于復雜的特殊系統建模時可能需要添加其它的UML圖去補充。例如,對于實時嵌入式系統,可能需要添加時間圖進行補充。將來,可以對轉換的方法提出改進,實現更全面的將UML圖轉換成Event-B形式化方法。