一种基于强化学习的CCSL综合方法及系统

摘要

本发明提出了一种基于强化学习的CCSL综合方法，该方法将一个不完整的CCSL规约编码成为一个强化学习模型，并系统预期行为对模型训练进行指导，最终将模型转化为完整的CCSL约束。该方法包括：强化学习模型的生成方法，强化学习模型的训练方法，CCSL约束验证方法以及强化学习奖励评估方法。通过本发明方法自动化的生成了CCSL规约，为设计人员提供了较为有效的指导，极大地降低了系统设计的成本。本发明还提出了一种基于强化学习的CCSL综合系统。

说明书

技术领域

本发明属于计算机技术领域，专注于时间约束规约语言(CCSL)的综合，提出了一种基于强化学习的可根据不完整的CCSL约束以及一些系统的预期时间行为的例子而生成出完整的较为精确的CCSL规约的方法。

背景技术

随着MARTE(一个用于实时和嵌入式系统建模和分析的UML概要文件)的普及，时钟约束规范语言(CCSL)越来越受到工业界和学术界的关注。它提供了一套完整的预定义时钟约束，以捕获事件之间的经典因果关系和时间关系。时钟约束规范语言实现了复杂嵌入式系统的精确时序行为建模。通过模拟事件的逻辑时钟，CCSL提出了一套全面的语法构造来捕获的因果关系和事件发生的时间之间的关系。

嵌入式系统设计通常采用自上而下的设计流程，要求需求工程师从文本设计描述中手动导出CCSL规范。这可能会导致严重的问题，因为大多数需求工程师对逻辑时间/时钟的形式定义及其关系了解有限。更糟糕的是，由于实时嵌入式系统的复杂性急剧上升，需求工程师很难在设计阶段找出系统的所有时序轨迹。因此，大多数CCSL规范的构造都是基于对系统时序轨迹的有限观察，这使得CCSL规范生成过程更加耗时和容易出错。

发明内容

本发明的目的是针对现有技术的不足而设计的一种基于强化学习的时间约束规约语言综合方法。该方法将一个不完整的CCSL规约编码成为一个强化学习模型，并系统预期行为对模型训练进行指导，最终将模型转化为完整的CCSL约束。该方法包括：强化学习模型的生成方法，强化学习模型的训练方法，CCSL约束验证方法以及强化学习奖励评估方法。通过本方法自动化的生成了CCSL规约，为设计人员提供了较为有效的指导，极大地降低了系统设计的成本。

实现本发明目的的具体技术方案是：

本发明包括两个主要模块：模型生成器模块和强化学习模块。其中模型生成器模块为步骤1的实现，强化学习模块为步骤2和步骤3的实现。

步骤1：强化学习模型生成及剪枝

模型生成器模块是根据不完整的CCSL约束生成强化学习模型，再根据系统预期行为对初始的强化学习模型进行剪枝生成初始的强化学习模型。模型生成器分为模型生成和模型剪枝两个步骤。

本方法将不完整的CCSL约束进行分析，根据不完整CCSL约束的数量和种类以及每一种不完整的CCSL约束对应的可以补全其的选项生成强化学习模型。之后，根据系统预期行为对模型进行剪枝，剪枝后为初始强化学习模型。

步骤2：强化学习模型训练

强化学习模块是本发明的核心模块，对于步骤1生成的初始的强化学习模型进行训练。一次训练过程为选择一组可选项填补不完整的CCSL约束，会按照不完整的CCSL约束种类的顺序进行训练，并验证这些选项是否满足给定的系统预期行为。若选项满足给定的系统预期行为则评估这一组选项的奖励值，并更新模型中这些选项对应的参数。若选项不满足给定的系统预期行为，则将模型中这些选项对应的参数减去一个惩罚项。模型训练会进行多次，上述选择可选项填补约束并更新模型参数的过程会进行多次，具体的次数由使用者对训练模型的时间限制所决定，即训练的次数是用户指定的。

