嵌入式建模中帶有時間擴展的ＵＭＬ狀態圖的形式化方法

摘要:面向對象建模語言UML(Unified Modeling Language)已廣泛用于嵌入式系統建模，但它在嵌入式實時系統建模時存在概念模型形式化復雜和狀態圖對時間約束方面的建模功能不強的問題，針對這些問題，提出一種對UML狀態圖進行時間擴展的方法，并提出利用“可執行UML”對帶有時間擴展的UML狀態圖形式化的方法#65377;

關鍵詞:嵌入式系統;UML狀態圖;形式化

中圖分類號:TP311

文獻標識碼:A

1引言

隨著嵌入式系統在各個領域的廣泛應用，嵌入式系統變得越來越復雜#65377;因此，研究一種支持嵌入式系統從分析#65380;設計#65380;驗證到編碼這一整個開發過程的模型系統及建模方法變得越來越重要#65377;

UML是一種可視化建模語言[11]，它通過用例圖#65380;類圖#65380;協作圖#65380;狀態圖等一系列圖形符號來描述特定的系統，支持不同層次的系統抽象，能夠清晰而準確地描述特定系統的結構#65380;功能和行為，在多個領域中有成功的應用[10]#65377;將UML用于嵌入式系統的分析與設計，能夠由簡到詳，描繪出嵌入式系統的需求#65380;結構#65380;功能及相應的行為，讓開發者對所開發的系統有準確而全面的了解#65377;然而，但它對嵌入式系統建模時存在兩個主要不足:

一是UML不是形式化描述語言，不能直接對其模型進行模擬驗證#65377; 目前國內外解決這個問題的方法主要有四種:

(1)使用可執行語言進行系統描述#65380;模擬#65380;驗證#65377;如采用Cx語言去描述系統，然后將Cx對系統的描述編譯成內部擴充語法圖去分析和模擬系統[1]#65377;

(2)使用一種建模語言描述狀態圖，再使用基于此語言的框架技術進行系統分析#65380;設計#65380;驗證和編程#65377;如文獻[2]#65380;[3]提出的使用UML進行系統描述，然后使用基于UML的集成可視化開發環境Rhapsody(一個實時框架)，進行系統分析#65380;設計#65380;實現和驗證#65377;

(3)使用兩種建模語言#65377;如文獻[1]#65380;[4]提出的使用UML進行系統分析和設計，采用SystemC模擬驗證#65377;

(4)使用UML建模語言進行系統分析#65380;設計，再用其對此建模語言的改進使之能形式化描述，從而進行模型驗證#65377;如文獻[5]提出的將UML進行擴展使之成為“可執行UML”#65377;

二是UML狀態圖對時間約束的建模能力不強#65377;

嵌入式系統很多情況下具有實時性，在嵌入式實時系統的開發中，實時系統的動態屬性是其嚴格建模的重點#65377;其動態屬性主要表現在:反應式#65380;實時性這兩點#65377;UML狀態圖方法適合于對嵌入式實時系統的反應特性進行建模，然而，UML狀態圖在對時間約束方面的建模能力并不強，而且不規范#65377;]

2嵌入式實時系統中UML狀態圖的時間擴展

為了解決上述第二個問題，國內外提出了多種方法，如Sascha Konrad等[12]提出了實時描述模式，使用MTL#65380;TCTL#65380;RTGIL三種時序邏輯描述的方法;文章[6]提出了一種利用UML擴展機制，對UML狀態圖進行時間擴展，實現對基于狀態圖的時間約束進行建模，并使用時間化自動機進行模型形式化;還有一些研究[7]也通過UML擴展機制使得UML可以對實時系統進行表達#65377;本文采用UML擴展機制對UML狀態圖進行時間擴展，采用UML的增強性子集-可執行UML對UML模型進行形式化轉換#65377;

UML包含了三種擴展結構:約束(Constraints)#65380;版型(Stereotypes)#65380;標簽值(Tag)#65377;這些結構都可以在不更改基本UML元模型的前提下，對UML進行各種擴展#65377;現有的許多研究都通過擴展機制使得UML可以對實時系統進行表達#65377;本文借鑒[6]的方法，通過版型來提供時鐘以及時鐘事件的擴展#65377;

