一种基于目标规约满足度评估的并发程序合成方法和装置

摘要

本发明公开了一种基于目标规约满足度评估的符合规约并发程序合成方法和装置。该方法或装置通过将用户提供的线性时序逻辑规约转换成限界线性时序逻辑规约，然后使用统计模型检验工具评估候选者满足规约的概率，计算每个候选者的适应度，然后再根据该适应度采用遗传算法得到新的候选程序，避免了模型检验工具直接逐个检验候选程序，从而提高程序合成的生成效率。