[發明專利]基于UPPAAL的實時嵌入式系統構件間協同行為的驗證方法

有效

• 申請號: 201110423095.4
• 申請日: 2011-12-16
• 公開（公告）號: CN102567163A
• 公開（公告）日: 2012-07-11
• 發明（設計）人: 杜德慧;溫巖;馮曙光;包丹珠;徐亞祎;杜麗
• 申請（專利權）人: 華東師范大學
• 主分類號: G06F11/26
• 分類號: G06F11/26
• 代理公司: 上海藍迪專利事務所 31215
• 代理人: 徐筱梅;張翔

1.一種基于UPPAAL的實時嵌入式系統構件間協同行為的驗證方法，其特征在于該方法是：將實時嵌入式系統建模形成的MARTE模型轉化為工具UPPAAL能夠驗證的時間自動機，然后使用UPPAAL工具對時間自動機驗證，并得出驗證結果；具體包括以下步驟：

a、實時嵌入式系統MARTE模型轉化為時間自動機

ⅰ)、對于MARTE模型中有CCSL約束的MARTE構件圖，根據CCSL語義將構件模型轉化為仿真自動機；?

ⅱ)、對于MARTE模型中沒有CCSL約束的MARTE構件圖，首先，將模型中的MARTE順序圖轉化為監控自動機；然后，將模型中的MARTE狀態圖轉化為對象時間自動機；?

b、使用工具UPPAAL對轉化好的時間自動機模型進行驗證并輸出驗證結果。

2.根據權利要求1所述的驗證方法，其特征在于所述根據CCSL語義將構件模型轉化為仿真自動機是：根據各個端口CCSL語義，將構件的每一個端口建模成一個從時間自動機，各從時間自動機負責模擬對應端口的協同行為；同時將整個構件建模為主時間自動機，主時間自動機通過同步機制控制各從自動機的行為。

3.根據權利要求1所述的驗證方法，其特征在于所述將模型中的MARTE順序圖轉化為監控自動機的過程是：模型驗證是通過message的傳遞作為建模依據的；首先，將message作為一個監控對象，根據每一個message的接收方和發送方，message的前后關系和message中所包含的時間約束對應地生成UPPAAL監控自動機的狀態遷移和信號變量，然后再轉化為監控自動機，用來對整個系統的交互行為進行監控。

4.根據權利要求1所述的驗證方法，其特征在于所述將模型中的MARTE狀態圖轉化為時間自動機的過程是：MARTE狀態圖對應地為一個系統構件建模；構件內部的事件信息通過MARTE狀態圖表示；事件信息包括外部交互信息和內部的更新信息；將MARTE狀態圖中的各狀態一一對應地轉化為時間自動機中的location，根據狀態之間的遷移相應地轉化為時間自動機中的edge，對于狀態圖中對其他對象的調用轉化為synchronization，將狀態圖內部變量更新轉化為effect，狀態圖中控制變量轉化為guard；最后再在涉及到交互的edge中加入額外的synchronization和effect，以便監控自動機收集信號。