(1)超時事件版型:在某個狀態只能保持限定的時間，超時之后，系統遷移到另一狀態;

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

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

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

經過以上擴展，UML就可以對實時系統進行表達#65377;UML狀態圖中狀態遷移由兩類事件觸發，一類事件是由于狀態圖所表示的對象的外部輸入事件，另一類是在對象的運行中，內部時鐘所激發的時鐘事件#65377;

3形式化帶時間擴展的狀態圖的可執行UML

為了能對上述帶時間擴展的UML狀態圖形式化，我們類似[5]中提出的方法，采用可執行UML方法#65377;所謂可執行UML，是UML的增強性子集，使用與UML相同的符號表示法，并集成了狀態圖所用的形式化語義定義，其目標是為了模型的形式化描述，從而能進行模型的仿真和驗證#65377;在可執行UML元模型中，所有概念實體被抽象為類，每個概念實體在其生命周期內的所有活動用狀態圖來表示#65377;概念實體在其生命周期內的每一階段被抽象為狀態#65377;當一個概念實體處在生命周期內的某個階段時，某些事件的發生使實體從當前的狀態遷移到另一個狀態，這種遷移被抽象為變遷#65377;變遷描述了實體在當前狀態下可能發生的活動及其發生條件#65377;此外，元模型還定義了建模元素之間的關系，通過這些關系的定義，在建模過程中可以方便地區分不同的實例并描述這些實例之間的關系#65377;圖1顯示了可執行UML的元模型#65377;圖1可執行的UML的元模型(meta-model)

對于實時系統，根據第2節的討論，我們對狀態圖進行了時間擴展，為了能形式化表達狀態圖的時間約束，系統中所有可能發生的狀態遷移#65380;時間約束及其發生條件用狀態-約束-事件矩陣來表示#65377;

變遷#65380;時間約束和狀態-約束-事件矩陣可以被認為是用來描述系統行為的抽象概念，狀態和變遷之間的關系代表了當信號事件觸發后系統向新狀態的過渡#65377;

下面，以超時事件#65380;周期事件為例給出如何得出狀態-約束-事件矩陣，圖2是一個簡單的帶時間擴展的UML狀態圖，其中T0是超時事件，Tp是周期事件#65377;圖2帶時間擴展的UML狀態圖

根據上面的分析，在嵌入式實時系統建模中，先要確定模型中應包含的類及各類相應的狀態圖，各類的狀態圖包含了該類擁有的狀態#65380;引起狀態變換的信號事件#65380;帶時間約束的時鐘和時鐘事件及執行狀態變換的變遷等信息，然后在此基礎上建立系統的狀態-約束-事件矩陣，對系統的行為做形式化描述#65377;

4相關工作

本節給出一些與本文不同的形式化方法#65377;在賴明志等[6]的研究中，使用UML擴展機制對UML狀態圖進行時間擴展，構造了時間自動化機，然后將UML圖形轉換成時間自動化機模型的形式化方法#65377;

在石柯等[5]的研究中，使用了可執行UML對UML圖形進行形式化，但在時間約束方面，沒有給出更深的研究#65377;

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

此外，在嵌入式實時系統建模中，對時間和時間約束的描述還可以使用UML序列圖，我們的相關研究和文獻對這方面進行了研究#65377;

5結論

本文針對在嵌入式實時系統建模中，UML狀態圖時間約束方面建模能力不強以及UML模型非形式化描述的特點，根據嵌入式實時系統動態模型嚴格建模的要求，提出了一種將UML狀態圖進行時間擴展#65380;以及將此圖形轉換成可執行UML模型的方法#65377;而可執行UML能形式化描述UML模型#65377;在本文的研究中，給出了完整的且簡單的UML模型的形式化過程，并且增加時間擴展，實現了實時特性的建模與形式化描述#65377;

注：本文中所涉及到的圖表、注解、公式等內容請以PDF格式閱讀原文。