步骤3：生成完整的CCSL规约

将步骤2训练完成的模型转化为完整的CCSL约束进行输出。对于每一个不完整的CCSL约束，选取模型中表示其选项的值最大的参数所对应的选项填补该约束。

在步骤1的模型生成阶段，生成器分析输入的不完整的CCSL约束，根据不完整的CCSL约束的不完整部分的类型对其进行分类，即分为expression操作符、expression操作数、relation操作符和relation操作数四类。对于expression操作符其可选项为所有的expression操作符，expression操作数的可选项为所有时钟以及所有expression时钟，relation操作符的可选项为所有relation操作符，而relation操作数的可选项为所有时钟以及expression时钟。根据CCSL约束的数量生成和种类生成初始的强化学习模型，该模型由一个矩阵组成，即将不完整的CCSL约束编码成为一个矩阵。每一列矩阵表示对应的不完整的CCSL约束的可选项，因此矩阵的列数为不完整的CCSL约束的数量，而每一列矩阵的元素个数为对应的CCSL约束的可选项的个数，矩阵中的第i列第j行即表示第i个不完整的CCSL约束的第j个可选项，矩阵的参数的值表示该可选项的奖励期望值，若参数值为-1表示该选项不可选，值越大表示该选项更应该被选则填补对应的约束。再将所有的列矩阵进行拼接合并，即该矩阵表示所有不完整约束的可行解。

在步骤1的模型剪枝阶段，首先模型生成器将预期的行为进行分析，会根据CCSL约束的类型建立约束的操作符和操作数时钟滴答次数的关系列表，这些关系是通过逻辑推导得出的。接着，对于每一个不完整的约束，从系统预期的时钟中抽取其操作数或者可选操作数的滴答序列，计算其序列的长度，并与关系列表进行比对，判断每一个元素对应可选项填充后的CCSL约束的时钟序列的长度是否满足预期行为中对应时钟的滴答序列长度，根据CCSL约束对于时钟滴答次数的关系，若可选项不满足关系则表示该选项一定不满足系统预期行为，则将其在矩阵中对应元素的值置为-1，即将该可选项置为不可选，在后续强化学习过程中不会选择该选项。经过剪枝将减少模型中可选项的数量，加速了后续强化学习的训练过程。最终模型生成器将经过剪枝的模型作为强化学习模块的初始模型进行输出。

在步骤2中，使用预期系统行为验证强化学习训练过程中选择选项的正确性，强化学习的训练过程需要若干次训练，每一次训练过程为一次求解完整CCSL约束的搜索，即在每一列矩阵中选择一个值大于-1的元素，即表示选择元素对应的可选项来填补不完整的CCSL约束。每搜索一个元素则需要判断该选项是否满足预期的系统行为，判断过程为验证预期行为的时钟滴答序列是否符合使用该选项填补的CCSL约束，若满足则进行下一个元素的搜索，若不满足则结束该次搜索，并判断当前不完整的CCSL约束是否与其他不完整的约束存在依赖关系，若不存在则说明当前搜索的选项在任何时候都是与预期行为相违背的，则将模型中对应位置的元素的值置为-1，若满足则返回1，若无法判断则返回0。若当前选项不满足预期行为，则判断当前不完整的CCSL约束是否与其他不完整的约束存在依赖。若存在依赖关系则将该次搜索所有选择的选项在模型中对应的元素减去一个惩罚项。若不存在依赖，则将该选项在模型中对应位置的元素值置为-1。若当前选项无法判断则如11行所示将当前选项存入一个队列。

使用CCSL约束之间的关系制定强化学习奖励评估方法，在一次搜索结束后若所有的选项都满足预期行为，则调用奖励评估模块，根据CCSL约束的特性对每一次训练的一组选项进行打分，分数即为强化学习中的奖励值，最后从最后一个选项开始对奖励进行累加并对选项在模型中对应位置的元素值进行更新，更新的值为当前选项即其之后选项奖励的累加值乘以一个学习率加上原值乘以1减去学心率。

