程序合成是软件开发中的一个重要研究问题,其主要目标是自动生成符合给定规约的可执行代码。随着计算机技术的发展,程序变得越来越复杂,其正确性也越来越难以保证,这也使得程序合成的研究得到越来越多的重视。其中,并发程序行为高度复杂,极易出错,因此,如何对其进行自动程序合成是相关领域的重要研究内容。传统的并发程序合成方法主要通过证明,推导等方式进行代码构造,这些方法大多存在复杂度高、自动化程度低、时间开销大等问题。近年来,以遗传算法为代表的基于搜索的并发程序合成方法被提出。其基本思路为随机生成大量代码样本后对每个样本进行评估,基于评估值通过遗传算法等方式对代码样本进行变换与搜索。现有方法直接使用模型检验对每个样本直接进行验证来进行评估,在性能和可用性上有较大限制。一,对每个样本分别进行验证时间开销极大,性能低下,二,每次验证仅得到样本满足与否,评估粒度过粗,不利于搜索收敛。针对上述问题,我们进行了系统化研究:●针对传统方法存在的时间开销大和打分粗粒度的问题,本文提出一种基于统计评估的并发程序合成方法,此方法核心思想是通过对程序执行路径的检查和对结果的统计实现对程序适应度的评估。此方法只需模拟程序执行生成一组路径,并对路径进行检查,无需遍历程序状态空间,所以时间开销大幅降低。对一组路径的检查结果的统计情况富有多样性,从而可以达到细粒度评分。●基于统计评估的并发程序合成方法虽然有时间开销小,适应度打分平滑的优点,但是解决不同问题时,对路径进行验证的模块需要不同的代码实现。针对这个问题我们提出了更具有普适性的方法:基于统计模型检验的并发程序合成方法,该方法将表示程序行为的逻辑规约转换为表示路径行为的有界规约,使用统计模型检验评估程序满足有界规约的概率,最后利用这组概率计算程序的适应度。●由于统计模型检验模块需要频繁调用,我们实现了一个本地化统计模型检验工具,并在此基础上开发了并发程序自动生成工具PSSMC。在互斥、轮询、哲学家就餐等经典问题上我们对PSSMC进行了系统化评估。实验表明相比现有方法,本工作所提出基于统计模型检验的并发程序自动生成方法在成功率,效率上均有显著优势。