Bounded reaching algorithm for communicated pushdown systems

doi:10.3778/j.issn.1002-8331.2008.24.006

Computer Engineering and Applications ›› 2008, Vol. 44 ›› Issue (24): 19-21.DOI: 10.3778/j.issn.1002-8331.2008.24.006

• 博士论坛 • Previous Articles Next Articles

Bounded reaching algorithm for communicated pushdown systems

MIAO Li,ZHANG Da-fang

Software School of Hunan University，Changsha 410082，China

Received:2008-04-11 Revised:2008-05-12 Online:2008-08-21 Published:2008-08-21
Contact: MIAO Li

通信下推系统的一种有界可达算法

缪力,张大方

湖南大学软件学院，长沙 410082

通讯作者: 缪力

Abstract

Abstract: Qadeer presented a bounded reaching algorithm for concurrent pushdown systems，which based on limiting the number of context switch，can analyze interprocedural concurrent programs.But concurrent pushdown systems simulate concurrency by global variables，which are not able to model event-drive concurrent programs.This paper presents a bounded reaching algorithm for communicated pushdown systems，which based on limiting the number of synchronization schedule and double schedule technology，can analyze event-drive concurrent programs.

Key words: bounded reaching algorithm, communicated pushdown system, interprocedural concurrent program analysis, model checking

摘要： Qadeer首次针对并发下推系统提出一种有界可达算法，通过限定上下文切换的次数使得算法可终止，可有效地分析过程间并发程序。但是并发下推系统以全局变量模拟同步，不适应于当前广泛使用的基于事件驱动的并发程序。针对通信下推系统，提出一种基于双重调度的有界可达算法，通过限定同步调度的次数，结合线程间的同步调度和线程内的路径调度解决通信下推系统的可达性问题，从而为事件驱动的过程间并发程序分析提供了算法基础。

关键词: 有界可达算法, 通信下推系统, 并发过程间程序分析, 模型检查

MIAO Li,ZHANG Da-fang. Bounded reaching algorithm for communicated pushdown systems[J]. Computer Engineering and Applications, 2008, 44(24): 19-21.

缪力,张大方. 通信下推系统的一种有界可达算法[J]. 计算机工程与应用, 2008, 44(24): 19-21.

[1]	LI Qian1, WANG Zheng1, MA Jianfen1, LI Na2. Lightweight mobile payment protocol fairness analysis [J]. Computer Engineering and Applications, 2018, 54(19): 82-87.
[2]	QIN Manman, WANG Zheng, WANG Li. Formal analysis and improvement of remote attestation protocol based on the SPIN [J]. Computer Engineering and Applications, 2017, 53(1): 34-38.
[3]	LV Jianghua1, LIU Zhifeng1, XU Yatao2, ZHOU Conghua1. Verification of correctness of attribute based access control [J]. Computer Engineering and Applications, 2016, 52(18): 98-103.
[4]	XIA Chunrui1, WANG Rui1, LI Xiaojuan1, GUAN Yong1, ZHANG Jie2, WEI Hongxing3. Probabilistic model checking for path planning in dynamic environment [J]. Computer Engineering and Applications, 2016, 52(12): 5-11.
[5]	HUANG Yankai, ZHOU Yu, WEI Ou. Novel approach for attributed graph grammar response specification verification [J]. Computer Engineering and Applications, 2016, 52(12): 15-18.
[6]	WANG Ming1, WANG Rui1, LI Xiaojuan1, GUAN Yong1, ZHANG Jie2, WEI Hongxing3. Verification of mobile robot obstacle avoidance strategies in uncertain environment based on formal modeling and probabilistic analysis [J]. Computer Engineering and Applications, 2016, 52(10): 31-38.
[7]	ZHANG Shuqing, XU Zhongwei, CHEN Zuxi. Research on modeling and verification methods of interlocking system based on term rewriting system [J]. Computer Engineering and Applications, 2014, 50(3): 49-54.
[8]	WANG Changda1，2, DONG Xuegang1, ZHOU Conghua1，2. Security analysis of E-bank online-payment based on UCON [J]. Computer Engineering and Applications, 2014, 50(16): 90-94.
[9]	TONG Chao, WANG Jianxin, QI Jiandong. Approach of constructing defect rule base and detecting source code based on formal specification [J]. Computer Engineering and Applications, 2014, 50(13): 66-72.
[10]	YOU Qifang, YANG Jinji. Model checking of SIP protocol via SPIN [J]. Computer Engineering and Applications, 2014, 50(13): 87-89.
[11]	LV Wei, HUANG Zhiqiu, CHEN Zhe, KAN Shuanglong, WEI Ou. ESpin：SPIN-based Eclipse model checking environment [J]. Computer Engineering and Applications, 2013, 49(7): 45-51.
[12]	CHEN Juanjuan, WEI Ou, HUANG Zhiqiu, CHEN Zhe. Refinement and symmetry reduction of bilattice-based multi-valued models [J]. Computer Engineering and Applications, 2013, 49(22): 40-45.
[13]	JI Lixia1, MA Jianhong1, ZHOU Qinglei2. Study of model and verification about hybrid system based on extended timed automata [J]. Computer Engineering and Applications, 2012, 48(8): 73-75.
[14]	DONG Lingling1, GUAN Yong1, LI Xiaojuan1, SHI Zhiping1, ZHANG Jie2, HUA Wei1. Verification for SpaceWire error detection mechanism by LTL model checking [J]. Computer Engineering and Applications, 2012, 48(22): 88-94.
[15]	MIAO Li, TAN Zhihua, ZHANG Dafang. Effective model checking of network authentication protocol based on SPIN [J]. Computer Engineering and Applications, 2012, 48(21): 62-67.

Bounded reaching algorithm for communicated pushdown systems

通信下推系统的一种有界可达算法

PDF

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Recommended Articles

Metrics