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

無效

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

1、一種驗證UML模型中動態行為與時序契約的一致性的方法，其特征在于，包括以下步驟：

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

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

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

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

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

2、如權利要求1所述的驗證UML模型中動態行為與時序契約的一致性的方法，其特征在于，所述步驟A1中生成的UML狀態圖具有的屬性包括觸發時間、遷移動作和狀態圖守衛條件，UML順序圖具有的屬性包括順序圖守衛條件和到達狀態。

3、如權利要求1所述的驗證UML模型中動態行為與時序契約的一致性的方法，其特征在于，所述步驟A2包括以下步驟：

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

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

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

4、如權利要求1所述的驗證UML模型中動態行為與時序契約的一致性的方法，其特征在于，所述步驟A3包括以下步驟：

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

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

5、如權利要求1所述的驗證UML模型中動態行為與時序契約的一致性的方法，其特征在于，所述步驟A4包括以下步驟：

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

D2，將順序圖裝換得到的LTL時態邏輯公式進行處理，得到符合SPIN語法的Never?Claim代碼，并儲存在SPIN包下的pan.ltl文件中；

D3，提取SPIN中的參數設置創建批處理文件來模擬SPIN工具的選擇環境，選擇相應的參數，執行批處理文件，用指定的參數調用SPIN進行驗證。

6、如權利要求1所述的驗證UML模型中動態行為與時序契約的一致性的方法，其特征在于，所述步驟A5包括以下步驟：

E1，所述SPIN驗證結果生成于SPIN目錄下的pan.out文件中，將pan.out中的結果提取出來解析驗證結果并輸出；

E2，如果在所述的PROMELA所建的模型中找不到所述的LTL時態邏輯公式所描述可到達的路徑，則表示所述模型的動態行為滿足其時序契約，反之則表示所述模型的動態行為不滿足該模型的時序契約。