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

• 作者: 曹子宁 李国拯
• 来源期刊: 计算机与现代化
• 学科: 工学
• 关键词: 混成系统 混成ZIA MARTE模型 Object-Z语言 模型转换
• 年，卷（期）: 2015,（6）
• 所属期刊栏目: 信息系统
• 页码范围: 64-68
• 页数: 5页
• 分类号: TP311
• 字数: 4714字
• 语种: 中文
• DOI: 10.3969/j.issn.1006-2475.2015.06.014

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	曹子宁	南京航空航天大学计算机科学与技术学院	25	200	8.0	13.0
2	李国拯	南京航空航天大学计算机科学与技术学院	2	1	1.0	1.0