带数据约束的概率实时系统的验证

带数据约束的概率实时系统是指一种既带有概率时间约束又带有数据变量约束的计算系统。目前将离散数据约束和连续时间约束统一在一个概率模型中的规范及验证研究较少。提出了一种既带有连续数据约束又带有离散数据约束的规范——基于连续时间的概率ZIA规范,并给出了它的时序逻辑。对于CTL和PCTL而言,尽管这些逻辑很强大,但是只能反映时序性质,因此提出一个新的形式化语言CTML来表达度量性质查询,同时保留表达时序性质的能力并给出概率ZIA规范的验证算法。

Validation for Probability Real-time System with Data Constraints

A probabilistic real-time system with data constraints is a computing system with both probabilistic time constraints and data constraints.At present,there exist a few studies of the specification and verification that uniform discrete data constraints and sequence time constraint work in the probability model.In this paper,we proposed a specification based on sequence time probability ZIA,which has both sequence data anstraints and discrete data constraints,and gave its temporal logic.For CTL and PCTL,although the logic is very powerful,it can only reflect the temporal properties.This paper proposed a new formal language CTML to express the metric properties of query which retaines the ability to express temporal properties and gave the validation algorithm of probability of ZIA specification.