基於MARTE的實時系統模型驅動架構關鍵問題研究

《基於MARTE的實時系統模型驅動架構關鍵問題研究》是依託華東師範大學，由劉靜擔任項目負責人的面上項目。

基本介紹

• 中文名：基於MARTE的實時系統模型驅動架構關鍵問題研究
• 項目類別：面上項目
• 項目負責人：劉靜
• 依託單位：華東師範大學

項目摘要

國際對象管理組織OMG將模型驅動架構，作為提高軟體質量與開發效率最有前景的方法, 並於2010年8月發布模型驅動實時系統建模規範MARTE。但MARTE 模型缺乏嚴格的語義，特別是多時鐘系統的時間關係語義，不能精確地描述帶多類混合時間約束的模型系統，不能對反應性進行精確建模，並保證模型的正確性、一致性。本項目研究採用形式方法，探索解決多抽象層次、多視角MARTE模型中的時間關聯、模型正確性驗證、模型一致性幾個關鍵問題的理論和方法。研究將統一程式理論與MARTE規範和時間約束語言CCSL結合起來，針對包含大量並發事件、隨機事件的複雜實時系統軟體設計中的關鍵問題，探索給出精確建模的方法，並給出模型轉換規則、模型精化策略與有效進行模型驗證的手段，最後將研究成果套用於上海軌道交通列控系統設計，力爭為提高我國自主研發安全攸關實時系統軟體開發能力作出貢獻。

結題摘要

項目的背景模型驅動架構中，包含大量並發事件與隨機事件的複雜實時系統模型構造、帶時間約束的模型檢查與模型一致性保證一直是系統可信性保證中的難題。國際對象管理組織 OMG發布了針對模型驅動式實時系統的建模規範 MARTE，但MARTE 模型缺乏嚴格的語義，特別是多時鐘系統的時間關係語義，不能精確地描述帶多類混合時間約束的模型系統，不能對反應性進行精確建模，並保證模型的正確性、一致性。本項目研究採用形式方法，探索解決多抽象層次、多視角MARTE 模型中的時間關聯、模型正確性驗證、模型一致性問題的理論和方法。 主要研究內容本項目主要研究實時系統軟體建模規範 MARTE 和時間約束語言 CCSL，針對 MARTE 實時系統時間結構模型構造的特點, 建立統一的離散/稠密時間模型；研究 MARTE/CCSL 時間模型中的多時鐘約束關聯，和保證多視角、多抽象層次 MARTE 模型一致性策略；並對驗證方法進行最佳化，驗證安全性、活性；改進、擴充和完善本課題組已經開發的模型驅動可信軟體開發系統Trustable MDA 1.0，以支持實時系統建模與驗證。 重要結果本課題從建立MARTE規範統一的離散/稠密時間模型入手，將形式化的軟體規約技術套用到MARTE多層次模型構建中，對實時系統軟體類型的多樣性、離散狀態和連續狀態統一性、軟體實體和運行環境的協同等特性進行了深入的研究。建立了實時系統的狀態模型、通信模型、構件模型、體系結構模型，並從語義上給出了模型的安全條件。系統地給出了一系列提高MARTE軟體模型精確性和保持MARTE模型一致性的方法，以及面向軌道交通運控系統的最佳化驗證策略。開發了模型驅動式可信實時系統軟體集成開發環境。將研究成果與工具套用到北京房山線的列車控制系統。 關鍵數據及其科學意義在連續離散融合的混成系統模型研究中，我們獲得了邊遷移和一種特殊類型的演化遷移，邊遷移發生在離散的時間點，而演化遷移則發生在兩個離散時間點之間的時間區間。通過兩類遷移可以同時對離散時間變數和連續時間變數的變化過程進行統一的描述。演化遷移可定義由模式中的連續變數的變化而引起的從模式到自身的遷移。在含有連續變數的系統中，當模式中的連續變數隨著時間的流逝而變化時，通過該遷移可以將模式轉變和系統環境聯繫起來。我們還獲得了模型的安全語義和活性語義。