基于MARTE的面向混成系统的模型形式化转换  

Hybrid System-Oriented Model Formal Transformation Based on MARTE Language

作　　者：李国拯 曹子宁[1] 

机构地区：[1]南京航空航天大学计算机科学与技术学院,江苏南京210016

出　　处：《计算机与现代化》2015年第6期64-68,共5页Computer and Modernization

基　　金：航空科学基金资助项目(20128052064);中央高校基本科研业务费专项资金资助项目(NZ2013306);国家重点基础研究发展计划项目(2014CB744903)

摘　　要：混成系统是离散逻辑跳转与实时连续行为交织的复杂状态变迁系统,形式化建模与验证是确保混成系统正确性和可靠性的重要途径。首先介绍一种混成ZIA形式规范;然后,基于建模语言MARTE建立扩展Object-Z的规范,即OZMARTE,该规范弥补了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.

关 键 词：混成系统 混成ZIA MARTE模型 Object-Z语言 模型转换 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]