计算机与现代化Issue(6):64-68,5.DOI:10.3969/j.issn.1006-2475.2015.06.014
基于MARTE的面向混成系统的模型形式化转换
Hybrid System-Oriented Model Formal Transformation Based on MARTE Language
摘要
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 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语言/模型转换Key words
Hybrid system/Hybrid ZIA/MARTE model/Object-Z language/model transformation分类
信息技术与安全科学引用本文复制引用
李国拯,曹子宁..基于MARTE的面向混成系统的模型形式化转换[J].计算机与现代化,2015,(6):64-68,5.基金项目
航空科学基金资助项目(20128052064) (20128052064)
中央高校基本科研业务费专项资金资助项目(NZ2013306) (NZ2013306)
国家重点基础研究发展计划项目(2014CB744903) (2014CB744903)