實時系統(tǒng)動態(tài)行為模型的一種形式分析方法

摘 要:提出了一種基于統(tǒng)一建模語言UML 2.0的實時系統(tǒng)動態(tài)行為模型的形式分析方法。首先給出了UML順序圖的形式化描述，分析了UML順序圖中事件之間的關系;在此基礎上，給出一種對象自動機來描述每個對象在UML順序圖描述的場景中所參與的事件序列的方法，并將該方法擴展到帶有組合片段的UML 2.0順序圖;最后通過分析UML 2.0順序圖中的時間建模機制，給出了從UML 2.0順序圖中提取時間約束得到時間自動機的算法。

關鍵詞:實時系統(tǒng); 動態(tài)行為模型; 時間約束; 統(tǒng)一建模語言UML 2.0; 對象自動機

中圖分類號:TP311文獻標志碼:A

文章編號:1001-3695(2009)09-3365-04

doi:10.3969/j.issn.1001-3695.2009.09.046

Formal analysis for dynamic behavioral models of real-time systems

RONG Mei

(Shenzhen Tourism College， Jinan University， Shenzhen Guangdong 518053， China)

Abstract:This paper introduced a formal analysis for dynamic behavioral models of real-time systems based on unified modeling languages(UML 2.0). Firstly， presented the formal specification of UML sequence diagrams，and studied the relationship between the events in the sequence diagram， after thatintroduced an automata to describe the events that every object participated in the scenario that the sequence diagram depicts. Then extended the automata to describe the UML 2.0 sequence diagram that contains combined fragment. Finally， analyzed the time modeling mechanism in UML 2.0 sequence diagram， after that introduced an algorithm to extract the timing constraints from UML 2.0 sequence diagram and translated the object automata which got in the last step into timed automata.

Key words:real-time systems; dynamic behavioral model; timing constraint; unified modeling language UML 2.0; object automata

0 引言

實時系統(tǒng)是一種在限定時間內(nèi)對來自外界的請求、輸入等作出響應的計算機系統(tǒng)[1]。實時系統(tǒng)的正確性不僅依賴于計算的邏輯結(jié)果，而且依賴于結(jié)果產(chǎn)生的時間。許多重要的系統(tǒng)都具有實時性，如控制系統(tǒng)、監(jiān)測系統(tǒng)、通信系統(tǒng)等，它們一般比較復雜且對安全性和可靠性要求較高，尤其在一些諸如核電站控制、航空航天、軍事指揮及鐵路調(diào)度等安全悠關(safety-critical)領域更是如此，這類系統(tǒng)要求絕對安全可靠，不容半點疏漏，否則將導致災難性后果。如何確保實時系統(tǒng)的可靠性已成為近年來計算機科學與控制論領域共同關注的一個焦點問題。

本文提出了一種在實時系統(tǒng)開發(fā)的早期階段，對基于UML的動態(tài)行為模型進行形式化分析的方法。首先給出UML順序圖的形式化描述，分析了順序圖中事件之間的關系，在此基礎上，給出一種對象自動機來描述順序圖中每個對象在場景中參與的事件序列的方法，并將該方法擴展到帶有組合片段的UML2.0順序圖[2]，最后，針對UML2.0順序圖中提供的時間建模機制，提出了從順序圖中提取時間約束得到時間自動機[3]的算法。

1 順序圖的形式化描述與分析

UML順序圖用來在系統(tǒng)設計的早期階段對系統(tǒng)的動態(tài)行為建模，它描述在一個特定情況下系統(tǒng)的運行場景。場景描述了系統(tǒng)中消息傳遞的時間次序，即消息是如何在各個對象之間被發(fā)送和接收的。

定義1 UML順序圖是一個五元組SD=(O，E，M，obj，)。其中:

O表示有窮對象的集合。

E=S∪R表示有窮事件集合，包括發(fā)送事件集S和接收事件集R，且S∩R=。

M表示有窮消息的集合，每個消息m∈M，與兩個有因果關系的事件相連:一個消息發(fā)送事件m!∈S，表示對象發(fā)送一個消息;一個消息接收事件m?∈R，表示對象接收一個消息。m!和m?構成了一對同步事件。

