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

摘要：

混成系统是离散逻辑跳转与实时连续行为交织的复杂状态变迁系统,形式化建模与验证是确保混成系统正确性和可靠性的重要途径。首先介绍一种混成ZIA形式规范；然后,基于建模语言MARTE建立扩展Object-Z的规范,即OZ-MARTE,该规范弥补了MARTE规范在形式化描述方面的不足,同时为了方便描述混成系统中连续动态行为属性,给出对混成系统中连续变量的描述转换规则,增强了MARTE对混成系统的描述能力；最后,给出OZ-MARTE规范到混成ZIA规范的转换方法,因此针对混成ZIA规范的验证技术同样适用于对MARTE模型进行形式化验证。

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

分类号：TP311(计算技术、计算机技术)

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

在线出版日期：2015-07-07（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：64-68