电子学报 ›› 2017, Vol. 45 ›› Issue (9): 2241-2249.DOI: 10.3969/j.issn.0372-2112.2017.09.027

• 学术论文 • 上一篇    下一篇

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

钱俊彦, 徐力, 古天龙, 赵岭忠, 蔡国永   

  1. 桂林电子科技大学广西可信软件重点实验室, 广西桂林 541004
  • 收稿日期:2015-11-17 修回日期:2016-07-18 出版日期:2017-09-25 发布日期:2017-09-25
  • 通讯作者: 赵岭忠
  • 作者简介:钱俊彦,男,1973年7月出生于浙江省绍兴市.博士,现为桂林电子科技大学教授.主要研究领域为软件工程、软件分析与验证、模型检验和VLSI容错.E-mail:qjy2000@gmail.com;徐力,男,1989年8月出生于湖北省天门市.硕士,主要研究方向为软件工程、软件分析与验证.E-mail:xuli890808@hotmail.com;古天龙,男,1964年11月出生于山西省芮城市.博士,现为桂林电子科技大学教授、博士生导师.主要研究领域为形式化方法、符号计算.E-mail:cctlgu@guet.edu.cn;蔡国永,男,1971年7月出生于广西区河池市.博士,现为桂林电子科技大学教授.主要研究方向为社交媒体数据挖掘、机器学习、可信软件理论.E-mail:ccgycai@guet.edu.cn
  • 基金资助:
    国家自然科学基金(No.61262008,No.61562015,No.61572146,No.U1501252);广西高等学校高水平创新团队及卓越学者计划;广西自然科学基金(No.2014GXNSFAA118365,No.2015GXNSFDA139038);广西可信软件重点实验室重点基金;桂林电子科技大学创新团队

Reachability Analysis for Time Dynamic Pushdown Networks

QIAN Jun-yan, XU Li, GU Tian-long, ZHAO Ling-zhong, CAI Guo-yong   

  1. Guangxi Key Laboratory of Trusted Software, Guilin University of Electronic Technology, Guilin, Guangxi 541004, China
  • Received:2015-11-17 Revised:2016-07-18 Online:2017-09-25 Published:2017-09-25

摘要: 动态下推网络(DPN,Dynamic Pushdown Networks)由一组能刻画动态创建线程的动态下推系统(DPDS,Dynamic PushDown Systems)组成.本文首先将描述连续时间的实时时钟引入DPN,提出了时间动态下推网络(TDPN,Timed Dynamic Pushdown Networks),能对动态创建线程的实时并发递归系统建模;然后基于时钟关键点的时钟等价优化方法,并采用on-the-fly技术,仅关心栈顶及下一层的域状态转换,动态的将连续时间模型TDPN转换为时间域表示的离散模型DPN,同时给出TDPN到DPN的转换算法;最后证明在TDPN中的可达状态当且仅当其转换状态在DPN中可达,从而可解决带动态线程创建的实时并发系统的可达性分析.

关键词: 动态下推网络, 时钟等价, 实时并发递归系统, 时间动态下推网络

Abstract: 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 time 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.

Key words: DPN, clock equivalent, real-time concurrent recursive system, TDPN

中图分类号: