摘要:面向?qū)ο蠼ＵZ(yǔ)言UML(Unified Modeling Language)已廣泛用于嵌入式系統(tǒng)建模，但它在嵌入式實(shí)時(shí)系統(tǒng)建模時(shí)存在概念模型形式化復(fù)雜和狀態(tài)圖對(duì)時(shí)間約束方面的建模功能不強(qiáng)的問(wèn)題，針對(duì)這些問(wèn)題，提出一種對(duì)UML狀態(tài)圖進(jìn)行時(shí)間擴(kuò)展的方法，并提出利用“可執(zhí)行UML”對(duì)帶有時(shí)間擴(kuò)展的UML狀態(tài)圖形式化的方法#65377;

關(guān)鍵詞:嵌入式系統(tǒng);UML狀態(tài)圖;形式化

中圖分類號(hào):TP311

文獻(xiàn)標(biāo)識(shí)碼:A

1引言

隨著嵌入式系統(tǒng)在各個(gè)領(lǐng)域的廣泛應(yīng)用，嵌入式系統(tǒng)變得越來(lái)越復(fù)雜#65377;因此，研究一種支持嵌入式系統(tǒng)從分析#65380;設(shè)計(jì)#65380;驗(yàn)證到編碼這一整個(gè)開(kāi)發(fā)過(guò)程的模型系統(tǒng)及建模方法變得越來(lái)越重要#65377;

UML是一種可視化建模語(yǔ)言[11]，它通過(guò)用例圖#65380;類圖#65380;協(xié)作圖#65380;狀態(tài)圖等一系列圖形符號(hào)來(lái)描述特定的系統(tǒng)，支持不同層次的系統(tǒng)抽象，能夠清晰而準(zhǔn)確地描述特定系統(tǒng)的結(jié)構(gòu)#65380;功能和行為，在多個(gè)領(lǐng)域中有成功的應(yīng)用[10]#65377;將UML用于嵌入式系統(tǒng)的分析與設(shè)計(jì)，能夠由簡(jiǎn)到詳，描繪出嵌入式系統(tǒng)的需求#65380;結(jié)構(gòu)#65380;功能及相應(yīng)的行為，讓開(kāi)發(fā)者對(duì)所開(kāi)發(fā)的系統(tǒng)有準(zhǔn)確而全面的了解#65377;然而，但它對(duì)嵌入式系統(tǒng)建模時(shí)存在兩個(gè)主要不足:

一是UML不是形式化描述語(yǔ)言，不能直接對(duì)其模型進(jìn)行模擬驗(yàn)證#65377; 目前國(guó)內(nèi)外解決這個(gè)問(wèn)題的方法主要有四種:

(1)使用可執(zhí)行語(yǔ)言進(jìn)行系統(tǒng)描述#65380;模擬#65380;驗(yàn)證#65377;如采用Cx語(yǔ)言去描述系統(tǒng)，然后將Cx對(duì)系統(tǒng)的描述編譯成內(nèi)部擴(kuò)充語(yǔ)法圖去分析和模擬系統(tǒng)[1]#65377;

(2)使用一種建模語(yǔ)言描述狀態(tài)圖，再使用基于此語(yǔ)言的框架技術(shù)進(jìn)行系統(tǒng)分析#65380;設(shè)計(jì)#65380;驗(yàn)證和編程#65377;如文獻(xiàn)[2]#65380;[3]提出的使用UML進(jìn)行系統(tǒng)描述，然后使用基于UML的集成可視化開(kāi)發(fā)環(huán)境Rhapsody(一個(gè)實(shí)時(shí)框架)，進(jìn)行系統(tǒng)分析#65380;設(shè)計(jì)#65380;實(shí)現(xiàn)和驗(yàn)證#65377;

(3)使用兩種建模語(yǔ)言#65377;如文獻(xiàn)[1]#65380;[4]提出的使用UML進(jìn)行系統(tǒng)分析和設(shè)計(jì)，采用SystemC模擬驗(yàn)證#65377;

(4)使用UML建模語(yǔ)言進(jìn)行系統(tǒng)分析#65380;設(shè)計(jì)，再用其對(duì)此建模語(yǔ)言的改進(jìn)使之能形式化描述，從而進(jìn)行模型驗(yàn)證#65377;如文獻(xiàn)[5]提出的將UML進(jìn)行擴(kuò)展使之成為“可執(zhí)行UML”#65377;

二是UML狀態(tài)圖對(duì)時(shí)間約束的建模能力不強(qiáng)#65377;

嵌入式系統(tǒng)很多情況下具有實(shí)時(shí)性，在嵌入式實(shí)時(shí)系統(tǒng)的開(kāi)發(fā)中，實(shí)時(shí)系統(tǒng)的動(dòng)態(tài)屬性是其嚴(yán)格建模的重點(diǎn)#65377;其動(dòng)態(tài)屬性主要表現(xiàn)在:反應(yīng)式#65380;實(shí)時(shí)性這兩點(diǎn)#65377;UML狀態(tài)圖方法適合于對(duì)嵌入式實(shí)時(shí)系統(tǒng)的反應(yīng)特性進(jìn)行建模，然而，UML狀態(tài)圖在對(duì)時(shí)間約束方面的建模能力并不強(qiáng)，而且不規(guī)范#65377;]

2嵌入式實(shí)時(shí)系統(tǒng)中UML狀態(tài)圖的時(shí)間擴(kuò)展

為了解決上述第二個(gè)問(wèn)題，國(guó)內(nèi)外提出了多種方法，如Sascha Konrad等[12]提出了實(shí)時(shí)描述模式，使用MTL#65380;TCTL#65380;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]也通過(guò)UML擴(kuò)展機(jī)制使得UML可以對(duì)實(shí)時(shí)系統(tǒng)進(jìn)行表達(dá)#65377;本文采用UML擴(kuò)展機(jī)制對(duì)UML狀態(tài)圖進(jìn)行時(shí)間擴(kuò)展，采用UML的增強(qiáng)性子集-可執(zhí)行UML對(duì)UML模型進(jìn)行形式化轉(zhuǎn)換#65377;

UML包含了三種擴(kuò)展結(jié)構(gòu):約束(Constraints)#65380;版型(Stereotypes)#65380;標(biāo)簽值(Tag)#65377;這些結(jié)構(gòu)都可以在不更改基本UML元模型的前提下，對(duì)UML進(jìn)行各種擴(kuò)展#65377;現(xiàn)有的許多研究都通過(guò)擴(kuò)展機(jī)制使得UML可以對(duì)實(shí)時(shí)系統(tǒng)進(jìn)行表達(dá)#65377;本文借鑒[6]的方法，通過(guò)版型來(lái)提供時(shí)鐘以及時(shí)鐘事件的擴(kuò)展#65377;

(1)超時(shí)事件版型:在某個(gè)狀態(tài)只能保持限定的時(shí)間，超時(shí)之后，系統(tǒng)遷移到另一狀態(tài);

(2)操作的時(shí)間延遲版型:遷移中附帶的操作所花費(fèi)的時(shí)間不為0;

(3)受時(shí)鐘約束的遷移:時(shí)鐘約束是遷移約束條件，也就是說(shuō)遷移只能發(fā)生在某個(gè)時(shí)間段，該遷移約束條件中使用了時(shí)鐘版型;

(4)周期事件版型:某些操作周期性執(zhí)行，或者事件#65380;遷移在狀態(tài)圖中周期性發(fā)生#65377;

經(jīng)過(guò)以上擴(kuò)展，UML就可以對(duì)實(shí)時(shí)系統(tǒng)進(jìn)行表達(dá)#65377;UML狀態(tài)圖中狀態(tài)遷移由兩類事件觸發(fā)，一類事件是由于狀態(tài)圖所表示的對(duì)象的外部輸入事件，另一類是在對(duì)象的運(yùn)行中，內(nèi)部時(shí)鐘所激發(fā)的時(shí)鐘事件#65377;

3形式化帶時(shí)間擴(kuò)展的狀態(tài)圖的可執(zhí)行UML

