基于上下文定界的队列通信并发递归程序验证方法

摘要

基于上下文定界的消息队列通信并发递归程序的验证方法属于软件安全、可靠性技术领域，其特征在于通过对每个下推系统迭代地应用Post^*算法，穷尽搜索其执行的状态空间，并通过有限的上下文切换次数k利用上下文切换函数实现不同上下文间的切换，以模拟各个进程之间的交错执行，得到k次上下文执行内的可达格局集合，通过计算可达格局集合与目标格局集合的交集是否为空，判断出目标格局集合即状态是否可达，从而确定程序中存在的设计错误或漏洞，保证程序的正确与可靠。本发明无需用户过多参与，实现了基于可达性求解的程序自动化检验，而且格局计算过程简单而有效，在良序排队约束的条件下，本发明提出的上下文定界可达性是可以判定的。