在步骤3中，经过多次训练之后，将模型的每一列值最大的元素对应的选项作为综合结果填补不完整的CCSL约束，并将补全的完整的CCSL约束作为结果输出。

基于以上方法，本发明还提出了一种基于强化学习的时间约束规约语言综合系统，包括：模型生成器模块和强化学习模块，所述模型生成器模块和强化学习模块实现上述方法。

本发明将CCSL规约的综合问题转化为强化学习问题，将不完整的CCSL约束编码成为强化学习模型，通过系统预期行为对初始模型进行剪枝并指导强化学习模型的训练，最终将训练完成的模型转化为完整的CCSL约束，有益效果在于：本方法将强化学习的优点与逻辑推理中的演绎技术相结合，实现CCSL规范的高效协同合成。具体地说，本方法利用强化学习方法来列举所有可能的解决方案来填补不完整规范的漏洞，并使用演绎技术来判断每一次试验的质量。本发明提出的演绎机制不仅有助于修剪枚举空间，而且有助于引导枚举过程快速获得最优解。通过本方法自动化的生成了CCSL规约，为设计人员提供了较为有效的指导，极大地降低了系统设计的成本。

附图说明

图1是本发明总结构图。

图2是本发明模型生成器模块结构图。

图3是本发明强化学习模块结构图。

图4是本发明流程图。

具体实施方式

结合以下具体实施例和附图，对发明作进一步的详细说明。实施本发明的过程、条件、实验方法等，除以下专门提及的内容之外，均为本领域的普遍知识和公知常识，本发明没有特别限制内容。

如图1所示，根据两个步骤将发明设计为两个主要模块：模型生成器和强化学习。其中模型生成器模块为步骤1的实现，强化学习模块即为步骤2和步骤3的实现。

模型生成器模块是根据不完整的CCSL约束生成强化学习模型，再根据系统预期行为对强化学习模型进行剪枝，剪枝后为初始强化学习模型。如图2所示，模型生成器分为模型生成和模型剪枝两个步骤。

在模型生成阶段，生成器分析输入的不完整的CCSL约束，根据不完整的CCSL约束的不完整部分的类型对其进行分类，即分为expression操作符、expression操作数、relation操作符和relation操作数四类。对于expression操作符其可选项为所有的expression操作符，expression操作数的可选项为所有时钟以及所有expression时钟，relation操作符的可选项为所有relation操作符，而relation操作数的可选项为所有时钟以及expression时钟。生成器根据每一个不完整的CCSL约束生成一列矩阵，矩阵的元素个数为该约束的可选项，再将所有的列矩阵进行拼接合并，即该矩阵表示所有不完整约束的可行解。

在模型剪枝阶段，模型生成器将预期的行为进行分析，抽取所有时钟的滴答序列。再对生成的模型进行遍历，判断每一个元素对应可选项填充后的CCSL约束的时钟序列的长度是否满足预期行为中对应时钟的滴答序列长度，若不满足则将模型中对应元素的值置为-1，即将该可选项置为不可选。最终模型生成器将经过剪枝的模型作为强化学习模块的初始模型进行输出。

强化学习模块是本发明的核心模块，该模块对模型生成器生成的模型进行训练，并将训练完成的模型转化为完整的CCSL约束进行输出。

如图3所示，强化学习的训练过程需要进行若干次探索，每一次探索会选择一组可选项填补不完整的CCSL约束，而在探索的每一步中需要调用CCSL验证器对强化学习的选择进行验证，CCSL验证器将从系统预期行为中抽取与验证约束相关的时钟的滴答序列，并验证滴答序列是否满足CCSL约束，若满足则表示该次选择是正确的，若不满足则表示该次选择是错误的。在一次探索成功后，在强化学习过程中需要调用奖励评估模块，该模块用于评估强化学习探索中每一个选择的奖励值，而这些奖励值将用于更新模型参数。最终根据模型参数生成完整的CCSL约束。

