基于时间动态下推网络可达性分析

摘要

Dynamic pushdown networks (DPN) consist of a group of dynamic pushdown systems (DPNS).And each DPNS model can dynamically demonstrate as new threads.Firstly,this paper introduces the real numeric clock to DPN to verify the real-time concurrent recursive system created by dynamic threads,and demonstrate it as time dynamic pushdown networks (TDPN).Secondly,this paper uses the clock equivalent optimization technique based on rime key to convert a continuous TDPN models into a series of discrete TDPN models.Besides,this paper proposes the equivalence algorithm of TDPN into DPN.At last,we prove the status in TDPN is reachable if and only if its transition status in DPN is reachable.At the same time,this paper solves reachability problem of the real-time concurrent system created by dynamic threads.%动态下推网络(DPN,Dynamic Pushdown Networks)由一组能刻画动态创建线程的动态下推系统(DPDS,Dynamic PushDown Systems)组成.本文首先将描述连续时间的实时时钟引入DPN,提出了时间动态下推网络(TDPN,Timed Dynamic Pushdown Networks),能对动态创建线程的实时并发递归系统建模;然后基于时钟关键点的时钟等价优化方法,并采用on-the-fly技术,仅关心栈顶及下一层的域状态转换,动态的将连续时间模型TDPN转换为时间域表示的离散模型DPN,同时给出TDPN到DPN的转换算法;最后证明在TDPN中的可达状态当且仅当其转换状态在DPN中可达,从而可解决带动态线程创建的实时并发系统的可达性分析.