CAJ | 학술논문

混成系统是离散逻辑跳转与实时连续行为交织的复杂状态变迁系统,形式化建模与验证是确保混成系统正确性和可靠性的重要途径。首先介绍一种混成ZIA形式规范；然后,基于建模语言MARTE建立扩展Object-Z的规范,即OZ-MARTE,该规范弥补了MARTE规范在形式化描述方面的不足,同时为了方便描述混成系统中连续动态行为属性,给出对混成系统中连续变量的描述转换规则,增强了MARTE对混成系统的描述能力；最后,给出OZ-MARTE规范到混成ZIA规范的转换方法,因此针对混成ZIA规范的验证技术同样适用于对MARTE模型进行形式化验证。
혼성계통시리산라집도전여실시련속행위교직적복잡상태변천계통,형식화건모여험증시학보혼성계통정학성화가고성적중요도경。수선개소일충혼성ZIA형식규범；연후,기우건모어언MARTE건립확전Object-Z적규범,즉OZ-MARTE,해규범미보료MARTE규범재형식화묘술방면적불족,동시위료방편묘술혼성계통중련속동태행위속성,급출대혼성계통중련속변량적묘술전환규칙,증강료MARTE대혼성계통적묘술능력；최후,급출OZ-MARTE규범도혼성ZIA규범적전환방법,인차침대혼성ZIA규범적험증기술동양괄용우대MARTE모형진행형식화험증。
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 Ob-ject-Z, named OZ-MARTE, which makes up the shortcoming of formal description aspect of MARTE. Also, to describe the con-tinuous 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 verifica-tion techniques for Hybrid ZIA also apply to the verification of MARTE models.