基于UML的嵌入式系統(tǒng)模型驗證技術(shù)的研究

趙素萍

（蘭州交通大學(xué)電子與信息工程學(xué)院 730070）

0 引言

隨著對嵌入式系統(tǒng)復(fù)雜性和應(yīng)用需求的無限增加，其系統(tǒng)軟件開發(fā)的工作量劇增。統(tǒng)一建模語言UML已在嵌入式系統(tǒng)建模中得到廣泛應(yīng)用[2]。UML能夠直觀易懂的描繪出系統(tǒng)的需求、功能、結(jié)構(gòu)及相應(yīng)的行為，另外，使用UML有助于企業(yè)相互交流，克服溝通障礙。

然而在該領(lǐng)域還存在一定問題，首先UML對時間約束描述能力不強(qiáng)；其次UML為非形式化語言，其所建模型形式化轉(zhuǎn)換復(fù)雜。目前已有解決辦法：如文獻(xiàn)[1、3]使用UML的擴(kuò)展機(jī)制；文獻(xiàn)[8]使用的對象分析模式。然而擴(kuò)展機(jī)制是建模人員自己定義的，容易增加UML整體的復(fù)雜性；形式化轉(zhuǎn)換復(fù)雜，需要特殊工具支撐。

為了更好的解決上述問題，論文采用實時UML[4,5]對嵌入式系統(tǒng)建模；采用文獻(xiàn)[1]中提到的狀態(tài)-約束-事件矩陣方法對模型進(jìn)行形式化描述；最后利用SPIN[6,7]對模型進(jìn)行分析和驗證。

1 實時UML描述嵌入式系統(tǒng)

1.1 實時UML概述

實時UML主要由Rational公司開發(fā)。它合并了UML、角色建模、ROOM中的概念，開發(fā)出一個新的、比較完善的可用于復(fù)雜實時系統(tǒng)建模的標(biāo)準(zhǔn)。實時UML中主要引入三個概念。

端口：隨著膠囊事例的創(chuàng)建、消亡而同步運(yùn)作。

連接器：基于特定協(xié)議的信號傳遞通路。

膠囊：表示復(fù)雜實時系統(tǒng)中的主要結(jié)構(gòu)元素。

1.2 UML實時狀態(tài)圖的形式語義

1.3 超時事件

