作者 李勇坚 我国科学院软件研讨所(北京100190)
李勇坚，博士，研讨生导师，人工智能敞开立异渠道*联合学者，首要研讨方向：核算机科学理论和软件理论。
*注：人工智能敞开立异渠道：是由贵阳市政府与我国人工智能工业立异联盟、英特尔三方一起打造的敞开渠道。渠道结合端到端的全面技能，打造软硬件敞开立异渠道，加快工业运用立异，经过打造人工智能敞开渠道、创建人工智能立异加快器等，树立完善的技能生态、在人工智能笔直范畴运用、工业对接和市场推广等发挥各方优势和资源特征，加快我国人工智能的开展和运用立异。
0导言
带参体系存在于许多运用范畴中，比方缓存共同协议等。因为它的研讨价值，验证这样的体系也就招引来了方式化验证、模型检测和定理证明等社区的重视。要想验证带参体系的正确性，就必须验证恣意实例巨细的体系中的正确性，而这被证明是一个无法断定的问题。
虽然这样的难度，可是许多办法依然被提出来企图处理这个问题。CMP办法是其间最成功的办法之一。它用模型检测的办法来验证Intel、flash等大型的协议。经过保存m个节点，并用一个笼统的节点NOther来代替其他一切剩下节点的行为。经过这样的笼统，一个原始的协议就被笼统成了一个由m+1个节点组成的笼统适意。然后经过剖析模型检测器供给的反例，循环结构一系列引理来约束笼统节点NOther的行为，使得协议能够收敛，且不会违背原有性质。假如终究原始性质和引理都能在笼统协议中被查验经过，那么就能推导出原始协议在恣意巨细的实例下也都能建立。可是，CMP办法是在模型检测机给出反例之后，采纳的是被迫补救措施。这样的被迫办法因为依赖于人工了解和辅导，而无法主动化。而且“寻觅反例-卫式加强”这样的循环，所需求的次数不知道，这也就使得可达集是否能收敛、笼统协议能否满意安全性质成为不知道。
CMP存在的缺陷启示咱们去更深化地考虑：是否能够经过主动地探究满意上述条件的可达集边际，以使可达集收敛，并满意安全性质?假如能够主动的约束可达集能抵达的规模，则能够更主动地查找辅佐不变式，然后更精确地加强笼统体系。
因而，在这篇论文中，咱们提出了L-CMP，一种主动的学习结构，经过较小实例可达集学习/发掘辅佐不变式，而且主动的用这些辅佐不变式对笼统协议进行约束，终究，笼统协议的可达集能够被收敛在合理规模，安全性质也就能够确保。
1相关规矩学习
在本文中，咱们奇妙地将相关规矩学习(Association rule
learning)与卫式加强做结合，成功达到了寻觅辅佐不变式及主动卫式加强的意图。
相关规矩学习是Agrawal等人提出的依据规矩的机器学习办法。它的意图是运用一些风趣性的丈量来辨认数据库中发现的强规矩。依据强规矩的概念，Rakesh
Agrawal等人引入了相关规矩以发现由超市的POS体系记载的大批买卖数据中产品之间的规律性。许多有用的相关规矩算法，如Apriori,
Eclat和FP-growth。在本文中，咱们运用Apriori作为相关规矩的学习算法进行学习。
给定由一组业务组成的数据集D，记为D={t1，t2，…，tm}。设I={i1，i2，…，in}是一组包含许多项意图项集。每个买卖t包含一个项目子集。一个相关规矩的方式是X→Y，其间X，Y∈I.X被称为前件，Y是规矩的后件。此外，还有一些约束条件来衡量规矩的重要性。在本文中，咱们要点重视两个规范：支撑度和置信度。
支撑度：它丈量在同一业务中产生的项目集的频率。K频频项目集是频频调会集包含K个项意图项目集。能够将支撑核算为在同一业务中呈现多个项意图概率。支撑价值的最低阈值被称为最小支撑度。
2结构
L-CMP能够分为以下两个阶段，如图1。
2.1学习不变式
这个阶段旨在经过学习算法寻觅出辅佐不变量。在这个阶段，咱们首要搜集协议的一个小实例m(通常是m=2)的可达状况调集(进程1)。然后，咱们直接从协议描绘中提取原子谓词，并将它们看作项目集以辅导数据集的转化(进程2)。这一步关于第二阶段是必要的，第四节解说了背面的原因。接下来，经过相关规矩学习，能够学习一组相关规矩(进程3)。值得注意的是，咱们运用的数据集由一个小型的协议实例进行转化，因而因为实例的巨细有限，无法表明整个参数化协议的行为。此外，咱们现已运用了对称削减技能来使一些大协议中的可达状况最小化，导致数据集的不完整性。因而，需求额定的进程(进程4)。咱们将这些相关规矩视为候选不变量并将它们输入模型查看器Murphi。假如他们持有协议的一些小实例(大于m)，则它们被视为辅佐不变量。假如某些失利，失利的将从候选不变会集消除。最终，左面的候选不变量作为辅佐不变量。
2.2参数笼统和卫式加强
这个阶段是笼统协议，并运用辅佐不变量加强笼统规矩的卫式部分。首要，辅佐不变量以及协议中的转化规矩将经过分配详细索引来实例化(进程5)。这一步为加强进程供给了便当。接下来，经过以相关规矩的方式增加辅佐不变量的成果，递归地加强规矩看护(进程6)。然后，经过删去关于不行调查节点的局部变量来笼统加强的规矩(进程7)。值得注意的是，咱们提出了一个映射操作，它树立了护卫与举动之间的联系，以便最大极限地加强规矩。之后，加强和笼统的规矩将附加到原始协议并送入模型查看器(进程8)。请注意，用于加强守则规矩的辅佐不变量也需求验证将它们翻译成Murphi代码后。主动翻译的进程较为简略，所以咱们在本文中就不赘述。假如笼统协议实例经过巨细为$m+1$的模型检测器，则完毕结构(进程10)，不然就需求调整学习算法中的参数，而且结构开端下一轮学习(进程9)。
3试验成果
咱们将L-CMP运用于5个经典的带参协议上进行试验，试验成果如表1。其间，列名分别为协议称号、频频集个数、最小支撑度、相关规矩个数、辅佐不变式个数、所用不变式个数、总运转时长、所耗内存峰值、笼统协议能否经过验证。能够看到，咱们的L-CMP能够很好地对包含Flash协议在内的各个协议进行很好的验证。
4定论
在本文中，咱们提出了一个主动结构L-CMP，它能够在一个一致的结构中主动学习辅佐不变量，并进行笼统参数和卫式加强。咱们作业的立异性会集体现在于以下两个方面：1.咱们不是经过剖析计数器例子来手动拟定不同的变体，而是经过相关规矩学习从协议的可达状况调会集导出不变量;2.在反例生成之后，咱们不再强化协议，而是依据主动学习的不变量直接进行卫式加强。在未来的作业中，咱们期望扩展L-CMP的验证才能，使其能证明一般的安全性质和活性性质，而不只局限于不变式。
参考文献：
[1]Lv Y,Lin H,Pan H.Computing invariants for parameter abstraction.In:
Proceedings of the 5th IEEE/ACM International Conference on Formal Methods and Models for
Codesign, IEEE Computer Society (2007):29–38
[2]Apt K R, Kozen D C.Limits for automatic verification of
finite-stateconcurrent systems. Information Processing Letters 22(6) (1986) :307–309
[3]Chou C T,Mannava P K,Park S.A simple method for parameterized
verification of cache coherence protocols. In: FMCAD. Volume 4., Springer (2004):382–398
[4]Agrawal R,Imielin ́ski,T.,Swami A.Mining association rules between sets
of items in large databases. In: Acm sigmod record. Volume 22.,ACM (1993):207–216
本文来源于我国科技期刊《电子产品世界》2019年第1期第82页，欢迎您写论文时引证，并注明出处
