UML到Event-B的系統(tǒng)化轉(zhuǎn)換方法

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

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

0 引 言

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

1 研究現(xiàn)狀

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

2 抽象轉(zhuǎn)換方法

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

2.1 用例圖

用例圖到Event-B形式化方法的一些轉(zhuǎn)換方法已經(jīng)被提出。例如,文獻[20]介紹了將UML用例圖轉(zhuǎn)換成Event-B方法的轉(zhuǎn)換步驟?；谝陨系霓D(zhuǎn)換方法,該文基于關(guān)系的角度改進了UML用例圖到Event-B的轉(zhuǎn)換方法,對用例圖中的元素實現(xiàn)了更全面的翻譯。

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

表1 用例圖轉(zhuǎn)換規(guī)則

2.1.1 參與者和用例

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

CONSTANTS

actor1

usecase1

…

AXIOMS

axm1 : partition(ACTOR,{actor1}…)

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

END

2.1.2 關(guān) 系

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

INVARIANTS

inv1 : actor∈ACTOR

inv2 : usecase∈USECASE

inv3 : basic_relation∈{actor}→{usecase}

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

BEGIN

act1 : actor : =actor1

act2 : usecase : =usecase1

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

END

2.2 類 圖

iUML-B是一個“類似UML”的圖形前端,用于為Event-B形式化方法的面向?qū)ο蟾拍罱?。iUML-B支持類圖和狀態(tài)機圖的建模[21],在Rodin平臺中可以實現(xiàn)自動地將UML中的類圖和狀態(tài)機圖轉(zhuǎn)換成Event-B形式化方法。iUML-B應(yīng)用廣泛,許多使用iUML-B建模的研究實例已經(jīng)給出。例如,文獻[22]使用iUML-B中的類圖和狀態(tài)機圖為歐洲鐵路控制系統(tǒng)建模;文獻[23]使用iUML-B為血液透析機建模。

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

表2 類圖轉(zhuǎn)換規(guī)則

2.3 順序圖

順序圖到Event-B形式化方法的一些轉(zhuǎn)換方法已經(jīng)被提出[16]?；谝陨系霓D(zhuǎn)換方法中,順序圖在轉(zhuǎn)換成Event-B方法時,順序圖中的通信對象和消息轉(zhuǎn)換成上下文中的常量,機器中添加變量控制順序圖中消息的傳遞順序,消息傳遞的源對象以及目標對象。消息的具體傳遞過程則在機器中的事件進行展現(xiàn)。表3展示了順序圖到Event-B形式化方法的轉(zhuǎn)換規(guī)則。

表3 順序圖轉(zhuǎn)換規(guī)則

2.3.1 通信對象和消息

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

SETS

MESSAGE

CONSTANTS

message1

…

AXIOMS

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

END

2.3.2 交互過程

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

INVARIANTS

inv1 : source_obj∈OBJECT

inv2 : target_obj∈OBJECT

inv3 : message∈MESSAGE

inv4 : order∈N1

順序圖中對象之間消息的傳遞過程轉(zhuǎn)換成Event-B中的事件。順序圖中message1消息的傳遞過程轉(zhuǎn)換的事件如下所示。守衛(wèi)條件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 狀態(tài)圖

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

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

表4 狀態(tài)圖轉(zhuǎn)換規(guī)則

3 轉(zhuǎn)換方法的應(yīng)用

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

3.1 用例圖

根據(jù)電梯控制系統(tǒng)的需求描述,得到電梯控制系統(tǒng)的用例圖,如圖1所示。

圖1 電梯模型用例圖

根據(jù)上述UML用例圖到Event-B的轉(zhuǎn)換方法。抽象機器m0中的RequestElevator事件由用例圖中ElevatorUser參與者和RequestElevator用例轉(zhuǎn)換而來。在RequestElevator事件中,表示用戶請求狀態(tài)的參數(shù)any_request被創(chuàng)建,動作模塊act1-act4為表示關(guān)聯(lián)關(guān)系的變量和參數(shù)賦值。

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形式化方法的轉(zhuǎn)換,抽象電梯模型中不再進行展示,具體轉(zhuǎn)換過程將在精化模型的類圖中進行描述。精化電梯模型的類圖如圖2所示。根據(jù)電梯模型需求的描述,精化的電梯模型中抽象出電梯用戶類和維修人員,這兩個類在轉(zhuǎn)換時,則轉(zhuǎn)換成上下文中的常量,這與用例圖中類之間的泛化關(guān)系相一致。

圖2 電梯模型類圖

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

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描述了電梯響應(yīng)用戶請求的執(zhí)行過程。用戶向電梯發(fā)送請求后,電梯控制器會根據(jù)電梯的狀態(tài)判斷是否對用戶的請求進行響應(yīng)。電梯處于非故障狀態(tài),電梯控制器調(diào)度電梯運行,各樓層的傳感器持續(xù)感應(yīng)電梯,電梯控制器在接收到傳感信息后,將電梯停止在相應(yīng)的樓層。

圖3 電梯模型順序圖

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

WHEN

grd1 : order = 3

THEN

act1 : source_obj: =ElevatorController

act2 : message: =JudgeRequest

act3 : target_obj: =ElevatorController

act4 : order: =order + 1

END

3.4 狀態(tài)圖

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

圖4 電梯模型狀態(tài)機圖

根據(jù)前面介紹的轉(zhuǎn)換規(guī)則,狀態(tài)圖中的InduceElevator事件轉(zhuǎn)換的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

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

4 模型驗證方法

4.1 驗證方法

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

4.2 自動證明結(jié)果

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

圖5 模型證明結(jié)果

4.3 ProB驗證結(jié)果

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

4.4 動畫模擬

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

圖6 ProB動畫模擬狀態(tài)圖

5 結(jié)束語

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