為了能對(duì)上述帶時(shí)間擴(kuò)展的UML狀態(tài)圖形式化，我們類似[5]中提出的方法，采用可執(zhí)行UML方法#65377;所謂可執(zhí)行UML，是UML的增強(qiáng)性子集，使用與UML相同的符號(hào)表示法，并集成了狀態(tài)圖所用的形式化語(yǔ)義定義，其目標(biāo)是為了模型的形式化描述，從而能進(jìn)行模型的仿真和驗(yàn)證#65377;在可執(zhí)行UML元模型中，所有概念實(shí)體被抽象為類，每個(gè)概念實(shí)體在其生命周期內(nèi)的所有活動(dòng)用狀態(tài)圖來(lái)表示#65377;概念實(shí)體在其生命周期內(nèi)的每一階段被抽象為狀態(tài)#65377;當(dāng)一個(gè)概念實(shí)體處在生命周期內(nèi)的某個(gè)階段時(shí)，某些事件的發(fā)生使實(shí)體從當(dāng)前的狀態(tài)遷移到另一個(gè)狀態(tài)，這種遷移被抽象為變遷#65377;變遷描述了實(shí)體在當(dāng)前狀態(tài)下可能發(fā)生的活動(dòng)及其發(fā)生條件#65377;此外，元模型還定義了建模元素之間的關(guān)系，通過(guò)這些關(guān)系的定義，在建模過(guò)程中可以方便地區(qū)分不同的實(shí)例并描述這些實(shí)例之間的關(guān)系#65377;圖1顯示了可執(zhí)行UML的元模型#65377;圖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)遷移#65380;時(shí)間約束及其發(fā)生條件用狀態(tài)-約束-事件矩陣來(lái)表示#65377;

變遷#65380;時(shí)間約束和狀態(tài)-約束-事件矩陣可以被認(rèn)為是用來(lái)描述系統(tǒng)行為的抽象概念，狀態(tài)和變遷之間的關(guān)系代表了當(dāng)信號(hào)事件觸發(fā)后系統(tǒng)向新?tīng)顟B(tài)的過(guò)渡#65377;

下面，以超時(shí)事件#65380;周期事件為例給出如何得出狀態(tài)-約束-事件矩陣，圖2是一個(gè)簡(jiǎn)單的帶時(shí)間擴(kuò)展的UML狀態(tài)圖，其中T0是超時(shí)事件，Tp是周期事件#65377;圖2帶時(shí)間擴(kuò)展的UML狀態(tài)圖

根據(jù)上面的分析，在嵌入式實(shí)時(shí)系統(tǒng)建模中，先要確定模型中應(yīng)包含的類及各類相應(yīng)的狀態(tài)圖，各類的狀態(tài)圖包含了該類擁有的狀態(tài)#65380;引起狀態(tài)變換的信號(hào)事件#65380;帶時(shí)間約束的時(shí)鐘和時(shí)鐘事件及執(zhí)行狀態(tài)變換的變遷等信息，然后在此基礎(chǔ)上建立系統(tǒng)的狀態(tài)-約束-事件矩陣，對(duì)系統(tǒng)的行為做形式化描述#65377;

4相關(guān)工作

本節(jié)給出一些與本文不同的形式化方法#65377;在賴明志等[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ī)模型的形式化方法#65377;

在石柯等[5]的研究中，使用了可執(zhí)行UML對(duì)UML圖形進(jìn)行形式化，但在時(shí)間約束方面，沒(méi)有給出更深的研究#65377;

在Sascha Konrad等[12]的研究中，采用MTL#65380;TCTL#65380;RTGIL三種時(shí)序邏輯和構(gòu)造English文法及描述模式的方法#65377;

此外，在嵌入式實(shí)時(shí)系統(tǒng)建模中，對(duì)時(shí)間和時(shí)間約束的描述還可以使用UML序列圖，我們的相關(guān)研究和文獻(xiàn)對(duì)這方面進(jìn)行了研究#65377;

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ò)展#65380;以及將此圖形轉(zhuǎn)換成可執(zhí)行UML模型的方法#65377;而可執(zhí)行UML能形式化描述UML模型#65377;在本文的研究中，給出了完整的且簡(jiǎn)單的UML模型的形式化過(guò)程，并且增加時(shí)間擴(kuò)展，實(shí)現(xiàn)了實(shí)時(shí)特性的建模與形式化描述#65377;

注：本文中所涉及到的圖表、注解、公式等內(nèi)容請(qǐng)以PDF格式閱讀原文。