| 通信下推系统的一种有界可达算法 |
| |
| 引用本文： | 缪力,张大方. 通信下推系统的一种有界可达算法[J]. 计算机工程与应用, 2008, 44(24): 19-21. DOI: 10.3778/j.issn.1002-8331.2008.24.006 |
| |
| 作者姓名： | 缪力 张大方 |
| |
| 作者单位： | 湖南大学软件学院,长沙,410082;湖南大学软件学院,长沙,410082 |
| |
| 摘 要： | Qadeer首次针对并发下推系统提出一种有界可达算法，通过限定上下文切换的次数使得算法可终止，可有效地分析过程间并发程序。但是并发下推系统以全局变量模拟同步，不适应于当前广泛使用的基于事件驱动的并发程序。针对通信下推系统，提出一种基于双重调度的有界可达算法，通过限定同步调度的次数，结合线程间的同步调度和线程内的路径调度解决通信下推系统的可达性问题，从而为事件驱动的过程间并发程序分析提供了算法基础。
|
| 关 键 词： | 有界可达算法 通信下推系统 并发过程间程序分析 模型检查 |
| 收稿时间： | 2008-04-11 |
| 修稿时间： | 2008-5-12 |
Bounded reaching algorithm for communicated pushdown systems |
| |
| MIAO Li,ZHANG Da-fang. Bounded reaching algorithm for communicated pushdown systems[J]. Computer Engineering and Applications, 2008, 44(24): 19-21. DOI: 10.3778/j.issn.1002-8331.2008.24.006 |
| |
| Authors: | MIAO Li ZHANG Da-fang |
| |
| Affiliation: | Software School of Hunan University，Changsha 410082，China |
| |
| 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. |
| |
| Keywords: | bounded reaching algorithm communicated pushdown system interprocedural concurrent program analysis model checking |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程与应用》浏览原始摘要信息 |
|
点击此处可从《计算机工程与应用》下载免费的PDF全文 |
