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

摘要

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

说明书

技术领域

本发明主要涉及程序合成等领域，尤其涉及根据给定规约进行程序合成，生成满足规约的并发程序的问题。

背景技术

一直以来，如何提高编程的自动化，提升编程的效率都是人们关注的问题，程序合成是一种自动化编程方法，可以实现由给定的需求描述自动生成计算机程序的功能。

使用遗传算法进行程序合成是一种常用的方法。遗传算法是一种通过模拟自然进化过程搜索最优解的启发式方法，以集束搜索为基础，即每一轮迭代都保持一组候选者而不是单个候选者，并试图在每次生成新一轮候选者集合的时候提升新的候选者的质量，候选者被选中进入下一轮迭代的概率取决于它的适应度，适应度用来描述一个候选者距离正确结果的接近程度。

传统的方法是使用模型检验来计算候选者的适应度，然而模型检验是一种复杂的用来验证正确性的方法，因此它更适合用来确保代码的正确性而不是用来测试，另一方面，由于模型检验只能给出目标满足或不满足规约的结论，即只有0，1两种值，所以使用模型检验会导致适应度的可选值集合较小，不利于遗传算法搜索的过程。使用模型检验的另一个缺点是，模型检验的复杂度较高，需要将线性时序逻辑规约翻译成自动机，这一过程中可能发生空间爆炸。因此，传统采用模型检验和遗传算法的结合效率较低。

发明内容

本发明所要解决的问题：传统采用模型检验和遗传算法生成程序的效率低。

为解决上述问题，本发明采用的方案如下：

根据本发明的一种基于目标规约满足度评估的并发程序合成方法，该方法包含以下步骤：

S1：获取用户提供的程序模板和目标规约集合；所述目标规约为线性时序逻辑规约；

S2：根据所述程序模板随机生成初始的候选程序集合；

S3：计算所述候选程序集合中各个候选程序的适应度；

S4：选取所述候选程序集合中适应度超过阈值的候选程序，并对这些适应度超过阈值的候选程序用模型检验工具检验其是否满足所述目标规约集合中的各个目标规约；若模型检验工具检验到存在候选程序满足所述目标规约集合中的各个目标规约，则该候选程序作为最终输出并结束，否则进入步骤S5；

S5：根据所述各个候选程序的适应度迭代生成新的候选程序集合；

S6：重复步骤S3至S5直到迭代次数超过最大迭代轮次数；

所述步骤S3中计算所述候选程序的适应度包括如下步骤：

S31：将所述目标规约集合中各个目标规约转换成对应的限界规约；所述限界规约可以在有限长度的路径上进行检验；

S32：使用统计模型检验工具评估候选程序满足每个所述限界规约的概率；

S33：统计候选程序满足每个所述限界规约的概率得到所述候选程序的适应度。

进一步，根据本发明的基于目标规约满足度评估的并发程序合成方法，所述步骤S5包括如下步骤：

S51：根据所述候选程序的适应度，为每个候选程序分配一个概率值；

S52：根据各个候选程序的概率值，从候选程序集合中随机选择候选程序；

S53：对随机选择得到的候选程序进行拷贝或变异操作得到新的候选程序；

S54：重复步骤S51至S53直到候选程序集合中所有候选程序被新的候选程序所替换。

根据本发明的一种基于目标规约满足度评估的并发程序合成装置，该装置包含以下模块：

M1，用于：获取用户提供的程序模板和目标规约集合；所述目标规约为线性时序逻辑规约；

M2，用于：根据所述程序模板随机生成初始的候选程序集合；

M3，用于：计算所述候选程序集合中各个候选程序的适应度；

M4，用于：选取所述候选程序集合中适应度超过阈值的候选程序，并对这些适应度超过阈值的候选程序用模型检验工具检验其是否满足所述目标规约集合中的各个目标规约；若模型检验工具检验到存在候选程序满足所述目标规约集合中的各个目标规约，则该候选程序作为最终输出并结束，否则调用模块M5；

M5，用于：根据所述各个候选程序的适应度迭代生成新的候选程序集合；

M6，用于：重复调用模块M3至 M5直到迭代次数超过最大迭代轮次数；

所述模块M3中计算所述候选程序的适应度包括如下模块：

M31，用于：将所述目标规约集合中各个目标规约转换成对应的限界规约；所述限界规约可以在有限长度的路径上进行检验；

