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

摘要：

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

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

所属期刊栏目：44

分类号：TP311.5(计算技术、计算机技术)

资助基金：国家自然科学基金60673155;90718008

在线出版日期：2008-10-20（万方平台首次上网日期，不代表论文的发表时间）

页数：共3页

页码：19-21