带数据约束实时系统的模型检测

摘要：

带数据约束的实时系统是指一种既带有时间约束又带有数据变量约束的计算系统.目前将离散数据约束和连续时间约束统一在一个模型中的规范及验证研究较少.文中提出了一种既带有连续数据约束又带有离散数据约束的规范——基于连续时间的ZIA规范,并给出它的时序逻辑.MARTE是UML在嵌入式实时系统领域的建模规范,在工业界的应用非常广泛,但是目前对其模型检测的研究较少.在MARTE的基础上扩展Z,提出了Z-MARTE,并将Z-MARTE转换为基于连续时间的ZIA模型,在实现对连续时间ZIA模型检测的同时,也实现了对Z-MARTE的模型检测.最后通过一个实例进行验证,说明此方法可行有效.

关键词：数据约束、实时系统、连续时间、MARTE、ZIA、模型检测

所属期刊栏目：41

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

资助基金：航空科学基金20128052064;中央高校基本科研业务费专项资金NZ2013306;国家重点基础研究发展计划973计划2014CB744900;江苏省计算机信息处理技术重点实验室开放课题209035

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

页数：共10页

页码：254-262,269