M32，用于：使用统计模型检验工具评估候选程序满足每个所述限界规约的概率；

M33，用于：统计候选程序满足每个所述限界规约的概率得到所述候选程序的适应度。

进一步，根据本发明的基于目标规约满足度评估的并发程序合成装置，所述模块M5包括如下模块：

M51，用于：根据所述候选程序的适应度，为每个候选程序分配一个概率值；

M52，用于：根据各个候选程序的概率值，从候选程序集合中随机选择候选程序；

M53，用于：对随机选择得到的候选程序进行拷贝或变异操作得到新的候选程序；

M54，用于：重复调用模块M51至M53直到候选程序集合中所有候选程序被新的候选程序所替换。

本发明的技术效果如下：本发明通过将用户提供的线性时序逻辑规约转换成限界线性时序逻辑规约，然后使用统计模型检验工具评估候选者满足规约的概率，计算每个候选者的适应度，然后再根据该适应度采用遗传算法得到新的候选程序，避免了模型检验工具直接逐个检验候选程序，从而提高程序合成的生成效率。

附图说明

图1是本发明的流程图。

图2是本发明实施例中所输入的程序模板示例。

图3是本发明实施例中根据图2中的程序模板所生成的满足目标规约的程序。

具体实施方式

下面结合附图对本发明做进一步详细说明。

如图1所示，本实施例的基于目标规约满足度评估的并发程序合成方法，按顺序依次包括：步骤S1，输入程序模板和目标规约；步骤S2，随机生成初始的候选程序集合；步骤S3，计算各个候选程序的适应度；步骤S4，选取候选程序集合中适应度超过阈值的候选程序，并对这些候选程序用模型检验工具检验正确性，也就是检验候选程序是否满足目标规约；然后步骤S6，判断当前的迭代轮次是否超过限值，假如迭代轮次超过限值，则失败结束，否则执行步骤S5，采用遗传算法重新生成候选程序集合；之后再回到步骤S3。

上述步骤S1中，输入程序模板和目标规约，相对于用户或者操作者而言，对于计算机所执行的则是“获取用户提供的程序模板和目标规约”。需要指出的是，用户所输入的目标规约是线性时序逻辑规约，也就是LTL规约。此外，还需要指出的是，用户所输入的目标规约通常并不是单个，而是多个规约，因此步骤S1实际上应该是“获取用户提供的程序模板和目标规约集合”，其中目标规约集合是目标规约的集合。也就是说，本实施例的基于目标规约满足度评估的并发程序合成方法其输入为“程序模板和目标规约集合”，输出为步骤S4中“满足目标规约集合中各个目标规约的候选程序”或者步骤S6中找不到满足目标规约集合中各个目标规约的的候选程序后“失败”结束。

下面以经典的互斥问题为例，对上述步骤做进一步详细说明。互斥问题是同步控制的经典问题，当有多个进程竞争同一个资源时，既要保证同一时刻最多只有一个进程获取资源，又要保证每一个竞争资源的进程在将来某一刻都会得到资源，不会发生饥饿。

如图2所示，图2是用户提供的程序模板。图2中的[Pre Protocol]和[PostProtocol]是需要通过上述步骤生成的并发程序。PreCSi，CSi和PostCSi分别表示临界区前段，临界区以及临界区后段。同时用户提供了以下三个目标规约所组成的目标规约集合：

