基于時間自動機的UML模型轉換與驗證研究

姬莉霞， 馬建紅

(鄭州大學軟件技術學院 河南鄭州450002)

0 引言

基于模型的系統(tǒng)設計方法已經(jīng)得到廣泛的研究與應用，UML(unified modeling language)是一種面向對象的建模語言，運用統(tǒng)一的、標準化的標記和定義實現(xiàn)對軟件系統(tǒng)進行面向對象的描述和建模，是應用最廣泛的軟件建模語言，被業(yè)界稱為軟件分析和設計的標準語言．但UML是非形式化的，無法對其模型進行形式化分析和驗證，很難保證系統(tǒng)建模的安全性和正確性．形式化方法［1］是一種為硬件和軟件系統(tǒng)提供精確規(guī)約、設計和驗證的嚴格的數(shù)學技術和方法．為保證建模的正確性，對系統(tǒng)模型進行形式化驗證十分必要．將系統(tǒng)的UML模型轉換為形式化模型進行驗證的方法是軟件工程領域研究的熱點［2］．

模型驗證是一種應用非常廣泛的形式化驗證技術，將UML與模型驗證技術相結合能夠有效避免軟件設計錯誤，保證建模的正確性．本文結合國內(nèi)外有關研究，提出一種將UML模型轉換為時間自動機模型并進行驗證的方法．首先將非形式化的UML類和狀態(tài)機圖轉換為形式化的描述邏輯，接著基于元模型的轉換思想，結合UML類和狀態(tài)機語義抽象出UML元模型，同時根據(jù)時間自動機的形式化語義構造時間自動機元模型，通過模型轉換語言ATL構造兩者之間的轉換映射規(guī)則，實現(xiàn)從UML模型到時間自動機模型的轉換，并將轉換得到的時間自動機模型在模型驗證工具Uppaal中進行形式化驗證，最后結合自動取款機(auto trade machine，ATM)對該方法進行實例研究和分析．

1 模型驗證方法

模型驗證的基本思想是采用狀態(tài)空間搜索來驗證給定的計算模型是否滿足某種時態(tài)邏輯公式所表示的特定性質．在模型驗證過程中，使用有窮狀態(tài)模型建模，用某種時態(tài)邏輯公式表示性質規(guī)約，然后通過有效的搜索來驗證所建立的模型是否滿足該性質規(guī)約，這個問題是可判定的［3］．與其他形式化方法比較，模型驗證的優(yōu)點非常顯著，它有完整的數(shù)學理論基礎，適用于軟件工程、通信協(xié)議、嵌入式系統(tǒng)等多種領域．

Uppaal［4－5］是一種常用的實時系統(tǒng)模型驗證工具，主要通過快速搜索機制來驗證系統(tǒng)規(guī)范和可達性，其主要優(yōu)點表現(xiàn)為高效性和便捷性．它適用于可以被描述為非確定的并行過程的時間自動機積的系統(tǒng)，已成功應用于多個領域．Uppaal使用簡化的CTL(computational tree logic)描述系統(tǒng)模型需要滿足的性質［4，6］，它可以描述系統(tǒng)的安全性和活躍性，使用p和q表示系統(tǒng)的性質，則Uppaal中驗證性質可表示為

p－－＞q表示通往，p－－＞q為真，當且僅當在轉換系統(tǒng)中存在從p到q的序列．

E＜＞p表示可能的，也就是某些路徑中存在狀態(tài)滿足p，E＜＞p為真，當且僅當在轉換系統(tǒng)中從初始狀態(tài)s0開始存在一個序列s0→…→p．

A［］p表示必然的，即所有路徑的所有狀態(tài)都滿足p，等價于not E＜＞not p．

E［］p表示潛在必然的，即某些路徑中所有狀態(tài)滿足p，在一個轉換系統(tǒng)中，E［］p為真，當且僅當存在一個序列s0→…→si→…，使得p在所有狀態(tài)si中有效．

A＜＞p表示最終的，即所有路徑中都有狀態(tài)滿足p，等價于not E［］not p．

2 構建UML的形式化語義

UML是非形式化的，為了對其進行有效的驗證，必須給出精確的形式化語義［7］．本文研究UML的一種輕量級形式化描述，即針對待解決問題忽略一些UML模型構造子，但這些處理不會對UML的概念語義一致性產(chǎn)生影響．在構建UML的形式化語義之前，參考文獻［7］的做法，先做出如下一些約定．