為實時狀態(tài)圖D中的超時事件加入時間約束：對于集合T中的任意元素t，若G (t)為真，與t相對應(yīng)的截止期為d(t)=2。對于所有進(jìn)入狀態(tài)t b(t)的轉(zhuǎn)移，加入時鐘約束((x:=0)?；對于所有的從該狀態(tài)出發(fā)的轉(zhuǎn)移，加入時鐘約束((x＜2)? 。

2 模型驗證工具SPIN

2.1 SPIN概述

SPIN主要包括模型仿真器和模型分析器兩個主要功能：模型仿真器可以快速對所建立的系統(tǒng)模型進(jìn)行仿真；模型分析器可以嚴(yán)格地驗證用戶提出的正確性要求是否被滿足。SPIN作為一種形式化自動驗證工具，目的是提供：

2.1.1 建模語言PROMELA:直觀地描述系統(tǒng)規(guī)約；

2.1.2 功能強(qiáng)大而簡明的邏輯表示法LTL；

2.1.3 可驗證系統(tǒng)建模邏輯一致性及系統(tǒng)是否滿足所要驗證性質(zhì)。

2.2 線性時序邏輯LTL

SPIN用線性時序邏輯LTL性質(zhì)描述系統(tǒng)的性質(zhì)。采用線性、離散、與自然數(shù)同構(gòu)的時間結(jié)構(gòu)。以狀態(tài)序列作為命題的論斷對象。用線性時序邏輯公式在狀態(tài)序列上解釋其真值。語法可遞歸定義如下：

定義1：命題常元{true ，false}和原子命題變元{p，q，…}是線性時序邏輯公式。

定義2：如果p和q是線性時序邏輯公式。則〈〉p(sometimes),p∪q(until),p∨q(or),

p∧q(and),?p(not), []p(always),Xp(next)也是線性時序邏輯公式。

2.3 基本數(shù)據(jù)結(jié)構(gòu)

在SPIN中基本數(shù)據(jù)結(jié)構(gòu)有：狀態(tài)矢量，棧深度優(yōu)先和已搜

狀態(tài)：

2.3.1 狀態(tài)矢量：包括全局和局部變量；

2.3.2 棧深度優(yōu)先：指出回溯方向和引起違反的狀態(tài)遷移序列；

2.3.3 已搜狀態(tài)：達(dá)到減少狀態(tài)壓縮、提高搜索效率的目的。

3 應(yīng)用舉例

3.1 使用實時UML建模

對嵌入式系統(tǒng)進(jìn)行模型驗證的步驟為：1.用實時UML為嵌入式系統(tǒng)建模；2.根據(jù)所建模型構(gòu)建狀態(tài)-約束-事件矩陣；3.根據(jù)矩陣的形式化描述，用Promela編寫系統(tǒng)程序；4.用XSPIN系統(tǒng)驗證程序的正確性和可行性；5.根據(jù)錯誤跡修改模型。下面以自動售貨機(jī)為例，討論如何建模和驗證。

自動售貨機(jī)系統(tǒng)由初始化模塊、投幣模塊、找零模塊、出貨模塊、超時退錢模塊組成執(zhí)行步驟為：1.系統(tǒng)初始化，等待顧客來購買；2.顧客選擇所要購買的商品；3.根據(jù)系統(tǒng)提示的價格進(jìn)行投幣；4.系統(tǒng)對顧客所投的錢與商品單價進(jìn)行比較；5.大于則找零、相等則系統(tǒng)出貨、不足提醒顧客繼續(xù)投；6.若顧客投幣不足，且不想繼續(xù)購買，則系統(tǒng)進(jìn)行超時退錢。對應(yīng)的UML狀態(tài)圖如圖1所示：

圖1：加入時間約束的自動售貨機(jī)狀態(tài)圖

3.2 模型形式化描述

為了能形式化表達(dá)自動售貨機(jī)狀態(tài)圖的時間約束，該系統(tǒng)中可能發(fā)生的遷移、時間約束和發(fā)生條件用狀態(tài)-約束-事件矩陣來表示。狀態(tài)-約束-事件矩陣被認(rèn)為是用來描述嵌入式系統(tǒng)行為的抽象概念。自動售貨機(jī)系統(tǒng)對應(yīng)的部分狀態(tài)約束事件矩陣如圖2所示：

圖2：系統(tǒng)狀態(tài)-約束-事件矩陣

3.3 形式化驗證

運(yùn)行程序時，首先進(jìn)行語法檢測和冗余檢測。冗余檢測時會給出一些改進(jìn)模型的建議。如果在運(yùn)行中發(fā)現(xiàn)一些給定參數(shù)的狀態(tài)沒有正確達(dá)到，這些語句將被反顯在主窗口中，并給出驗證輸出窗口，如圖3。根據(jù)提示可以確定錯誤類型。錯誤類型包括違反斷言、死鎖、無效循環(huán)等，圖3可以看出錯誤為違反斷言。

圖3：驗證尋找反例

4 結(jié)論

近年來，關(guān)于UML與模型檢測結(jié)合的研究一直十分活躍，但是這方面的技術(shù)還不夠成熟。首先，一些國內(nèi)外著名的研究高校都在進(jìn)一步研究和發(fā)展這種技術(shù)，這些研究機(jī)構(gòu)把提高UML語言的精確性，研究UML模型轉(zhuǎn)換和開發(fā)UML的支撐工具作為當(dāng)前的研究重點。其次，在眾多已經(jīng)流行的模型驗證工具中，SPIN是唯一獲得ACM軟件系統(tǒng)獎的工具，已經(jīng)成功應(yīng)用在控制系統(tǒng)驗證、安全協(xié)議驗證、最優(yōu)化規(guī)劃等領(lǐng)域。SPIN 內(nèi)嵌了很多用于狀態(tài)空間壓縮的優(yōu)化算法，但模型校驗器仍然需要很長的時間才能驗證一個指定的屬性，所以，狀態(tài)爆炸問題仍是一個令人頭疼的問題。

[1]段盛,李仁發(fā),謝佳芳.基于UML的嵌入式系統(tǒng)建模及模型驗證機(jī)制研究[J].計算機(jī)工程與科學(xué),2007,29（8）:138～139.

[2]段盛.UML擴(kuò)展機(jī)制在嵌入式實時建模中的應(yīng)用[J].科學(xué)技術(shù)與工程.2007, 7（6）:1012～1014.

[3]石柯,陽富民,胡貫榮.基于UML的嵌入式系統(tǒng)模型驗證機(jī)制的研究[J].計算機(jī)工程與應(yīng)用, 2001, 25（13）:111～113.

[4]BP DOUGLASS,尹浩瓊,歐陽宇.實時UML——開發(fā)嵌入式系統(tǒng)高效對象[M].中國電力出版社,105～150.

[5]鄒玉麗.基于UML的實時性研究[D].山東科技大學(xué),2005.13～24

[6]劉俏威.SPIN模型檢測的形式化分析機(jī)理研究及應(yīng)用[D].南昌大學(xué),2008.12～37

[7]G.J.HOLZMANN: The Model Checker SPIN.IEEE Transactions on Software Engineering,1997.23(5):279～295.

[8]Kourad S, Cheug B H C, Campbell L A.Object Analysis Patterns for Embedded Systems[J].IEEE Trans on Software Engineering, 2004,30(12):970～992.