基于时间多栈下推网络的实时系统验证

多栈下推网络(MPDN)是利用多个栈来描述并发递归程序线程之间交互的一种下推系统模型.为了描述基于线程之间交互的实时并发递归程序,首先将描述连续时间的时钟引入到MPDN,提出了时间多栈下推网络(TMPDN),并给出了语法及其操作语义;其次利用基于时间关键点的时钟等价优化技术,缩减等价域状态空间;然后通过静态转换方法,获得所有的可达域状态格局,将连续时间的TMPDN模型转换成离散的MPDN模型.在此基础上,基于on-the-fly技术,采用动态转换方法,仅关心栈顶域状态转换,进一步缩减转换后的状态空间.同时证明了状态q_F在TMPDN可达当且仅当其转换状态q′_F在MPDN可达,并给出了模型转换算法;最后可采用现有模型检验工具验证转换后的MPDN.