procedure CCSLSyhthesize(Spec，Traces，π

Input Spec：不完整的CCSL约束

Input Traces：系统预期行为

Inputπ

Input round：训练次数

Inputα：学习率

Output Spec：完整的CCSL约束

1π

2 for i in 1 to round

3 S←Spec

4 T←Traces

5 chooseList←{}

6 unAcList←{}

7 forH∈Spec.holes

8 choose a～π

9 chooseList.add((H，a))

10 S←Fill(S，(H，a))

11 (r，π

12 ifr＝-1

13 break

14 Ifr＝1and UnActList＝{}

15 π

16 return ResultEvaluator(Spec，π

上述算法描述了强化学习训练的过程，round表示训练次数，由用户指定，每一次训练即为一次探索过程。在每一次探索过程中会按照不完整的CCSL约束种类的顺序进行探索，如9-10行所示。对于每一个不完整的约束选择一个可选项填补该约束，如11行所示CCSLChecker将验证所选的选项是否满足预期行为，CCSLChecker即为CCSL验证器。如14-15行所示，在一次成功的探索结束后PolicyUpdate将会更新模型参数，该函数即实现了奖励评估函数，即计算每一个选项的奖励值并更新模型。在训练结束后ResultEvaluator函数将根据模型参数生成完整的CCSL约束并输出。

procedure CCSLChecker(S，chooseList，π

1←chooseList.getLast()

2r←Deduce((H，a)，T)

3 if r＝-1

4 if checkDependence((H，a)，S)

5 for(H′，a′)∈chooseList

6 a←chooseList[i]

7 π

8 else

9 π

10 else if r＝0

11 UnActList.append((H，at))

12 else

13(r，unActList，T)←UpdateUnAct(unActList，T，H，a)

14 return(r，π

上述算法描述了CCSL验证器的验证过程，如第2行所示，Deduce函数判断当前选项是否满足预期行为，若不满足则返回-1，若满足则返回1，若无法判断则返回0。若当前选项不满足预期行为checkDependence函数判断当前不完整的CCSL约束是否与其他不完整的约束存在依赖。若存在依赖则如5-7行所示，将该次搜索所有选择的选项在模型中对应的元素减去一个惩罚项。若不存在依赖，则如9行所示，将该选项在模型中对应位置的元素值置为-1。若当前选项无法判断则如11行所示将当前选项存入一个队列。若当前选项满足约束则如13行所示更新unActList队列，该队列保存了该次探索之前步无法判断的选项，若当前选项导致之前步无法判断的选项不满足预期行为则返回-1并将该次搜索所有选择的选项在模型中对应的元素减去一个惩罚项，若该次探索导致之前步无法判断的选项满足预期行为则将满足的选项从队列中删去。最终返回验证结果。

procedure PolicyUpdate(chooseList，S，π

1 sumTeward←0

2 for i in len(chooseList)to 1

3(H，a)←chooseList[i]

4 reward←rewardEvaluator((H，a)，S)

5 sumReward←sumReward+reward

6 π

7 returnπ

上述算法描述了强化学习奖励评估和模型更新的过程，在一次成功的探索之后会调用该算法。首先如2行所示，该算法从最后一个选项开始计算奖励值，第4行为计算奖励值的函数，该函数根据时钟滴答的次数与其操作符的关系进行奖励值评估，同时对于重复出现的约束会降低奖励值。第6行为更新模型参数的过程，对每个选项在模型中对应位置的元素值进行更新，更新的值为当前选项即其之后选项奖励的累加值乘以一个学习率加上原值乘以1减去学心率。

本发明的保护内容不局限于以上实施例。在不背离发明构思的精神和范围下，本领域技术人员能够想到的变化和优点都被包括在本发明中，并且以所附的权利要求书为保护范围。