技術(shù)分享 嵌入式建模中UML狀態(tài)圖的形式化方法
在學(xué)習(xí)UML的過程中你可能會(huì)遇到UML狀態(tài)圖問題，本節(jié)和大家一起學(xué)習(xí)一下嵌入式建模中帶有時(shí)間擴(kuò)展的UML狀態(tài)圖的形式化方法，希望通過本節(jié)的介紹大家對(duì)UML狀態(tài)圖有所了解。
嵌入式建模中帶有時(shí)間擴(kuò)展的UML狀態(tài)圖的形式化方法
摘要:面向?qū)ο蠼ＵZ言UML(UnifiedModelingLanguage)已廣泛用于嵌入式系統(tǒng)建模,但它在嵌入式實(shí)時(shí)系統(tǒng)建模時(shí)存在概念模型形式化復(fù)雜和狀態(tài)圖對(duì)時(shí)間約束方面的建模功能不強(qiáng)的問題,針對(duì)這些問題,提出一種對(duì)UML狀態(tài)圖進(jìn)行時(shí)間擴(kuò)展的方法,并提出利用“可執(zhí)行UML”對(duì)帶有時(shí)間擴(kuò)展的UML狀態(tài)圖形式化的方法。
1引言
隨著嵌入式系統(tǒng)在各個(gè)領(lǐng)域的廣泛應(yīng)用,嵌入式系統(tǒng)變得越來越復(fù)雜｡因此,研究一種支持嵌入式系統(tǒng)從分析､設(shè)計(jì)､驗(yàn)證到編碼這一整個(gè)開發(fā)過程的模型系統(tǒng)及建模方法變得越來越重要。
UML是一種可視化建模語言[11],它通過用例圖､類圖､協(xié)作圖､狀態(tài)圖等一系列圖形符號(hào)來描述特定的系統(tǒng),支持不同層次的系統(tǒng)抽象,能夠清晰而準(zhǔn)確地描述特定系統(tǒng)的結(jié)構(gòu)､功能和行為,在多個(gè)領(lǐng)域中有成功的應(yīng)用[10]｡將UML用于嵌入式系統(tǒng)的分析與設(shè)計(jì),能夠由簡(jiǎn)到詳,描繪出嵌入式系統(tǒng)的需求､結(jié)構(gòu)､功能及相應(yīng)的行為,讓開發(fā)者對(duì)所開發(fā)的系統(tǒng)有準(zhǔn)確而全面的了解｡然而,但它對(duì)嵌入式系統(tǒng)建模時(shí)存在兩個(gè)主要不足：
一是UML不是形式化描述語言,不能直接對(duì)其模型進(jìn)行模擬驗(yàn)證。目前國(guó)內(nèi)外解決這個(gè)問題的方法主要有四種:
(1)使用可執(zhí)行語言進(jìn)行系統(tǒng)描述､模擬､驗(yàn)證｡如采用Cx語言去描述系統(tǒng),然后將Cx對(duì)系統(tǒng)的描述編譯成內(nèi)部擴(kuò)充語法圖去分析和模擬系統(tǒng)[1]。
(2)使用一種建模語言描述狀態(tài)圖,再使用基于此語言的框架技術(shù)進(jìn)行系統(tǒng)分析､設(shè)計(jì)､驗(yàn)證和編程｡如文獻(xiàn)[2]､[3]提出的使用UML進(jìn)行系統(tǒng)描述,然后使用基于UML的集成可視化開發(fā)環(huán)境Rhapsody(一個(gè)實(shí)時(shí)框架),進(jìn)行系統(tǒng)分析､設(shè)計(jì)､實(shí)現(xiàn)和驗(yàn)證。
(3)使用兩種建模語言｡如文獻(xiàn)[1]､[4]提出的使用UML進(jìn)行系統(tǒng)分析和設(shè)計(jì),采用SystemC模擬驗(yàn)證。
(4)使用UML建模語言進(jìn)行系統(tǒng)分析､設(shè)計(jì),再用其對(duì)此建模語言的改進(jìn)使之能形式化描述,從而進(jìn)行模型驗(yàn)證｡如文獻(xiàn)[5]提出的將UML進(jìn)行擴(kuò)展使之成為“可執(zhí)行UML”。
二是UML狀態(tài)圖對(duì)時(shí)間約束的建模能力不強(qiáng)。
嵌入式系統(tǒng)很多情況下具有實(shí)時(shí)性,在嵌入式實(shí)時(shí)系統(tǒng)的開發(fā)中,實(shí)時(shí)系統(tǒng)的動(dòng)態(tài)屬性是其嚴(yán)格建模的重點(diǎn)｡其動(dòng)態(tài)屬性主要表現(xiàn)在:反應(yīng)式､實(shí)時(shí)性這兩點(diǎn)｡UML狀態(tài)圖方法適合于對(duì)嵌入式實(shí)時(shí)系統(tǒng)的反應(yīng)特性進(jìn)行建模,然而,UML狀態(tài)圖在對(duì)時(shí)間約束方面的建模能力并不強(qiáng),而且不規(guī)范｡]
2嵌入式實(shí)時(shí)系統(tǒng)中UML狀態(tài)圖的時(shí)間擴(kuò)展
為了解決上述第二個(gè)問題,國(guó)內(nèi)外提出了多種方法,如SaschaKonrad等[12]提出了實(shí)時(shí)描述模式,使用MTL､TCTL､RTGIL三種時(shí)序邏輯描述的方法;文章[6]提出了一種利用UML擴(kuò)展機(jī)制,對(duì)UML狀態(tài)圖進(jìn)行時(shí)間擴(kuò)展,實(shí)現(xiàn)對(duì)基于狀態(tài)圖的時(shí)間約束進(jìn)行建模,并使用時(shí)間化自動(dòng)機(jī)進(jìn)行模型形式化;還有一些研究[7]也通過UML擴(kuò)展機(jī)制使得UML可以對(duì)實(shí)時(shí)系統(tǒng)進(jìn)行表達(dá)｡本文采用UML擴(kuò)展機(jī)制對(duì)UML狀態(tài)圖進(jìn)行時(shí)間擴(kuò)展,采用UML的增強(qiáng)性子集-可執(zhí)行UML對(duì)UML模型進(jìn)行形式化轉(zhuǎn)換。
UML包含了三種擴(kuò)展結(jié)構(gòu):約束(Constraints)､版型(Stereotypes)､標(biāo)簽值(Tag)｡這些結(jié)構(gòu)都可以在不更改基本UML元模型的前提下,對(duì)UML進(jìn)行各種擴(kuò)展｡現(xiàn)有的許多研究都通過擴(kuò)展機(jī)制使得UML可以對(duì)實(shí)時(shí)系統(tǒng)進(jìn)行表達(dá)｡本文借鑒[6]的方法,通過版型來提供時(shí)鐘以及時(shí)鐘事件的擴(kuò)展。
(1)超時(shí)事件版型:在某個(gè)狀態(tài)只能保持限定的時(shí)間,超時(shí)之后,系統(tǒng)遷移到另一狀態(tài);
(2)操作的時(shí)間延遲版型:遷移中附帶的操作所花費(fèi)的時(shí)間不為0;
(3)受時(shí)鐘約束的遷移:時(shí)鐘約束是遷移約束條件,也就是說遷移只能發(fā)生在某個(gè)時(shí)間段,該遷移約束條件中使用了時(shí)鐘版型;
(4)周期事件版型:某些操作周期性執(zhí)行,或者事件､遷移在狀態(tài)圖中周期性發(fā)生。
經(jīng)過以上擴(kuò)展,UML就可以對(duì)實(shí)時(shí)系統(tǒng)進(jìn)行表達(dá)｡UML狀態(tài)圖中狀態(tài)遷移由兩類事件觸發(fā),一類事件是由于狀態(tài)圖所表示的對(duì)象的外部輸入事件,另一類是在對(duì)象的運(yùn)行中,內(nèi)部時(shí)鐘所激發(fā)的時(shí)鐘事件。
3形式化帶時(shí)間擴(kuò)展的狀態(tài)圖的可執(zhí)行UML
為了能對(duì)上述帶時(shí)間擴(kuò)展的UML狀態(tài)圖形式化,我們類似[5]中提出的方法,采用可執(zhí)行UML方法｡所謂可執(zhí)行UML,是UML的增強(qiáng)性子集,使用與UML相同的符號(hào)表示法,并集成了狀態(tài)圖所用的形式化語義定義,其目標(biāo)是為了模型的形式化描述,從而能進(jìn)行模型的仿真和驗(yàn)證｡在可執(zhí)行UML元模型中,所有概念實(shí)體被抽象為類,每個(gè)概念實(shí)體在其生命周期內(nèi)的所有活動(dòng)用狀態(tài)圖來表示｡概念實(shí)體在其生命周期內(nèi)的每一階段被抽象為狀態(tài)｡當(dāng)一個(gè)概念實(shí)體處在生命周期內(nèi)的某個(gè)階段時(shí),某些事件的發(fā)生使實(shí)體從當(dāng)前的狀態(tài)遷移到另一個(gè)狀態(tài),這種遷移被抽象為變遷｡變遷描述了實(shí)體在當(dāng)前狀態(tài)下可能發(fā)生的活動(dòng)及其發(fā)生條件｡此外,元模型還定義了建模元素之間的關(guān)系,通過這些關(guān)系的定義,在建模過程中可以方便地區(qū)分不同的實(shí)例并描述這些實(shí)例之間的關(guān)系｡圖1顯示了可執(zhí)行UML的元模型｡圖1可執(zhí)行的UML的元模型(meta-model)
對(duì)于實(shí)時(shí)系統(tǒng),根據(jù)第2節(jié)的討論,我們對(duì)狀態(tài)圖進(jìn)行了時(shí)間擴(kuò)展,為了能形式化表達(dá)狀態(tài)圖的時(shí)間約束,系統(tǒng)中所有可能發(fā)生的狀態(tài)遷移､時(shí)間約束及其發(fā)生條件用狀態(tài)-約束-事件矩陣來表示。
變遷､時(shí)間約束和狀態(tài)-約束-事件矩陣可以被認(rèn)為是用來描述系統(tǒng)行為的抽象概念,狀態(tài)和變遷之間的關(guān)系代表了當(dāng)信號(hào)事件觸發(fā)后系統(tǒng)向新狀態(tài)的過渡。
下面,以超時(shí)事件､周期事件為例給出如何得出狀態(tài)-約束-事件矩陣,圖2是一個(gè)簡(jiǎn)單的帶時(shí)間擴(kuò)展的UML狀態(tài)圖,其中T0是超時(shí)事件,Tp是周期事件｡圖2帶時(shí)間擴(kuò)展的UML狀態(tài)圖
根據(jù)上面的分析,在嵌入式實(shí)時(shí)系統(tǒng)建模中,先要確定模型中應(yīng)包含的類及各類相應(yīng)的狀態(tài)圖,各類的狀態(tài)圖包含了該類擁有的狀態(tài)､引起狀態(tài)變換的信號(hào)事件､帶時(shí)間約束的時(shí)鐘和時(shí)鐘事件及執(zhí)行狀態(tài)變換的變遷等信息,然后在此基礎(chǔ)上建立系統(tǒng)的狀態(tài)-約束-事件矩陣,對(duì)系統(tǒng)的行為做形式化描述?！ ?/p>
4相關(guān)工作
本節(jié)給出一些與本文不同的形式化方法｡在賴明志等[6]的研究中,使用UML擴(kuò)展機(jī)制對(duì)UML狀態(tài)圖進(jìn)行時(shí)間擴(kuò)展,構(gòu)造了時(shí)間自動(dòng)化機(jī),然后將UML圖形轉(zhuǎn)換成時(shí)間自動(dòng)化機(jī)模型的形式化方法。
在石柯等[5]的研究中,使用了可執(zhí)行UML對(duì)UML圖形進(jìn)行形式化,但在時(shí)間約束方面,沒有給出更深的研究。
在SaschaKonrad等[12]的研究中,采用MTL､TCTL､RTGIL三種時(shí)序邏輯和構(gòu)造English文法及描述模式的方法。
此外,在嵌入式實(shí)時(shí)系統(tǒng)建模中,對(duì)時(shí)間和時(shí)間約束的描述還可以使用UML序列圖,我們的相關(guān)研究和文獻(xiàn)對(duì)這方面進(jìn)行了研究。
5結(jié)論
本文針對(duì)在嵌入式實(shí)時(shí)系統(tǒng)建模中,UML狀態(tài)圖時(shí)間約束方面建模能力不強(qiáng)以及UML模型非形式化描述的特點(diǎn),根據(jù)嵌入式實(shí)時(shí)系統(tǒng)動(dòng)態(tài)模型嚴(yán)格建模的要求,提出了一種將UML狀態(tài)圖進(jìn)行時(shí)間擴(kuò)展､以及將此圖形轉(zhuǎn)換成可執(zhí)行UML模型的方法｡而可執(zhí)行UML能形式化描述UML模型｡在本文的研究中,給出了完整的且簡(jiǎn)單的UML模型的形式化過程,并且增加時(shí)間擴(kuò)展,實(shí)現(xiàn)了實(shí)時(shí)特性的建模與形式化描述。
【編輯推薦】
- 教你繪制整潔的UML圖
- SVG與UML圖詳解
- UML用例圖用法實(shí)例剖析
- 術(shù)語匯編 UML統(tǒng)一建模語言簡(jiǎn)介
- UML圖中用例圖和活動(dòng)圖簡(jiǎn)介
