Formal method of MARTE model based on MDA
基于MDA的MARTE模型形式化方法

For the reliability and predictability requirements of embedded systems, this paper proposed MDA-based method to formal describe MARTE, which was a modeling language for embedded systems. It established Object-Z metamodel, and defined model transformation relationship between MARTE metamodel and Object-Z metamodel. It also presented the specific process of semantic mapping and the syntax conversion between MARTE model and Object-Z model. The method supported the formal translation between MARTE model and Object-Z model, it was helpful to test and verify in the early stage of the software development.