2．1 規(guī)約

1)在本文方法中，一個UML模型中主要包含類和狀態(tài)機圖．類不支持操作調(diào)用和子類，其靜態(tài)結構由類圖描述，其動態(tài)行為被定義為行為的狀態(tài)機．

2)UML為建模提供了2種同步機制:通過信號通信或者對象在狀態(tài)機中的正交區(qū)域通信，本文采用第1種方法，即對象之間通過使用信號進行通信，信號可以關聯(lián)參數(shù)．

3)在執(zhí)行語義上，同一時間最多有一個完成轉換(沒有明確觸發(fā)的轉換)可以被觸發(fā)，這個限制保證每一步驟最多有一個區(qū)域改變狀態(tài)，這有利于簡單轉換算法的實施．

4)UML允許執(zhí)行連續(xù)的活動狀態(tài)，但本文不支持此做法，因為模型檢查工具將會離散地執(zhí)行模型．

5)不支持歷史偽態(tài)、交叉或連接偽態(tài)、進入或者退出活動狀態(tài)．

2．2 狀態(tài)機語義

狀態(tài)機包含狀態(tài)和狀態(tài)之間的轉換，參考文獻［7－8］構造狀態(tài)機的形式化語義．

定義1 H=〈∑s，∑i，∑ch，∑f，∑c，R，top，↘〉是一個狀態(tài)層次當且僅當↘∑cR∪R ∑，并且〈∑∪R，↘〉是樹根，它的樹葉集合是∑∑c．這里∑是狀態(tài)集合，它包含簡單狀態(tài)集合∑s、開始偽態(tài)集合∑i、選擇偽態(tài)集合∑ch、結束狀態(tài)集合∑f和復合狀態(tài)集合∑c;R是有限域集合;子關系↘表示，如果復合狀態(tài)c的一個域r直接包含一個狀態(tài)s，那么c↘r并且r↘s．

定義2 在給定狀態(tài)層次上的一個轉換是一個5元組，

其中，s是轉換的源狀態(tài)，記為source(t);e是轉換的觸發(fā)條件，記為trigger(t);g是轉換的衛(wèi)士(約束)條件，記為guard(t);a是轉換觸發(fā)的更新動作，記為effect(t);S'是轉換的目標集合，記為target(t)．

在UML圖形表示中，轉換被表示為從源狀態(tài)source(t)到目標狀態(tài)target(t)的箭頭．轉換伴有文本標簽:trigger［guard］/effect，即“觸發(fā)［衛(wèi)士］/動作”．一個轉換只有在其觸發(fā)事件被調(diào)度時才能發(fā)生，觸發(fā)trigger(t)是一個信號，轉換通過接收信號(完成轉換接收特殊符號ч，ч在圖中省略)而觸發(fā)．轉換還關聯(lián)一個衛(wèi)士guard(t)，缺省時默認為true，衛(wèi)士是布爾表達式，表示轉換發(fā)生的先決約束條件．轉換可以伴隨更新效果動作effect(t)，它在轉換發(fā)生時被執(zhí)行，缺省時不做任何更新．

定義3 一個UML狀態(tài)機是一個4元組〈H，ф，E，deferrable〉，這里H是狀態(tài)層次;ф是H上的轉換;E是有限事件集合;deferrable:∑ 2E，是從狀態(tài)集合到事件集合E的子集的映射，表示可被延遲發(fā)生的事件．

3 模型轉換

3．1 模型轉換模式

模型轉換在MDE(model driven engineering)中扮演著重要角色，傳統(tǒng)的模型轉換大多是基于模型層的轉換，因此轉換規(guī)則和轉換關系很難重用，而基于元模型的模型轉換可以有效地解決此問題［2］．MDE的模型轉換遵循圖1所示的統(tǒng)一模式［9］，M1、M2和M3分別表示模型層、元模型層和元元模型層．Tab是一個轉換程序，它自動創(chuàng)建從源模型Ma到目標模型Mb的轉換．Tab、Ma和Mb分別是遵從元模型MMt、MMa和MMb的定義，MMt對應于轉換語言的抽象語法．3個元模型MMt、MMa和MMb遵從元元模型MMM的定義．

