[發明專利]一種驗證UML模型中動態行為與時序契約的一致性的方法

無效

• 申請號: 200910047165.3
• 申請日: 2009-03-06
• 公開（公告）號: CN101673198A
• 公開（公告）日: 2010-03-17
• 發明（設計）人: 劉靜;杜德慧;謝越;尹玲;宮學強;曹虹華
• 申請（專利權）人: 華東師范大學
• 主分類號: G06F9/44
• 分類號: G06F9/44
• 代理公司: 上海伯瑞杰知識產權代理有限公司
• 代理人: 傅戈雁

技術領域

本發明屬于軟件開發技術領域，尤其涉及一種驗證統一建模語言UML模型中動態行為與時序契約的一致性的方法。

背景技術

面向服務架構(SOA)是一種架構模型，它可以根據需求通過網絡對松散耦合的粗顆粒應用組件進行分布式部署，組合和使用。服務層是SOA的基礎，而SOA服務必須由契約，接口和實現組成。而契約是服務共享和重用得以實現的基礎，契約式設計和SOA的結合為軟件開發和重用帶來了諸多益處。

統一建模語言(UML)是現今分析和設計軟件系統最為常用和有效的方法之一，通過動態模擬模型的行為，不但可以準確的描繪系統需求，還可以通過驗證方法在建模的初期發現模型中存在的問題，這也是模型驅動式(Model?Driving)軟件開發的目標所在。如何能夠讓UML模型滿足某些特性而又不出現錯誤則是設計時應該考慮的一個重要問題，而模型檢測是一種能夠非常有效提高系統可靠性的自動化技術。

模型檢測主要分三部分的工作，其中包括：對系統進行形式化建模，精確表達系統約束以及驗證模型是否滿足給定約束。

狀態圖(Statechart?Diagram)是描述一個實體基于事件反應的動態行為，顯示了該實體如何根據當前所處的狀態對不同的時間做出反應，狀態圖的創建通常是為了研究類，角色，子系統或者組件之間的復雜關系。狀態圖用于顯示狀態機(狀態機指定對象所在的狀態序列)，使對象達到這些狀態的事件和條件，已經達到這些狀態時所發生的操作。

順序圖(Sequence?Diagram)同樣是種動態建模方法，它表示對象間消息傳遞的順序關系，它可以表達成對象動態行為的時間契約，很好的約束模型中對象間的動態行為。

研究狀態圖和順序圖之間的一致性關系可以很好的分析模型中對象的動態行為是否滿足其定義的時間契約，從而有效分析UML動態模型間的關系，對于保證軟件開發初期需求模型的正確性和可重用性有著很大的作用。

系統屬性的描述方法有很多種，其中時序邏輯被證明能夠很有效地描述系統屬性，其中最為常用的是線性時序邏輯(LTL)。它能有效地描述模型中的時序和邏輯關系。模型檢測工具SPIN能夠有效地對并發系統進行建模并檢測，但由于其建模語言PROMELA是一種類C的代碼語言，因此通過PROMELA來精確描述系統并不是一件很容易的事情，而這是UML在模型描述上的優勢所在，同時將UML圖形轉換為PROMELA代碼也成為模型檢測的有效手段之一。

然而，目前沒有一種通用的辦法將模型的動態行為和時間契約用模型驗證工具有效聯系起來，給基于UML模型中的動態行為與時序契約一致性檢測帶來了很大困難。

發明內容

本發明的目的是提供一種驗證統一建模語言UML模型中動態行為與時序契約的一致性的方法，解決軟件開發需求設計階段所出現的模型不一致性的問題，為面向服務架構SOA和契約式設計的組合運用提供模型級的標準化技術解決方案。

本發明的技術方案是，一種驗證UML模型中動態行為與時序契約的一致性的方法，其特征在于，包括以下步驟：

A1，根據UML標準建模，包括生成UML狀態圖和UML順序圖，保存圖形的元模型；

A2，對所建模型的動態行為，實現UML狀態圖到PROMELA代碼的映射；

A3，構建所建模型時序契約，實現UML順序圖到LTL時態邏輯公式的映射；

A4，利用模型驗證工具SPIN對所述PROMELA代碼和所述LTL時態邏輯公式進行驗證；

A5，分析返回的所述的SPIN驗證結果。

所述步驟A1中生成的UML狀態圖具有的屬性包括觸發時間、遷移動作和狀態圖守衛條件，UML順序圖具有的屬性包括順序圖守衛條件和到達狀態。

所述步驟A2包括以下步驟：

B1，遍歷所述UML狀態圖得到所述保存的狀態圖元模型；

B2，抽取所述的狀態圖元模型中的動態行為，轉化為層次狀態機；

B3，根據所述的層次狀態機使用PROMELA語言建模，得到PROMELA代碼。

所述步驟A3包括以下步驟：

C1，遍歷所述UML順序圖得到所述保存的順序圖元模型。

C2，構建所建模型的時序契約，生成所述的LTL時態邏輯公式。

所述步驟A4包括以下步驟：

D1，將所述狀態圖轉換得到的PROMELA代碼保存在SPIN包下的pan?in文件中；????