【摘要】 针对消息队列并发程序执行过程中可达性问题上存在的不确定性,将消息队列并发程序转换为多栈下推系统,利用饱和过程,构造一个可以接收逆向格局集合的非确定型有限自动机,并给出相应的求解算法,证明了逆向格局集合的可达性,进而验证了此类并发程序的可达性。更多还原

【Abstract】 According to the non-determinacy during the execution of concurrent programs based on message queues, this paper convert concurrent program communicating using message queues to the multi-stack pushdown system, moreover uses the saturation procedure to construct an automaton which can recognize the sets of backward configuration, then the relevant solving algorithm is provided, thus further proves that the backward reachability of configuration sets is decidable. Consequently, the reachability problem for these concurrent queue programs is solved.更多还原