-
题名基于MARTE的面向混成系统的模型形式化转换
- 1
-
-
作者
李国拯
曹子宁
-
机构
南京航空航天大学计算机科学与技术学院
-
出处
《计算机与现代化》
2015年第6期64-68,共5页
-
基金
航空科学基金资助项目(20128052064)
中央高校基本科研业务费专项资金资助项目(NZ2013306)
国家重点基础研究发展计划项目(2014CB744903)
-
文摘
混成系统是离散逻辑跳转与实时连续行为交织的复杂状态变迁系统,形式化建模与验证是确保混成系统正确性和可靠性的重要途径。首先介绍一种混成ZIA形式规范;然后,基于建模语言MARTE建立扩展Object-Z的规范,即OZMARTE,该规范弥补了MARTE规范在形式化描述方面的不足,同时为了方便描述混成系统中连续动态行为属性,给出对混成系统中连续变量的描述转换规则,增强了MARTE对混成系统的描述能力;最后,给出OZ-MARTE规范到混成ZIA规范的转换方法,因此针对混成ZIA规范的验证技术同样适用于对MARTE模型进行形式化验证。
-
关键词
混成系统
混成zia
MARTE模型
Object-Z语言
模型转换
-
Keywords
hybrid system
hybrid zia
MARTE model
Object-Z language
model transformation
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
