基于MDA的MARTE模型形式化轉換*

王立杰，劉昌祿，俞烈彬

(江蘇自動化研究所，江蘇 連云港 222006)

嵌入式系統是一種嵌入到具體設備中，對性能、成本、功耗等有嚴格要求的專用計算機系統，目前已經廣泛應用于軍事、通訊、醫療、交通等行業中。運行時系統功能的失效或者違反安全性、可靠性、實時性等非功能屬性都將導致災難性的后果［1］。因此，提高軟件可信性成為嵌入式軟件開發領域的重要課題。

MARTE(Modeling and Analysis of Real Time and Embedded systems)是UML在嵌入式實時系統領域的建模規范［2］，彌補了UML對嵌入式實時領域的非功能屬性的表達能力的不足。UML/MARTE規范采用圖形化的方式描述系統，缺乏精確的語義信息，因此難以直接進行一致性驗證。形式化方法提供了一種嚴格精確的數學方法，通常被用于軟件設計階段，分析系統的可靠性［3］。Ahmed M.Mostafa等提出使用Z形式化UML用例圖、類圖、狀態圖等［4］。張天等利用AMMA平臺，在元模型層定義了MARTE到FIACRE的映射關系，完成了異構轉換［5］。Soon-Kyeong Kim and David Carrington提出了元建模方法完成從UML圖到Object-Z的轉換，兩種語言定義在元模型層次，保證了轉換的精確性，完整性和一致性［6］。目前研究者對UML的形式化進行了多方面的研究，并考慮MARTE與嵌入式系統的其它建模語言進行轉換或集成，但對于MARTE模型的形式化基礎研究的還比較少。

本文首先建立了擴展的Object-Z的元模型，以方便描述嵌入式時間和資源非功能屬性。然后在MDA框架下分別定義MARTE靜態結構圖，動態行為圖和時間資源非功能屬性到Object-Z語義的轉換規則，實現MARTE模型到Object-Z規約之間的轉換。從而可以根據Object-Z規范及其推理技術對MARTE模型進行形式化的驗證。……