obj表示S∪R→O為一函數(shù)，將每個事件映射到其所屬的對象，該函數(shù)將順序圖中的事件根據(jù)其所屬的對象生命線進行分割。obj-1:O→S∪R，將順序圖所表示的描述場景事件序列映射到一個對象，得到該對象在場景中所參與的一個事件集合。

表示為順序圖中事件之間滿足的可視關系。

順序圖包含同步消息和異步消息，同步消息的發(fā)送者只有在收到接收者的返回消息后才能繼續(xù)執(zhí)行自己的操作，異步消息的發(fā)送者在發(fā)送完消息后不用等待返回消息即可繼續(xù)執(zhí)行自己的操作。

UML順序圖所描述的場景表現(xiàn)為表示系統(tǒng)執(zhí)行路徑的一些事件序列，順序圖的語義就表示為這樣一些事件序列。在控制關系中，可能存在不確定的接收消息的先后次序，而且UML 2.0中所添加Alt、Opt和Par等組合片段都會產(chǎn)生執(zhí)行路徑的分支，因此一個順序圖可能允許多個事件序列，從而使順序圖能表達多種邏輯語義。

定義2 一個UML順序圖SD=(O，E，M，obj，)可以表達多種邏輯語義『SD』=〈TR1，TR2，…，TRn〉，每種語義TRi可以由一個定義在(E，)上的事件序列來表示:TRi=〈e0e1…em〉。其中:ei∈E(0≤i≤m);ei+1在事件ei之后發(fā)生(1≤i≤m-1);TRi中的事件滿足可視關系。

2 順序圖的對象自動機模型

將順序圖所表達的邏輯語義映射到順序圖中的一個對象o就得到了該對象在執(zhí)行場景中所參與的事件序列，表示為『SDo』。該事件序列可以用一個有窮自動機進行識別，稱刻畫一個對象在場景中所參與的事件序列的有窮自動機為該對象的對象自動機。整個順序圖所描述的行為就可以表示為由所有對象的對象自動機構成的有窮自動機網(wǎng)絡，對象自動機之間通過同步事件進行通信。

2.1 不含組合片段的順序圖的對象自動機模型

每個對象自動機的觸發(fā)事件為順序圖生命線上對象所參與的事件，對象發(fā)送或接收一個消息都觸發(fā)對象自動機狀態(tài)之間的一次遷移。下面給出不帶組合片段的UML順序圖對象自動機的構造方法。

定義3 令SD=(O，E，M，obj，)為UML順序圖，o∈O，對象o所對應的對象自動機AMo可以表示為一個五元組AMo=(S，Eo，s0，T，o)。其中:

S為狀態(tài)集合，S={sk:O→E，k∈N}={sk:o→w∈E |n≤|w|，m≤n:(w(n)，w(m))}S中的每個狀態(tài)sk為系統(tǒng)運行過程中的第k步上，Eo上的字(一個事件序列)到對象o的映射，每一步中出現(xiàn)的事件與上一步中出現(xiàn)的事件滿足關系。

Eo=obj-1(o)為順序圖中對象o所參與的事件集合，每個事件可以表示為m!或m?的形式。

s0∈S表示初始節(jié)點，在該節(jié)點沒有記錄事件，即o∈O，s0(o)=ε。

T:S×Eo×Guard→S，為狀態(tài)遷移的集合，每個遷移tr可表示為(si，e[cond]，sj)，表示對象o所參與的場景序列中出現(xiàn)了事件e，并且在遷移使能條件cond滿足的條件下，由上一步的狀態(tài)si遷移到當前狀態(tài)sj。

oEo×Eo，為對象o的生命線上事件之間滿足的全序關系，用來描述在一個場景的執(zhí)行序列中，一個事件在另一個事件之前發(fā)生。

圖1給出了一個具有兩個對象的簡單順序圖。圖2給出了圖1中對象A的對象自動機SimpleSD_A和對象B的對象自動機SimpleSD_B。在SimpleSD_A中AS0=〈ε〉，對象A收到消息m1后，AS1=〈m1?〉，在對象A的生命線上滿足m1?Am2!。

根據(jù)定義3中狀態(tài)S的構造方法可得AS2=〈m1?，m2!〉，同理，AS3=〈m1?，m2!，m3?〉，AS4=〈m1?，m2!，m3?，m4!〉。這樣圖1中的順序圖所表示的系統(tǒng)行為就由SimpleSD_A和SimpleSD_B組成的有窮自動機網(wǎng)絡進行表示。

