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

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