基于时间动态下推网络可达性分析
发布时间：2018-10-11 13:35
【摘要】：动态下推网络(DPN,Dynamic Pushdown Networks)由一组能刻画动态创建线程的动态下推系统(DPDS,Dynamic Push Down Systems)组成.本文首先将描述连续时间的实时时钟引入DPN,提出了时间动态下推网络(TDPN,Timed Dynamic Pushdown Networks),能对动态创建线程的实时并发递归系统建模;然后基于时钟关键点的时钟等价优化方法,并采用on-the-fly技术,仅关心栈顶及下一层的域状态转换,动态的将连续时间模型TDPN转换为时间域表示的离散模型DPN,同时给出TDPN到DPN的转换算法;最后证明在TDPN中的可达状态当且仅当其转换状态在DPN中可达,从而可解决带动态线程创建的实时并发系统的可达性分析.
[Abstract]:Dynamic pushdown network (DPN,Dynamic Pushdown Networks) consists of a set of dynamic push systems (DPDS,Dynamic Push Down Systems) that can depict dynamically created threads. In this paper, a real-time clock describing continuous time is introduced into DPN,. A time-dynamic pushdown network (TDPN,Timed Dynamic Pushdown Networks),) is proposed to model the real-time concurrent recursive system with dynamically created threads, and then the clock equivalence optimization method based on the key points of the clock is proposed. Using on-the-fly technology, we only care about the domain state transition between the top of stack and the next layer, and dynamically convert the continuous time model (TDPN) into the discrete model (DPN,) expressed in time domain. At the same time, we give the transform algorithm from TDPN to DPN. Finally, the reachable state in TDPN is proved if and only if the transition state is reachable in DPN, thus solving the reachability analysis of real-time concurrent systems created with dynamic threads.
【作者单位】： 桂林电子科技大学广西可信软件重点实验室;
【基金】：国家自然科学基金(No.61262008,No.61562015,No.61572146,No.U1501252) 广西高等学校高水平创新团队 卓越学者计划 广西自然科学基金(No.2014GXNSFAA118365,No.2015GXNSFDA139038) 广西可信软件重点实验室重点基金 桂林电子科技大学创新团队
【分类号】：TP301.1;TP311.1
本文编号：2264363
[Abstract]:Dynamic pushdown network (DPN,Dynamic Pushdown Networks) consists of a set of dynamic push systems (DPDS,Dynamic Push Down Systems) that can depict dynamically created threads. In this paper, a real-time clock describing continuous time is introduced into DPN,. A time-dynamic pushdown network (TDPN,Timed Dynamic Pushdown Networks),) is proposed to model the real-time concurrent recursive system with dynamically created threads, and then the clock equivalence optimization method based on the key points of the clock is proposed. Using on-the-fly technology, we only care about the domain state transition between the top of stack and the next layer, and dynamically convert the continuous time model (TDPN) into the discrete model (DPN,) expressed in time domain. At the same time, we give the transform algorithm from TDPN to DPN. Finally, the reachable state in TDPN is proved if and only if the transition state is reachable in DPN, thus solving the reachability analysis of real-time concurrent systems created with dynamic threads.
【作者单位】： 桂林电子科技大学广西可信软件重点实验室;
【基金】：国家自然科学基金(No.61262008,No.61562015,No.61572146,No.U1501252) 广西高等学校高水平创新团队 卓越学者计划 广西自然科学基金(No.2014GXNSFAA118365,No.2015GXNSFDA139038) 广西可信软件重点实验室重点基金 桂林电子科技大学创新团队
【分类号】：TP301.1;TP311.1
【相似文献】
相关期刊论文 前5条
1 缪力;张大方;;通信下推系统的一种有界可达算法[J];计算机工程与应用;2008年24期
2 孙聪;唐礼勇;陈钟;;基于下推系统可达性分析的输出信道信息流检测[J];计算机科学;2011年07期
3 孙聪;唐礼勇;陈钟;;基于下推系统可达性分析的程序机密消去机制[J];软件学报;2012年08期
4 刘耀东;为BROWSE配置下推按钮[J];电脑编程技巧与维护;1995年09期
5 孙聪;唐礼勇;陈钟;马建峰;;基于加权下推系统优化可达性分析的Java安全信息流研究[J];计算机研究与发展;2012年05期
相关硕士学位论文 前1条
1 靳阳;良结构下推系统的表达能力[D];上海交通大学;2015年
，本文编号：2264363
本文链接：https://www.wllwen.com/kejilunwen/ruanjiangongchenglunwen/2264363.html
