A Formal Transformation Approach of MARTE Model

Formal method is a good way to enhance the reliability and to verify the system properties of the embedded system. This paper presents a formal transformation approach from MARTE model to Object-Z model in the MDA framework, and defines the transformation rules of structure and behaviour semantic on the basis of the meta-model. Though the approach, we can get a precise specification and can verify the correctness of the system properties at the design stage. This approach is applied to a specific case study to implement formal transformation from MARTE to Object-Z. The result demonstrates that the approach could improve the accuracy of system model by transforming it into Object-Z specification and enhance the reliability of software system before implement.