本文使用ATL［9］進行模型轉換，它是ATLAS轉換語言，用于指定模型到模型的轉換，是ATLAS模型管理架構AMMA(ATLAS model management architecture)平臺的一部分，建立在的OCL(object constraint language)形式化之上．ATL扮演模型轉換模式中MMt的角色，它在元模型層定義轉換規(guī)則，將MMa的元素映射到MMb上，并據(jù)此實現(xiàn)低層模型的自動轉換．

3．2 UML 元模型

建模就是用模型元素來描述系統(tǒng)，通常需要捕捉系統(tǒng)的靜態(tài)結構和動態(tài)行為．在UML模型中，系統(tǒng)的靜態(tài)結構由類圖來表示，類圖描述類以及類之間的關系;系統(tǒng)的動態(tài)行為由狀態(tài)圖進行描述，狀態(tài)圖描述一類對象的所有可能的狀態(tài)以及事件發(fā)生時狀態(tài)的轉移條件．

根據(jù)UML模型的靜態(tài)結構和動態(tài)行為的特征，結合類圖元模型與狀態(tài)機元模型，形成一個如圖2所示的靜態(tài)與動態(tài)相結合的UML元模型．

3．3 時間自動機元模型

Uppaal中使用的模型是時間自動機，對Alur等提出的時間自動機［10］進行了擴展，使之擁有用于同步的數(shù)據(jù)變量，并增加了緊急位置、堅定位置和緊急通道等．

定義4 一個時間自動機是一個8元組，

圖1 模型轉換模式Fig．1 Model transformation pattern

這里L是一個有限位置集合;l0∈L是開始位置集合;C是有限時鐘集合;A是一個有限動作集合;

是邊的集合，邊一般伴隨有動作、衛(wèi)士條件和復位時鐘集合;

是位置的不變式;V是有窮變量集合;

是一個轉換函數(shù)．

雖然時間自動機擁有形式化定義，但進行模型轉換必須構造其元模型，并實現(xiàn)UML元模型和時間自動機元模型的同構化．圖3給出了Uppaal中時間自動機的元模型，它與UML元模型是同構的，都遵從于MMM元元模型．

多個時間自動機的積組成時間自動機網(wǎng)絡，它關聯(lián)1個或多個時間自動機，所有的時間自動機都由Uppaal中的模板(Template)表示．一個模板可能包含若干個位置(Location)、邊(Edge)、時鐘(Clock)和參數(shù)(Parameter)．位置又可能為開始位置(Initial Location)、緊迫位置(Urgent Location)和堅定位置(Committed Location)．時鐘、參數(shù)和數(shù)值等可構成各種表達式(Expression)，包括布爾表達式(BoolExp)、同步表達式(SynExp)和賦值表達式(AssignExp)．布爾表達式包括邊的衛(wèi)士條件(Guard)和位置的不變式(Invariant);同步表達式是觸發(fā)邊轉換的動作;賦值表達式是邊轉換后的更新(Update)．

3．4 轉換的映射

ATL模型轉換是基于圖1所示的模型轉換模式進行的，它在元模型層定義映射規(guī)則．根據(jù)UML元模型以及時間自動機元模型的結構，將UML驗證模型中的主要元素映射為時間自動機模型的元素，如表1所示．

表1 UML到價格時間自動機的映射Tab．1 Mapping from UML to TA

4 實例研究

下邊以ATM取款機的主要取款操作為例對前文方法進行實例研究．該實例主要涉及2個類ATM和Bank，類之間通過一對一的引用相互關聯(lián)．結合前文UML元模型，對ATM取款問題進行建模，得到圖4所示的ATM和Bank的類和狀態(tài)機圖，它們共同構成驗證模型基礎．

圖4ATM的UML模型Fig．4 UML model of ATM

接著進行模型轉換，ATL是Eclipse環(huán)境下的一個插件，通過ATL的模型轉換，將非形式化的UML模型轉換為形式化的時間自動機模型，轉換結果為xmi格式的文件．將生成的時間自動機模型的xmi文件轉換成xml文件，并將其作為Uppaal的輸入，得到時間自動機模型．轉換后可以適當在模型中增加約束以提高系統(tǒng)的精確性，比如約束ATM機退卡10個時間單位后轉入空閑狀態(tài)，ATM機在確認錢數(shù)后60個時間單位內(nèi)出錢等，調(diào)整后的時間自動機模型如圖5所示．

