论文部分内容阅读
随着多核处理器的高速发展,并发程序已经成为现代程序设计的主流趋势。然而并发程序的执行存在不确定性,这使得传统的测试方法很难发现程序中隐匿的错误,一旦并发程序出现执行故障,将会给国家及人民带来难以估量的灾难性损失。因此,如何验证并发程序的正确性已经成为当今软件形式化验证领域中日益紧迫的问题。 本文研究的重点是基于约束技术的并发程序验证,具体通过模型检测中的约束技术将并发程序的验证问题转化为其抽象模型的可达性问题进行分析,从而判定抽象模型是否满足系统预期的性质。可达性分析通过判断系统状态空间中的某一状态是否可达来判定程序执行的正确性,其是模型检测中的重要核心技术。本文主要研究工作如下: (1)研究了作为并发程序通用抽象模型的多栈下推系统模型,并运用多栈下推系统对并发程序进行建模。根据并发程序的执行方式,提出一种针对多栈下推系统的语义约束方法。将约束后的抽象模型称为SMpds,此类模型可以用来模拟交互更为频繁的并发程序。 (2)采用针对SMpds模型的限定匹配关系阶段的模型检测约束方法将验证问题转换为该抽象模型的可达性问题进行求解,并运用自动机理论对SMpds的可达性问题进行分析,证明其可达性问题是可以判定的。具体方法是将SMpds的可达性判定问题转化为在其可达图GM中搜索某个状态是否可达来判定系统是否满足预期性质。 (3)研究了基于消息队列交互的并发程序的可达性问题,并采用限定步长的模型检测约束方法,限定了其在状态迁移空间中所能搜索的步长数,同时证明其限定步长的可达性问题是可以判定的。提出一种将消息队列并发程序转化为多栈下推系统的转化方法,从而将消息队列并发程序的可达性问题转换为多栈下推系统的定界可达性问题进行求解。同时提出一种针对多栈下推系统的限定搜索步长数的定界可达算法,利用该算法计算k个步长内并发程序的可达格局集合,并将其与目标格局集合取交后判空,最终验证此类并发程序的可达性问题。