使用『AMo』表示對象o的對象自動機AMo所識別的語言，這樣對象o在場景中所參與的事件序列集合『SDo』=『AMo』。

2.2 包含組合片段的順序圖的對象自動機模型

在構造加入組合片段的UML 2.0順序圖的對象自動機前，先定義關于對象自動機的兩個二元操作符，即邏輯加和邏輯與。邏輯加表示兩個對象自動機之間的異或關系，根據(jù)給定的判定條件執(zhí)行其中一個對象自動機中的事件。邏輯與表示兩個對象自動機之間的并發(fā)關系，兩個對象自動機中的事件可以交替執(zhí)行。

設AM1=(S ，Eo ，s0 ，T ， o)，AM2=(S2，Eo2，s02，T2，2o)為兩個對象自動機，邏輯加和邏輯與的定義如下:

a)AM1AM2=(S，Eo，s0，T，o)。其中:

Eo=Eo ∪Eo2;

S=S ∪S2∪{s0}，這里s0為新的初始狀態(tài)，s0(o)=ε;

T=T ∪T2，為狀態(tài)之間的遷移，T的選擇由所給定的判定條件cond決定，cond的值為true時T=T ，否則T=T2;

o= o∪2o。

b)AM1AM2=(S，Eo，s0，T，o)。其中:

Eo=Eo ∪Eo2;

S=(S S2)∪(S2S )，其中每個狀態(tài)表示為

sk∈S:o→sk(o)=s i(o)#8226;s2j(o)，其中，s i∈S ，s2j∈S2，對于e∈s i(o)，e′∈s2j(o):(e′，e)os2i(o)#8226;s j(o)，其中，s2i∈S2，s j∈S ，對于e∈s2i(o)，e′∈s j(o):(e′，e)o

s0為新的初始狀態(tài)，s0(o)=ε;

T:S×Eo→S，為狀態(tài)之間的遷移集合，該遷移由并發(fā)區(qū)域中的子遷移得到:

T={(sk，e，sk′)|sk=s i(o)#8226;s2j(o)∧ sk′=s m(o)#8226;s2n(o)∧((s i(o)，e，s m(o))∈T ∨(s2j(o)，e，s2n(o))∈T2)}∪{(sk，e，sk′)|sk=s2i(o)#8226;s j(o)∧sk′=s2m(o)#8226;s n(o)∧((s i(o)，e，s m(o))∈T2∨ (s2j(o)，e，s2n(o))∈T )}

UML 2.0順序圖中添加了Coregion、Alt、Opt和Par組合片段，它們是UML 2.0順序圖產(chǎn)生語義分支的根源。基于上述兩個數(shù)學結(jié)構，下面給出帶有以上組合片段的UML 2.0順序圖對象自動機構造方法。

1)Coregion組合片段

Coregion標注了順序圖對象生命線上一個特殊的區(qū)域，如果對象的生命線處于該區(qū)域，則事件出現(xiàn)的次序是不確定的。

圖3為具有coregion組合片段的UML 2.0順序圖中的一個對象的生命線，圖中消息m3、m4出現(xiàn)在Coregion區(qū)域中，即m3、m4到達對象A的次序沒有定義。

圖4為該組合片段所對應的對象自動機。在該自動機中從狀態(tài)s2離開的遷移，將隨機地執(zhí)行到達s3或s4的遷移，從而對應于Coregion區(qū)域中m3、m4消息的不確定性。

2)Alt組合片段

一個Alt組合片段有m個互斥的可選分支，每個分支上都有執(zhí)行該分支的使能條件，只有使能條件為真的分支才被執(zhí)行。基于上面給出的邏輯加的定義，在UML 2.0順序圖SD中具有n個交互子集的Alt組合片段，映射到對象o上的執(zhí)行路徑集合可以形式化地表示為

『SDo』=『SDo1 Alt SDo2Alt …Alt SDon』=

『AM1』『AM2』…『AMn』

其中:SDoi(1≤i≤n)表示對象o中第i個交互子集，AMi表示第i個交互子集所對應的子對象自動機。對于每個分支的使能條件中的變量應設為全局變量，以便該順序圖中除該對象以外的其他對象的對象自動機都可以根據(jù)該使能條件執(zhí)行路徑的選擇。對于具有嵌套結(jié)構的復合組合片段轉(zhuǎn)換成對象自動機時，將父親分支的使能條件與子分支的使能條件的合取，作為對象自動機的分支使能條件。