Safety规约：G!(P1>

Liveness规约(P1)：G(P1 in PreCS1 -> F>

Liveness规约(P2)：G(P2 in PreCS2 -> F P1 in CS2)

其中，safety规约表示如下：P1 in CS1表示线程或进程P1在临界区CS；P2 in CS2表示线程或进程P2在临界区CS；G表示全局；！表示非，and表示与的关系；也就是整个safety规约表示线程或进程P1在临界区CS和线程或进程P2在临界区CS不能同时发生，这也就意味着，同一时刻最多有一个进程进入临界区。Liveness规约(P1)表示如下：P1 in PreCS1表示线程或进程P1在临界区前段PreCS1，-> F表示将来，P1 in CS1表示线程或进程P1在临界区CS；也就是整个Liveness规约(P1)表示为，线程或进程P1在临界区前段PreCS1时，将来一定会有线程或进程P1在临界区CSc，这就是意味着，如果一个进程请求进入临界区那么它终究会进入临界区。Liveness规约(P2)同Liveness规约(P1)，不再赘述。

得到上述程序模板和目标规约后，执行步骤S2，也就是，根据程序模板随机生成初始的候选程序集合，每个候选程序以语法树的形式保存。步骤S2的输入是前述步骤S1中的程序模板，输出为候选程序集合。初始的候选程序集合中的候选程序随机生成，基于语法树，具体包括以下两个步骤：

步骤S21，随机生成[Pre Protocol]和[Post Protocol]中的语法子树节点；

步骤S22，根据语法子树的节点类型对节点的子节点进行随机填充。

语法树是由节点组成的树状数据结构。语法树的节点类型，本实施例中，定义为五种分别为：“if”类型，“while”类型，“sequence”类型，“assignment”类型，以及“criticalsection”类型。“if”类型对应条件选择语句，必然包含一个子节点；“while”类型对应循环语句，必然包含一个子节点；“sequence”类型定义为包含两个子节点，两个子节点按顺序依次执行。“assignment”类型表示的是赋值语句。“critical section”类型表示的是临界区。语法子树的节点随机填充时，对于“if”类型和“while”类型的节点，随机填充其中的条件判断语句；对于“sequence”类型的节点，本身不需要填充内容，仅需要填充其具体的两个子节点即可；对于“assignment”类型的节点，随机生成赋值语句；对于“critical section”类型，是模板固定的内容，无需填充内容，如图1中的PreCSi，CSi和PostCSi即组成“criticalsection”类型的节点。上述“随机填充其中的条件判断语句”，“随机生成赋值语句”时，需要引用的变量为随机。具体来说，候选程序中的变量可以随机生成，也可以随机使用上下文中的变量比如图3中为根据图2程序模板随机生成的候选程序。其中数组变量A、整数变量me和other均为随机生成的变量。随机生成候选程序的语法子树时，所生成的语法子树的深度有要求。本实施例中，语法子树深度不能超过3。当然本领域技术人员理解，语法子树深度也可以设定为不能超过4或5等。语法子树深度要求可以预先设定，也可以通过步骤S1输入。初始的候选程序集合中所生成的候选程序数量可以预先设定，也可以通过前述步骤S1输入。

步骤S3，计算候选程序集合中各个候选程序的适应度。候选程序的适应度的计算根据候选程序逐个进行计算。本实施例中，计算单个候选程序的适应度的步骤如下：

步骤S31：将目标规约集合中各个目标规约转换成对应的限界规约；限界规约可以在有限长度的路径上进行检验；

步骤S32：使用统计模型检验工具评估候选程序满足每个限界规约的概率；

步骤S33：统计候选程序满足每个限界规约的概率得到候选程序的适应度。

上述步骤S31中，限界规约也就是Bounded LTL规约，具体图2的例子中，上述的Safety规约、Liveness规约(P1)、Liveness规约(P2)三个目标规约分别转换成三个限界规约：

Bounded Safety规约：G^<=n!(P1>

Bounded Liveness规约(P1)：G^<=n(P1><=n>

Bounded Liveness规约(P2)：G^<=n(P2><=n>

上述限界规约中，符号“<=n”表示n步之内。也就是，对于Bounded Safety规约，表示，执行n步之内不存在P1和P2同时进入临界区的情况；对于Bounded Liveness规约(P1)，表示，执行n步之内，只要线程或进行P1请求进入临界区，那么在之后的n步之内它一定能够进入临界区。上述限界规约中符号“<=n”中“n”的具体数值可以预先设定，也可以通过步骤S1输入。需要指出的是，转换方式并不是唯一的，也存在一些其他的合理的转换方式。

步骤S32中，首先，将候选程序转换成统计模型检验工具的程序输入模型，然后将程序输入模型和步骤S31中获得的限界规约组成限界规约集合输入至统计模型检验工具进行检验统计。统计模型检验工具检验统计后的输出为程序输入模型满足每个限界规约的概率，也就是，候选程序满足每个限界规约的概率。本实施例中，统计模型检验工具采用Plasma。具体可参照https://project.inria.fr/plasma-lab/，本说明书不再赘述。

步骤S33中，最为简单的方法是对候选程序满足每个限界规约的概率计算平均值，然后将平均值作为该候选程序的适应度。比如，某个候选程序对上述Bounded Safety规约、Bounded Liveness规约(P1)、 Bounded Liveness规约(P2)满足的概率分别为c1,c2,c3，则该候选程序的适应度F=(c1+c2+c3)/3。此外，也可以采用加权平均的方法。假设用户在步骤S1中输入目标规约时，同时还输入了各个目标规约的加权系数，比如图2例子中，Safety规约、Liveness规约(P1)、Liveness规约(P2)的加权系数分别为：α，β，γ，而Bounded Safety规约、Bounded Liveness规约(P1)、 Bounded Liveness规约(P2)满足的概率分别为c1,c2,c3；由此可以通过以下公式计算出候选程序的适应度：

，或者也可以通过以下公式计算出候选程序的适应度：

步骤S4，选取候选程序集合中的适应度超过阈值的候选程序，并对这些候选程序用模型检验工具检验候选程序是否满足目标规约。本实施例中，模型检验工具采用Spin。具体可参照www.spinroot.com，本说明书不再赘述。

步骤S5，采用遗传算法重新生成候选程序集合，也就是，根据各个候选程序的适应度迭代生成新的候选程序集合。具体到本实施例中，步骤S5包括以下步骤：

S51：根据候选程序的适应度，为每个候选程序分配一个概率值；

S52：根据各个候选程序的概率值，从候选程序集合中随机选择候选程序；

S53：对随机选择得到的候选程序进行拷贝或变异操作得到新的候选程序；

S54：重复步骤S51至S53直到候选程序集合中所有候选程序被新的候选程序所替换。

上述步骤S51中，假如各个候选程序的适应度分别为：S₁，S₂，S₃，...，S_n。其中S_i表示第i个候选程序的适应度，n为候选程序集合中的候选程序数。计SS为各个候选程序的适应度的总和，也就是。则各个候选程序所分配的概率值A_i=>i/SS。A_i表示第i个候选程序的概率值。

上述步骤S52本实施例采用如下方法：首先根据各个候选程序的概率值确定各个候选区间：R_i={RMIN_i，RMAX_i}；其中，R_i表示第i个候选程序的候选区间，RMIN_i表示第i个候选程序的候选区间的下限值，RMAX_i表示第i个候选程序的候选区间的上限值，RMIN_i和RMAX_i均为整型数。RMIN_i和RMAX_i满足如下条件：

RMIN₁=0，

RMAX_i=RMIN_i+A_i×RANMAX，

RMIN_i=RMAX_i-1+1；

其中，A_i表示第i个候选程序的概率值，RANMAX为预先设定的常数。RMIN_i=RMAX_i-1+1表示第i个候选程序的候选区间的下限值是第i-1个候选程序的候选区间的上限值加1。最后，从RMIN₁和RMAX_n之间随机生成随机数Rx，判断Rx所落入的候选区间，然后选择该候选区间所对应的候选程序作为随机选择的候选程序。

上述步骤S53，对随机选择得到的候选程序进行拷贝或变异操作得到新的候选程序中的变异操作在本实施例中具体方法如下：首先从四种变异操作类型中随机选择一种，然后根据随机选择的变异操作的类型，进行相应的变异操作。本实施例中四种变异操作的类型分别为：替换、添加父节点、以子节点替换自身、删除子树。“替换”变异操作类型之下，也就是在候选程序的语法树中，选择一个节点替换成随机生成的新节点。该随机的新节点与前述的步骤S2中的候选程序生成过程相同，同样可以是顺序执行的语句，也可以是条件选择语句，甚至还可以是循环语句。“添加父节点”变异操作类型之下，也就是在候选程序的语法树中，随机选择一个节点为其添加一个父节点，该父节点为随机生成的新节点。该随机的节点与前述的步骤S2中的候选程序生成过程相同，同样可以是顺序执行的语句，也可以是条件选择语句，甚至还可以是循环语句。“以子节点替换自身”变异操作类型之下，也就是在候选程序的语法树中，随机选择一个父节点，在该父节点所包含的子节点中随机选择一个将该父节点替换成该子节点。“删除子树”变异操作类型之下，也就是在候选程序的语法树中，随机选择一个父节点，并删除该父节点。候选程序的语法树由前述步骤S2生成并保存得到，同时，步骤S53进行变异操作后，其候选程序所对应的语法树保存。