[發明專利]一種基于模型驅動工程進行SysML狀態機圖分析驗證的方法

有效

• 申請號: 201210531992.1
• 申請日: 2012-12-11
• 公開（公告）號: CN103065000A
• 公開（公告）日: 2013-04-24
• 發明（設計）人: 張天;李江偉;李宣東
• 申請（專利權）人: 南京大學
• 主分類號: G06F17/50
• 分類號: G06F17/50
• 代理公司: 南京瑞弘專利商標事務所(普通合伙) 32249
• 代理人: 陳建和

1.一種基于模型驅動工程進行SysML狀態機圖分析驗證的方法，其特征是包括步驟：?

步驟10：根據編輯器設計一個SysML狀態機圖；?

步驟11：設計狀態機圖的時鐘；?

步驟12：新建一個ATL工程；?

步驟13：將用戶設計的狀態機圖及我們提供的兩個元模型和一個轉換文件導入到工程中；?

步驟14：運行轉換文件得到結果文件；?

步驟15：將結果文件用Uppaal打開，模擬分析及驗證用戶設計的SysML狀態機圖。?

2.根據權利要求1所述的基于模型驅動工程進行SysML狀態機圖分析驗證的方法，其特征是所述的設計一個SysML狀態機圖即步驟10的具體步驟如下：?

步驟200：用eclipse運行SysML狀態機圖編輯器；?

步驟201：右鍵單擊根節點，新建一個或多個Region；?

步驟202：右鍵單擊Region節點，創建系統中所需要的State節點，同時為每個State節點命名，如果State節點有時限變量，則跳轉到步驟203，否則跳轉到步驟204；?

步驟203：右鍵單擊State節點，增加時限變量節點，并設置初始值；?

步驟204：右鍵單擊Region節點，創建系統中所需要的Transition節點，同時為每個Transition節點命名及指定源和目標狀態；?

步驟205：右鍵單擊Region節點，增加局部變量聲明節點；?

步驟206：右鍵單擊Region節點，增加參數節點；?

步驟207：右鍵單擊Region節點，增加名字節點；?

步驟208：右鍵單擊根節點，增加全局變量聲明節點；?

步驟209：右鍵單擊根節點，增加系統模型聲明節點；?

步驟210：結束本次SysML狀態機圖設計。?

3.根據權利要求1所述的基于模型驅動工程進行SysML狀態機圖分析驗證的方法，其特征是所述的設計狀態機圖的時鐘即步驟11中步驟如下：?

要描述時間觸發機制，首先需要對時間進行建模，建立系統的時間訪問入口：時鐘，具體過程為：?

步驟30：建立一個離散的時鐘類，采用《ClockType》構造型表明該類是一個時鐘類，并在約束中描述相應的標記值來定義其他特征；?

步驟31：導入MARTE庫中的idealClk實例，代表實際物理時間的連續時鐘；?

步驟32：定義離散時鐘類的兩個實例（clk1，clk2）。?

4.根據權利要求1所述的基于模型驅動工程進行SysML狀態機圖分析驗證的方?法，其特征是創建一個新的ATL工程并將設計的SysML狀態機圖和兩個元模型和一個轉換文件導入到工程即步驟12和步驟13，過程包括：?

步驟40：安裝ATL插件；?

步驟41：將設計的SysML狀態機圖和我們提供的兩個元模型和一個轉換文件導入到工程。?

5.根據權利要求1所述的基于模型驅動工程進行SysML狀態機圖分析驗證的方法，其特征是執行轉換文件即步驟14，其中執行的過程包括：?

步驟51：狀態機圖到時間自動機網絡的轉換；?

步驟52：狀態機圖Region到時間自動機的轉換；?

步驟53：狀態機圖中狀態到時間自動機Location和分支點的轉換；?

步驟54：狀態機圖中狀態圖遷移到時間自動機遷移的轉換；?

步驟55：狀態機圖中初始狀態到時間自動機初始節點的轉換；?

步驟56：狀態機圖中遷移上的衛式，觸發動作，觸發后的行為到時間自動機遷移上Label的轉換；?

步驟57：狀態機圖中概率到時間自動機概率的轉換；?

步驟58：狀態機圖中時間約束到時間自動機時間約束的轉換；?

步驟59：得到轉換結果文件。?

6.根據權利要求1所述的基于模型驅動工程進行SysML狀態機圖分析驗證的方法，其特征是SysML狀態機圖設計模型的模擬，分析與驗證即步驟15，其過程包括：?

步驟61：用模型檢驗工具Uppaal打開轉換結果文件；?

步驟62：在模擬器標簽中，通過點擊下一步來模擬系統的運行過程；模擬過程能夠保存文件；?

步驟63：在驗證器標簽中，通過點擊添加按鈕來增加系統的一條驗證性質；?

步驟64：在驗證器標簽中，通過構造簡單CTL表達式來表示系統的某些性質；?

步驟65：在驗證器標簽中，通過點擊開始驗證按鈕來驗證某條性質是否滿足，若不滿足可以得到一個反例；?

步驟66：在驗證器標簽中，通過點擊刪除按鈕，刪除某條不再需要的性質；?

步驟67：；在驗證器標簽中，驗證結果與進度顯示了整個驗證過程和結果。?