Abstract: Hybrid systems are statetransition systems consisting of discrete control mode transformation and continuous real time behavior. Formal modeling and verification for hybrid systems are an important way to ensure the correctness and reliability of the systems. In this paper, we first introduce a Hybrid ZIA formal specification. Then, we expand the MARTE Language with ObjectZ, named OZMARTE, which makes up the shortcoming of formal description aspect of MARTE. Also, to describe the continuous dynamical property in hybrid systems, we propose the transformational rule of the continuous variable, which enhances the capability of modeling hybrid systems. Finally, we give the transformation method from OZMARTE to Hybrid ZIA. So verification techniques for Hybrid ZIA also apply to the verification of MARTE models.

Key words: Hybrid system, Hybrid ZIA, MARTE model, Object-Z language, model transformation