圖5為一個具有Alt組合片段的兩個對象的簡單UML 2.0順序圖，在該組合片段中有兩個交互子集。圖6為該順序圖所對應的對象自動機，包括對象A的對象自動機Alt_A和對象B的對象自動機Alt_B。

3)Opt組合片段

Opt組合片段稱為可選組合片段，它是Alt組合片段的一種特殊情況，相當于Alt組合片段中[else]分支為空的情況，它只能表達真假兩種語義分支，使能條件為真時才執(zhí)行該組合片段，否則跳過該片斷執(zhí)行其后續(xù)路徑。在UML 2.0順序圖SD中組合片段Opt映射到對象o上的執(zhí)行路徑集合可以形式化表示為

『SDo』=『Opt(SD)』=『SD Alt SD』=『AM』『AM』

其中:SD表示空交互子集;AM表示SD對應的空對象自動機，AM=〈，，s0，，〉，s0:O→{ε}給對象o的對象自動機的初始狀態(tài)賦值一個空事件。

4)Par組合片段

Par組合片段為并發(fā)組合片段，該組合片段并發(fā)區(qū)域中的事件可以交替執(zhí)行。在UML 2.0順序圖SD中具有n個并發(fā)子集的Par組合片段，映射到對象o上的執(zhí)行路徑集合可以形式化地表示為

『SDo』=『SDo1 Par SDo2Par …Par SDon』=『AM1』『AM2』…『AMn』

圖7為具有Par組合片段的兩個對象的簡單UML 2.0順序圖。圖8為該順序圖所對應的對象自動機Par_A和Par_B。

3 時間約束提取算法

UML 2.0順序圖中提供了時間建模機制，便于對實時系統(tǒng)的時間約束進行建模。圖9給出了在順序圖中使用相關符號來描述時間觀測和時間約束的方法。其中對象user發(fā)送消息code給對象ACSystem，消息傳遞過程中所需要的時間使用d=duration進行記錄。ACSystem在收到code消息后發(fā)送OK和cardout兩個消息給user，傳遞cardout消息所需的時間為0~13個時間單元，user對象從發(fā)送消息code到接收到消息OK之間的時間間隔是d~3×d個時間單元。這里d為發(fā)送消息code所需的時間。使用t=now來記錄發(fā)送消息OK的時間，也即事件b2的發(fā)生時間。

將順序圖中每個對象上的消息事件序列轉(zhuǎn)換成對象自動機之后，可以從UML 2.0順序圖中抽取其中的時間約束，從而將對象自動機轉(zhuǎn)換為時間自動機，這樣整個系統(tǒng)的行為就可以用時間自動機網(wǎng)絡進行表示，其中的時間自動機通過構造每個對象的對象自動機而得到。從UML 2.0中提取出時間約束將對象自動機轉(zhuǎn)換為時間自動機的方法如下:

首先定義兩個映射δ1、δ2:

δ1:S→Ψ(T)

δ2:T→2T

第一個映射給每個位置賦值一個位置不變式，第二個映射對每個與遷移相關聯(lián)的時鐘變量進行初始化，可以為空。當滿足δ1(s)時，系統(tǒng)可以位于狀態(tài)s，觸發(fā)事件e出現(xiàn)時遷移就被觸發(fā)，一旦δ1(s)的值變?yōu)楠?，就執(zhí)行遷移離開狀態(tài)s。遷移發(fā)生時，所有時鐘變量hi∈δ1(s)被重置為零，這些時鐘變量測量自重置為零時刻開始的時間進展，在后續(xù)階段還可以繼續(xù)使用。

處理時間約束方法的主要思路是:在事件發(fā)生時，以及出現(xiàn)時間觀測點的時刻都產(chǎn)生一個邏輯時鐘lgtimer，任何從該點離開的遷移都要對時鐘變量h進行重置，以使其可以測量時鐘被重置以來的時間進展情況，時間約束提取算法如下:

算法:對象自動機中時間約束的提取

輸入:SeqD=(O，E，M，obj，，C)，即帶時間約束的UML 2.0順序圖;AM={AMO|o∈O∧AMO=(S，Eo，S0，T，F(xiàn))}，即SeqD中對象自動機的集合。