圖5 ATM的時間自動機模型Fig．5 Timed automata model of ATM

在Uppaal的模擬器中可以對圖5所示的時間自動機模型進行追蹤模擬，得到多種運行軌跡，據(jù)此初步判斷模型的安全性和正確性．接著在驗證器中，通過簡化的CTL對系統(tǒng)要滿足的性質協(xié)議(如:A［］not deadlock，確保系統(tǒng)無死鎖;A［］ATM．GivingMoney imply ATM．x≤60，ATM機在確認錢數(shù)后60個時間單位內(nèi)出錢等)進行驗證，性質的驗證結果如圖6所示．

與常用的將UML模型轉換為PROMELA模型，并使用工具SPIN進行模型驗證的方法相比較［11－12］，本文方法可以對系統(tǒng)性質進行多方面驗證，而不僅僅是驗證系統(tǒng)是否出現(xiàn)不期望出現(xiàn)的交互行為．另外，Uppaal中可視化的時間自動機模型可進行直觀的模擬和追蹤，并且模型中的時鐘可以彌補UML在時間控制方面的不足，更加適用于有時間約束的實時系統(tǒng)等復雜系統(tǒng)．

圖6 驗證結果Fig．6 Verification results

5 結束語

結合國內(nèi)外有關研究，構造UML狀態(tài)機的形式化語義，對UML和時間自動機的形式化語義進行元建模，利用模型轉換語言ATL在元模型層完成從UML到時間自動機模型的轉換．最后結合ATM取款機對該方法進行實例研究，對ATM機取款主要操作進行UML建模并完成模型轉換，將得到的時間自動機模型在Uppaal中進行追蹤模擬以及安全性和正確性驗證．

今后將就此繼續(xù)展開研究，后續(xù)工作重點主要是對UML交叉或連接偽態(tài)、進入或者退出活動狀態(tài)等先進建模概念的轉換研究，以及系統(tǒng)時間約束的進一步研究．

［1］ Clarke E M，Wing J M．Formal methods:state of the art and future directions［J］．ACM Computing Surveys，1996，28(4):626－643．

［2］ 吉鳴，黃志球，祝義，等．基于MDA的實時軟件資源建模與模型轉換的方法［J］．計算機科學，2011，38(8):137－141．

［3］ 林惠民，張文輝．模型檢測:理論、方法與應用［J］．電子學報，2002，30(12A):1907－1912．

［4］ Gerd B，Alexandre D，Kim G L．A tutorial on Uppaal［C］∥Proc of the 4th Int’l School on Formal Methods for the Design of Computer，Communication，and Software Systems．Heidelberg:Springer-Verlag，2004:200 －236．

［5］ 周清雷，姬莉霞，王艷梅．基于UPPAAL的實時系統(tǒng)模型驗證［J］．計算機應用，2004，24(9):129－131．

［6］ 姬莉霞，馬建紅，周清雷．混雜系統(tǒng)的擴展時間自動機模型及驗證研究［J］．計算機工程與應用，2012，48(8):73－78．

［7］ Toni J，Jori D，Tommi J，et al．Model checking dynamic and hierarchical UML state machines［C］//Proceedings of MoDeV2a．Heidelberg:Springer-Verlag，2006:94 －110．

［8］ 何紅悅，宋自林，周波．基于DL-Safe規(guī)則的UML狀態(tài)圖形式化和一致性驗證［J］．鄭州大學學報:理學版，2009，41(1):94－98．

［9］ Jouault F，Allilaire F B J．ATL:a model transformation tool［J］．Science of Computer Programming Special Issue on Second Issue of Experimental Software and Toolkits(EST)，2008，72(1/2):31－39．

［10］ Alur R，Dill D L．A theory of timed automata［J］．Theoretical Computer Science，1994，126(2):183 －235．

［11］ Alexander K，Merz S．Model checking and code generation for UML state machines and collaborations［C］//Proc 5th Workshop on Tools for System Design and Verification．Reisenburg，2002:59 －64．

［12］ Timm S，Alexander K，Merz S．Model checking UML state machines and collaborations［J］．Electronic Notes in Theoretical Computer Science，2001，55(3):357－369．