基于UML的嵌入式系統模型驗證技術的研究

趙素萍

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

0 引言

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

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

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

1 實時UML描述嵌入式系統

1.1 實時UML概述

實時UML主要由Rational公司開發。它合并了UML、角色建模、ROOM中的概念，開發出一個新的、比較完善的可用于復雜實時系統建模的標準。實時UML中主要引入三個概念。

端口：隨著膠囊事例的創建、消亡而同步運作。

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

膠囊：表示復雜實時系統中的主要結構元素。

1.2 UML實時狀態圖的形式語義

1.3 超時事件

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

2 模型驗證工具SPIN

2.1 SPIN概述

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

2.1.1 建模語言PROMELA:直觀地描述系統規約；

2.1.2 功能強大而簡明的邏輯表示法LTL；

2.1.3 可驗證系統建模邏輯一致性及系統是否滿足所要驗證性質。

2.2 線性時序邏輯LTL

SPIN用線性時序邏輯LTL性質描述系統的性質。采用線性、離散、與自然數同構的時間結構。以狀態序列作為命題的論斷對象。用線性時序邏輯公式在狀態序列上解釋其真值。語法可遞歸定義如下：

定義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 基本數據結構

在SPIN中基本數據結構有：狀態矢量，棧深度優先和已搜

狀態：

2.3.1 狀態矢量：包括全局和局部變量；

2.3.2 棧深度優先：指出回溯方向和引起違反的狀態遷移序列；

2.3.3 已搜狀態：達到減少狀態壓縮、提高搜索效率的目的。

3 應用舉例

3.1 使用實時UML建模

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

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

圖1：加入時間約束的自動售貨機狀態圖

3.2 模型形式化描述

為了能形式化表達自動售貨機狀態圖的時間約束，該系統中可能發生的遷移、時間約束和發生條件用狀態-約束-事件矩陣來表示。狀態-約束-事件矩陣被認為是用來描述嵌入式系統行為的抽象概念。自動售貨機系統對應的部分狀態約束事件矩陣如圖2所示：

圖2：系統狀態-約束-事件矩陣

3.3 形式化驗證

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

圖3：驗證尋找反例

4 結論

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

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

[2]段盛.UML擴展機制在嵌入式實時建模中的應用[J].科學技術與工程.2007, 7（6）:1012～1014.

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

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

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

[6]劉俏威.SPIN模型檢測的形式化分析機理研究及應用[D].南昌大學,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.