輸出:TAM，時間對象自動機。

Alogrithm Extr_time_Constr(Time_constraint_type{t+a.t+b})

{clock lgtimer，T=;

for s∈S do δ1(s)=true;

TO={t|t=Time_observation(ev)∧t∈SeqD.C∧ev∈SeqD.E};

//TO為順序圖SeqD中事件ev的時間觀測點集合;

for t∈TO do

{T=T∪{lgtimer};//lgtimer測量自事件ev出現(xiàn)以來的時間進展

TR1={tr|tr.e=ev∧ev∈SeqD.E}

//TR1為SeqD中觸發(fā)事件為ev的遷移集合

for tr∈TR1 do δ2(tr)=δ2(tr)∪{lgtimer=0};

EV={ev′|ev′∈SeqD.E∧ev∝ev′};

for ev′∈EV do

{TR2={tr|tr.e=ev′∧ev′∈EV};

//TR2為觸發(fā)事件ev′的遷移集合

N={s|s∈S∧tr∈TR2∧src(tr)=s};

//N為TR2中遷移的源狀態(tài)集合

for s∈N do δ1(s)=δ1(s)∧lgtimer≤b;

for tr∈TR2 do tr.guard=a≤lgtimer≤b;

}

}

}

對于{t+a..t+b}形式的時間約束，假設在第一個事件ev處設置了時間觀測點t，如果第二個事件ev′發(fā)生的時間約束為{t+a..t+b}，則用ev∝ev′表示事件ev和ev′之間的這種關系。{a..b}形式的時間約束表示兩個事件ev和ev′之間的時間間隔為a~b個時間單元，同樣使用ev∝ev′表示具有這種時間約束的兩個事件。{a..b}與{t+a..t+b}的算法處理時的區(qū)別在于，對于每個事件ev，前者只有一個ev′與之對應，而后者可能有多個ev′與之對應。對于每個事件ev，在對象自動機中搜索所有滿足ev∝ev′關系的事件ev′的集合，將所有觸發(fā)事件為ev′的遷移時間約束置為a≤lgtimer≤b。

對于兩個事件之間形如{a..b}形式的時間約束提取算法如下:

Alogrithm Extr_time_Constr(Time_constraint_type {a.b})

{clock lgtimer，T=;

for s∈S do δ1(s)=true;

TC={tc|tc={a.b}∧tc∈SeqD.C};

//TC為順序圖SeqD中(a.b)類型的時間約束集合

for tc∈TC DO

{T=T∪{lgtimer};

//lgtimer測量自事件ev出現(xiàn)以來的時間進展

TR1={tr|tr.e=ev∧ev∈SeqD.E};

//TR1為SeqD中觸發(fā)事件ev的遷移集合

for tr∈TR1 do

δ2(tr)=δ2(tr)∪{lgtimer=0};

TR2={tr|tr.e=ev′∧ev′∈EV∧ev∝ev′};

TR2為觸發(fā)事件為ev′的遷移集合

N={s|s∈S∧tr∈TR2∧src(tr)=s};

//N為TR2中遷移的原狀態(tài)集合

for s∈N do δ1(s)=δ1(s)∧lgtimer≤b;

for tr∈TR2 do tr.guard=a≤lgtimer≤b;

}

}

經(jīng)過以上幾步以后，就將帶有時間約束的UML 2.0順序圖所描述的場景中，每個對象所參與的消息發(fā)送和接收的事件序列，轉(zhuǎn)換成了等價的時間自動機的形式進行表示，整個系統(tǒng)中所有時間自動機的集合組成了一個時間自動機網(wǎng)絡。

4 結(jié)束語

本文給出了一種基于對象自動機、對使用UML順序圖建立的實時系統(tǒng)動態(tài)行為模型進行形式分析的方法，為下一步使用模型檢測[4]等形式化工具對模型進行自動驗證奠定了基礎。

參考文獻:

[1]MANNA Z， PNUELI A. Models for reactivity[J]. Acta Informatica，1993，30(7):609-678.

[2]OMG. Unified modeling language:superstructure， version 2.0[K]. 2005.

[3]ALUR R， DILL D L. A theory of timed automata[J]. Theoretical Computer Science，1994，126(2):183-235.

[4]戎玫，張廣泉.模型檢測新技術研究[J].計算機科學，2003，30(5):101-104.