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

发布时间：2017-06-12 22:03

  本文关键词：基于时间多栈下推网络的实时系统验证，，由笔耕文化传播整理发布。

【摘要】：多栈下推网络(MPDN)是利用多个栈来描述并发递归程序线程之间交互的一种下推系统模型.为了描述基于线程之间交互的实时并发递归程序,首先将描述连续时间的时钟引入到MPDN,提出了时间多栈下推网络(TMPDN),并给出了语法及其操作语义;其次利用基于时间关键点的时钟等价优化技术,缩减等价域状态空间;然后通过静态转换方法,获得所有的可达域状态格局,将连续时间的TMPDN模型转换成离散的MPDN模型.在此基础上,基于on-the-fly技术,采用动态转换方法,仅关心栈顶域状态转换,进一步缩减转换后的状态空间.同时证明了状态q_F在TMPDN可达当且仅当其转换状态q′_F在MPDN可达,并给出了模型转换算法;最后可采用现有模型检验工具验证转换后的MPDN.
【作者单位】： 桂林电子科技大学广西可信软件重点实验室;中国科学院信息工程研究所;
【关键词】： MPDN TMPDN 并发递归程序 时钟等价 可达性
【基金】：国家自然科学基金(61262008,61562015,61572146,U1501252) 广西自然科学基金(2012GXNSFAA053220,2014GXNSFAA118365,2015GXNSFDA139038) 广西高等学校高水平创新团队及卓越学者计划 广西可信软件重点实验室重点基金 桂林电子科技大学创新团队资助~~
【分类号】：TP311.1;TP301.1
【正文快照】： 科学基金(2012GXNSFAA053220,2014GXNSFAA118365,2015GXNSFDA139038)、广西高等学校高水平创新团队及卓越学者计划、广西可信软件重点实验室重点基金、桂林电子科技大学创新团队资助.钱俊彦,男,1973年生,博士,教授,中国计算机学会(CCF)高级会员,主要研究领域为软件工程、模型

  本文关键词：基于时间多栈下推网络的实时系统验证，由笔耕文化传播整理发布。

本文编号：445009