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

Verification of Real-Time Systems with Time Multi-Pushdown Net

作　　者：钱俊彦[1] 甘鹏程 郭云川[2] 赵岭忠[1] 古天龙[1] 

机构地区：[1]桂林电子科技大学广西可信软件重点实验室,广西桂林541004 [2]中国科学院信息工程研究所,北京100093

出　　处：《计算机学报》2016年第11期2253-2269,共17页Chinese Journal of Computers

基　　金：国家自然科学基金(61262008;61562015;61572146;U1501252);广西自然科学基金(2012GXNSFAA053220;2014GXNSFAA118365;2015GXNSFDA139038);广西高等学校高水平创新团队及卓越学者计划;广西可信软件重点实验室重点基金;桂林电子科技大学创新团队资助~~

摘　　要：多栈下推网络(MPDN)是利用多个栈来描述并发递归程序线程之间交互的一种下推系统模型.为了描述基于线程之间交互的实时并发递归程序,首先将描述连续时间的时钟引入到MPDN,提出了时间多栈下推网络(TMPDN),并给出了语法及其操作语义;其次利用基于时间关键点的时钟等价优化技术,缩减等价域状态空间;然后通过静态转换方法,获得所有的可达域状态格局,将连续时间的TMPDN模型转换成离散的MPDN模型.在此基础上,基于on-the-fly技术,采用动态转换方法,仅关心栈顶域状态转换,进一步缩减转换后的状态空间.同时证明了状态q_F在TMPDN可达当且仅当其转换状态q′_F在MPDN可达,并给出了模型转换算法;最后可采用现有模型检验工具验证转换后的MPDN.Multi-Pushdown Net(MPDN)is a model of pushdown systems that makes use of multiple stacks to describe the interaction between threads of concurrent recursive programs.In order to model real-time concurrent recursive procedures based on thread interaction,a new model,i.e.time multiple stack pushdown network(TMPDN),is proposed by introducing a clock into MPDN to describe the continuous time.We give the syntax and operational semantics of TMPDN.Based on this definition,an optimization technique of clock domain equivalence that makes use of key time points is proposed to reduce the space of equivalence domains.Then static conversion methods are presented to obtain all reachable domains and based on which to convert a continuous time TMPDN into a discrete MPDN.Next a dynamic conversion method,the so-called on-the-fly technique,is used to further reduce the state space obtained by static methods,and in this process it is concerned only with the state transformation of the stack-top domains.Corresponding model transformation algorithms are given in this paper.It is proved that the state q_F in TMPDN can be reached if and only if the transition state q′_F in the corresponding MPDN canbe reached.The MPDN obtained by the above transformation can be verified using existing model checkers.

关 键 词：MPDN TMPDN 并发递归程序 时钟等价 可达性 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]