CSP组合验证技术：假设保证规则、自动学习假设与属性检查

理论计算机科学电子笔记250（2009）135-151www.elsevier.com/locate/entcs成分CSP跟踪细化检查丹尼尔·沃尼施2帕德博恩大学信息学院33098帕德博恩，德国摘要由于引入了自动学习假设的技术，使用假设保证推理的组合验证最近兴起。在本文中，我们将这种技术转移到CSP作为建模和属性指定语言的环境中，并提出了一种复合痕迹细化检查的方法。 该方法已实现使用CSP模型检查FDR在学习过程中，当老师。该实现表明，组合方法可以大大优于FDR的性能，也可以低于关键词：组合验证，假设保证规则，CSP，学习，精化1介绍即使经过25年的模型检查[9]，状态空间的复杂性仍然是自动验证正式指定模型的主要问题。 复杂系统中状态爆炸的一个因素是并行组件，因为-原则上-状态空间的大小随组件的数量呈指数增长。专门处理这个问题的技术已经并仍在开发中。其中包括例如偏序约简[19]，对称约简[6]，并行系统的特定抽象技术[16]或组合验证，我们将在这里感兴趣的技术组合验证[5]采用分而治之的方法来检查正确性：而不是对整个系统进行验证，只检查系统组件，并将验证结果合并。组合验证的一种具体方法是假设保证（AG）推理[12]，[15]。 检查系统S = S1||S2为持有物业道具进行了两次1电子邮件：wehrheim@mail.upb.de2电子邮件：dwonisch@mail.upb.de1571-0661 © 2009 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.08.022136H. Wehrheim，D.Wonisch/Electronic Notes in Theoretical Computer Science 250（2009）135步骤：首先，我们证明S2在关于其环境的假设A下保证Prop，然后证明S1 关于证明规则：真PRAYAPRAYS2型螺旋桨产品介绍||S2双柱支撑架在很长一段时间里，这条规则似乎是不切实际的，因为它涉及到对假设A的人工识别。最近，[8]提出了一种在验证安全属性时自动生成假设的算法。该方法使用Angluin [2]的算法（以及后续的改进[17]）来学习常规语言（有限状态自动机）。基本的想法是有一个老师来回答像“这是语言中的一个词吗？” （成员查询）和“这是正确的自动机吗？” （等价查询）。 教师的回答有助于不断提高学习者的初步猜测。在组合验证的情况下，常规语言是假设，学习者是生成假设的算法，教师是模型检查器。在本文中，我们将这种方法转移到CSP设置。CSP（Communicating SequentialProcesses，通信顺序进程[11]）是一个进程代数，用于描述并行通信进程。 系统的CSP模型的属性可以使用 三个细化排序轨迹之一，稳定失效或失效发散细化。在这里，我们将对过程的安全属性感兴趣，因此使用跟踪细化。为了在CSP设置中使用上面概述的组合验证和假设学习，我们需要将（a）上面的证明规则和（b）学习的成员资格和等价查询转移到CSP。 此外，我们需要一个老师，在这种情况下，这很简单，因为CSP带有模型检查器FDR [7]，用于检查所有三个细化排序，并且-正如我们稍后将看到的-成员和等价查询都可以重新表述为跟踪细化检查。除了上面给出的AG-规则之外，我们还将[10]的并行对称证明规则转移到CSP，CSP使用关于语言交集空性的第三个查询因此，转移的方法已在Java中实现，使用Tcl接口到FDR。许多优化（例如，递归应用学习，缓存先前计算的结果，基本和并行证明规则的组合）进一步加快了验证。 我们进行了大量的实验，以及从文献中的人造的例子。与FDR在完整CSP规范上的性能比较表明， 可以大大优于非组合验证，但也可以使事情变得更糟。性能取决于在学习过程中生成的假设的大小，这反过来又取决于感兴趣的属性。对于本文中的示例说明，我们都给出了一个性质，对于该性质，合成方法被证明是优秀的，并且对于该性质，FDR的性能要好得多。我们的实现已经成功地应用于[13]，其中H. Wehrheim，D.Wonisch/Electronic Notes in Theoretical Computer Science 250（2009）135137→⟨⟩提出了一种组合验证的分解技术，并将其应用于两阶段提交协议的验证2背景由于我们的组合验证基于规范语言CSP，因此需要一些关于CSP、标记转换系统（LTS）和跟踪细化的背景信息。我们通过提供以下示例来简要解释这些基本概念。2.1调度器该示例基于在FDR的sample文件夹中找到的Simon Gay的CSP规范。在[18]和[14]中也描述了类似版本的示例首先，想象一组要由调度程序处理的作业。 让n是这些工作的数量。可以开始或完成作业。因此，当查看单个作业时，可能会发生事件start和finish。 以便识别 对于带有start和finish事件的作业i，我们分别写start.i和finish.i（0≤in）。作业i完成后，可以使用start.i重新启动它。调度程序的目的是维护作业执行的某些约束。在这个简单的例子中，我们只对两个约束感兴趣：(i) 在作业i的两个start调用之间，必须恰好发生一个finish.i事件。因此，只有在作业之前完成时，才可以重新启动作业。此外，finish.i事件只能在start.i事件的前一次执行之后发生。(ii) 这些工作应该以“循环往复”的方式开始。这意味着首先启动作业0，然后是作业1，然后是作业2，依此类推，直到所有n个作业都已启动。在最后一个作业已经启动之后，作业0可以再次启动在对调度器应该如何工作有了直观的了解之后，现在的任务是使用CSP语言来表达这个系统。在实际构建一个满足约束的CSP过程之前，我们首先将约束本身描述为CSP过程。这将在以后证明是有用的约束（i）对于CSP中的单个作业i建模非常简单。对于单个作业i，该约束允许事件start.i和finish.i仅轮流发生这样的一系列事件称为迹线。 因此，例如，跟踪start.i、finish.i、start.i应该被允许用于描述约束（i）的CSP进程JobProp i。 由于作业i可以无限频繁地执行，所以JobProp i的所有迹的集合，表示为迹（JobProp i），应该包含无限多的元素。为了在CSP中描述这样一个过程，我们只需要前缀运算符，用e P表示某个事件e和一个过程P。这个操作符用来描述一个进程，在这个进程中，事件e首先被执行，然后它的行为与P完全一样。使用该运算符，单个作业i的约束（i）可以描述如下：JobPropi=start.i→finish.i →JobPropi138H. Wehrheim，D.Wonisch/Electronic Notes in Theoretical Computer Science 250（2009）135i=0||现在我们要描述一个CSP进程SchedProp，它为所有作业表达约束（i）。基本上应该允许JobPropi（0≤i n）的迹线的任何交织。例如，跟踪开始。0，开始。1，完成。0，完成。约束（i）允许在跟踪开始时执行1次跟踪。0，完成。0，开始。1，完成。1个月。这可以在CSP中使用交织运算符来表示|||：计划方案= |||n−1作业属性i类似地，约束（ii）可以再次使用前缀运算符建模为CSP过程：CycleProp0=开始。0 →CycleProp1CycleProp1=开始。1 →循环方案2.CycleProp n−2=开始。（n − 2）→CycleProp n−1CycleProp n−1= start。（n−1）→CycleProp0为了使CSP的迹语义的思想更清晰，我们想把这些CSP过程转换成相应的自动机。事实上，CSP具有操作语义，允许我们将任何CSP进程P转换为标记转换系统（LTS）。如果LTS是有限状态，我们可以把它看作一个自动机（通过使所有的状态都是最终的），因此可以说LTS的语言。当查看CSP进程P的跟踪语义时，我们 因此得 到P（ traces（ P） ）等 于LTS的语 言。 图1显示 了n=2的SchedProp的LTS，图2显示了n=5的CycleProp0Fig. 1. n= 2时的计划表ROP图二. 循环P rop0，n= 5接下来，我们设计了一个调度器遵守这两个约束。为此，我们首先引入一个新的操作符。并行合成算子用来表示两个CSP进程P1、P2并发执行，记为P1X1X2P2。虽然P1和P2是并发执行的，但它们可能必须在某些事件上同步.这就是为什么需要字母X1和X2字母表是一组事件，H. Wehrheim，D.Wonisch/Electronic Notes in Theoretical Computer Science 250（2009）135139∈∩∩||\⊆±--在这种情况下，X1基本上描述了在过程P1中可能发生的事件集。 这同样适用于X2和P2。 如果一个事件e在字母表X1中，在X2中，并且它可以由P1执行，则P1也可以执行并行组合P1X1X2P2中的事件e，反之亦然。但是如果P1只能执行字母表X1X2中的事件EJ，则在并行组合中P1必须等待，直到P2也执行EJ。因此，事件eJX1X2只能联合执行。利用这个概念，可以设计调度器。首先，我们将调度器分成所谓的单元。 调度器的单元可以是活动的或不活动的。 最初，除一个细胞外，所有细胞都应处于非活动状态。非活动单元i只是等待某个事件c.i发生，然后切换到活动状态。一个活动单元i将使用start.i执行其对应的作业i，并通过执行c.inc（i）激活下一个单元，其中inc的定义为inc（i）：=i+ 1 modn。一段时间后，finish.i可能会出现，因为作业已完成执行。当作业完成时，单元i再次等待事件c.i发生，然后再次启动单元。如果事件c.i发生在finish.i之前，则单元格应等待finish.i，然后立即执行start.i这两种可能性可以用CSP中的选择算子来表示，对于某些CSP过程P和Q，用PQQ表示。综上所述，我们得到以下CSP流程：ACelli=start.i→c.inc（i）→（finish.i→c.i →ACelliQc.i→finish.i →ACelli）0 ≤i n IACelli =c.i →ACelli0≤i n小区0=ACell0Cellj=IACellj0jn这n个信元仅在事件c.i上同步地同时执行：||C1∪... n−1（. . .（Celln−2Cn−2||Cn−1Celln−1)·· ·),其中C i定义为C i=start.i，finish.i，c.i，c.inc（i）。由于事件c.i只是我们实现调度程序所使用的人工事件，我们希望将它们隐藏在进程的跟踪中。CSP运算符为此目的而使用隐藏运算符，对于某个CSP进程P和字母表X，用P X表示。使用这个操作符，我们可以隐藏人工事件以获得最终的调度程序：Sched= SchedJ\{c. 0，c. 1、......、C. （n −1）}为了表示这个CSP过程保证了性质（i）和（ii），我们可以在 C S P 中 使用迹线细化。一个过程P定义了Q，记为Q T P，i = traces（P）traces（Q）。约束（i）、（ii）应仅允许分别由CSP过程SchedProp和CycleProp0定义的跟踪。因此，所需140H. Wehrheim，D.Wonisch/Electronic Notes in Theoretical Computer Science 250（2009）135||||±\\Sched的属性可以简单地写为：计划参数±T计划CycleProp0± T计划完成。0，完成。1，. . . ，完成。（n − 1）}为了验证这些改进，我们可以使用CSP模型检查器FDR。不幸的是，单元的并行组合在相应的LTS中产生指数（更精确地说是Θ（n2n），[18]）数量的状态。因此，FDR需要大量的时间来验证细化，甚至会因为n很大而耗尽内存。这就是为什么我们感兴趣的是一种方法，通过集中于细胞的性质而不是整个系统来从组成上检查我们的例子的改进。3成分验证为了将假设保证方法应用于跟踪细化检查，特别是用于假设生成的学习算法，我们首先需要根据CSP重新表述介绍和学习的证明规则。我们然后将这样专门化的技术应用于我们的调度器示例3.1一般方法首先，回顾一下引言中的基本证明规则我们现在想用CSP来表示证明规则最明显的是，组件Prop、S1、S2和A需要是CSP进程.此外，我们在这里只考虑系统S，它可以表示为S=S1<$1<$2S2，对于某些字母表<$1和<$2。 如第2节所示，我们可以表示系统S使用迹精化来填充属性P因此，我们可以将其表示为P TS（Events P），其中Events P是与P对应的字母表，并且字母表Events包含整个CSP规范的所有可能事件。最后，为了表示系统S2在假设A下运行，我们可以使用并行组合（即，A w2S2，其中w和2分别是A和S2的字母表总结一下，我们得到以下证明规则：A±TS1\（事件\nw）Prop± T（A ±W ||2S2）\（事件\Prop ± T（S1±1||2S2）\（事件\虽然字母表P、1和2由相应的过程定义，但字母表w可以或多或少地自由选择。由于我们想得到最简单的假设A，所以我们使用最小的字母表来表示A。假设A基本上描述了S1的行为，这对S2保证Prop很重要。因此，A的字母表应该包括在S1的字母表中的所有事件，以及在S2的字母表中或在Prop的字母表中的所有事件。H. Wehrheim，D.Wonisch/Electronic Notes in Theoretical Computer Science 250（2009）135141∪∩||\\因此，我们在本文中设置了EPWW：w=（使用这个字母表，上面给出的证明规则是健全和完整的（[4]）。给定CSP过程S1、S2和Prop，如果可能的话，现在的任务是自动找到满足证明规则条件的假设A为此，我们使用了由Angluin开发的学习算法（[2]，由[17]改进），并在[4]中提出了假设生成为此，我们将任务分为两个部分：学习者和教师。使用教师，学习者可以连续地构建可能足以用于证明规则的假设A事实上，学习者连续尝试学习所谓的最弱假设Aw。最弱的假设在证明规则中充当A，如果Prop ± T（S1±1||2S2）\（事件\是真的否则Aw不满足证明规则的前提条件。 ”[10]“”“”““”““”“”““”“形式上，Aw的特征如下：定义3.1设S2和Prop是CSP进程，定义在字母表S2和Prop上。 设1为字母表。 在字母表上定义的 C S P 过 程 A w：=（<$2<$P）<$1是过程S2和Prop i的最弱假设。对于在字母表<$1上定义的任何过程S 1，以下成立：Prop± T（S1±1 ||2 S2）\（Events\虽然学习者试图学习最弱的假设，但在学习过程中可能会发现其他假设作为中间步骤，这些假设足以表明精炼成立或不成立。 既然如此，当然，学习算法立即终止而不是继续学习最弱的假设。事实上，这是预期的情况。可以证明，最弱的假设在迹语义的意义上是唯一的（[20]），并且它包含最大的迹集，使得Prop±T（Aww2S2）（活动[20]第20话 此外，相应的LTS 如果S2和Prop的LTS是有限的，则w是有限的（[20]，[8]）。 这是根本因为它只能学习常规语言。图3显示了学习者和教师如何共同学习最弱的假设。学习算法开始于已标记的状态。 在那里，算法试图为最弱的假设创建初始候选。年初该算法完全没有关于最弱假设的信息。因此，学习者必须向老师询问一些迹的成员资格，以了解最弱的假设可能是什么样子。从技术上讲，学习者实际上开始填写包含所有观察知识的所谓观察表。一段时间后，学习者已经做了足够的观察，可以猜测最弱的假设可能是什么样子。因此，它创建了一个候选项，并要求142H. Wehrheim，D.Wonisch/Electronic Notes in Theoretical Computer Science 250（2009）135O||O∈图三. 学习算法老师问考生是否正确。如果老师返回yes，我们就完成了，算法也完成了。否则，教师返回一个反例，证明候选人不正确。在这种情况下，学习算法返回到其初始状态。然而，这一次，学习者具有关于已经观察到的轨迹的知识和关于证明候选者不正确的轨迹的附加知识。因此，学习者将反例添加到观察表中，并试图从中创建一个新的、更好的候选项。一些痕迹。 整个过程重复进行，直到最弱的假设 找到了给 定 一 个 正 确 的 教 师 ， 学 习 器 在 最 多 （ n ） 个 等 价 查 询 调 用 和 最 多 （ nnn2+nlogm）个成员查询调用之后终止，其中n是最弱假设的状态数，m是教师返回的最长反例的长度（[17]）。请注意，教师必须回答两种类型的问题：成员资格查询和等价查询。根据CSP和关于最弱假设Aw，教师必须回答以下问题：“这条迹线是最弱假设的一个元素吗？”（成员查询）和（equivalence-query）。为了实现学习器，我们使用[2]和[17]中提出的算法然而，我们在这里不详细讨论如何实际实现学习器，因为它基本上独立于所使用的特定语言。相反，我们专注于教师，从成员资格查询开始。企业查询教师必须回答一个问题，即给定的迹t是否是最弱假设的元素（即检查t迹（Aw））。 可以证明（[20]），这可以通过检查细化来回答Prop± T（CP（t））||2 S2）\（事件\H. Wehrheim，D.Wonisch/Electronic Notes in Theoretical Computer Science 250（2009）135143±||/±||\\.±||\\哪里CP（t1，t2，.，t n）：= t1→ t2→. →tn →停止是执行事件t1，...，t n，然后进入死锁（STOP）。基本上，细化检查给定的迹t是否在这个单一迹t下，S2不能违反Prop。如果我们把所有这些迹t（它们与S2一起不违反Prop）放入一个假设A，那么A实际上将有最大的迹集，它满足精化Prop TAw2S2。因此，迹线（A）=迹线（A w）成立。等价性查询这一次，教师必须回答给定过程A是否是等价于最弱假设Aw 的迹（即检查迹（A）=迹（Aw））。 如果不是这样的话，老师应该给学生提供一个反例我们现在描述一个等价查询的算法，它总是给出问题的正确答案，但是它也可以通过提供精化检查PropT（ S1<$1<$2S2）的结果来终止整个算法。（活动（见A/CN.9/647/Add.1）。 该算法基于[4]，分为三个步骤：(i) 我们首先检查以下细化：Prop± T（A ±W ||2 S2）\（事件\如上所述，最弱的假设满足此细化。因此，如果当使用A代替Aw时，精化不成立，那么A不可能是最弱的假设。在这种情况下，我们只需返回精化检查提供的反例，作为结论trace（A）=trace（Aw）的证明。如果该修正成立，我们继续进行步骤（ii）。(ii) 由于我们想完成我们的证明规则，我们现在检查以下细化：A±TS1\（事件\nw）如果这个细化事实上是真的，我们可以终止我们的算法返回真，因为使用证明规则，我们验证了系统S1||S2保证道具如果我们得到一个反例c来代替精化，我们继续步骤（iii）。(iii) 通过前面的步骤，我们现在知道证明规则不能使用给定的假设A来应用。 这可能有两个原因：假设A选择得不好，或者修正命题T（S11 2S2）（事件P）不成立。 我们现在必须区分这两种情况。 我们完成 这是通过对来自步骤（ii）的反例c进行成员查询来实现的：Prop± T（CP（c））||2 S2）\（事件\如果这是假的，那么c∈/traces（Aw）成立。但在这种情况下，EC也是一个国家-144H. Wehrheim，D.Wonisch/Electronic Notes in Theoretical Computer Science 250（2009）135联系我们∈2、、、⟨⟩下面是一个例子：Aw±TS1\（事件\\w）通过定义最弱假设（定义3.1），我们得到：Prop/± T（S1±1 ||2 S2）\（事件\因此，我们终止我们的算法，并基本上返回由成员查询提供的反例。如果成员查询为真，则ctrace（Aw）成立。由于c是步骤（ii）的反例，我们有c /迹（A）。因此，traces（A）=traces（Aw）成立，我们返回c作为这个结论的证据通过解释成员查询和等价查询，我们现在有了学习算法所需的完整教师。 因此，我们接下来可以将其应用于我们的调度程序的例子3.2调度员重新访问回想一下，我们有一个属性CycleProp0和一个系统Sched。虽然我们的一般方法是适用于系统组成的两个组件结合使用并行组合，Sched由n个组件（细胞）。 这是没有问题 因为我们可以举个例子n细胞结合在一起形成成分S1和其他组件合并为组件S2，并使用并行组合将这两个组件合并。在这个例子中，我们考虑n=4，并将两个细胞放入每个组件中。使用我们的学习算法，我们在字母表中得到四个生成的假设：{start. 0，开始。1，c. 0，c. （二）在查看生成的假设之前，我们首先解释S2的假设应该是什么这个假设应该包含S2填充CycleProp0所需的行为（或者应该施加限制）。这种假设所需要的最基本的行为就是开始。1仅在前一次启动后执行。0.同样，假设必须允许开始。2、执行C。2只有在前面的开始。1.最后，假设必须等到S2完成执行开始。2、开始3等待C 0.总之，这个假设至少应该允许跟踪开始的任何重复。0，开始。1，c. 2，c. 0，但也不允许比这多得多。图4显示了生成的假设。请注意，我们在这里提供了假设的LTS表示。在内部，假设被处理为CSP过程，这是细化检查所需的最后一个假设确实符合我们对S2的假设的期望.注意C。例如，在开始状态下执行的C 0会导致与S 2的并行组合中的死锁，因为S2等待C。2在C上同步之前。0.然而，死锁当然不被该属性禁止，任何死锁过程都满足安全属性。H. Wehrheim，D.Wonisch/Electronic Notes in Theoretical Computer Science 250（2009）135145⟨⟩⟨⟩⟨⟩⟨⟩假设1假设2假设3假设4见图4。 生成的假设另一方面，第一个假设显然允许太多的跟踪，因为假设本身可以创建违反CycleProp0的跟踪。 因此教师提供跟踪起始。0，开始。0作为等价查询的第一步中的反例。第二个假设仍然允许太多的痕迹。这一次开始。0，开始。1，开始。返回1作为证明。 即使是第三个假设也没有完成基本上只允许跟踪开始的状态链。0，开始。1，c. 2，c. 0。于是老师又开始了。0，开始。1，c. 2，c. 0，开始。1作为第一步的反例。最后一个假设最终通过了等价查询的第一步。此外，假设没有太多限制，因此第二步细化也成立。使用我们的证明规则，教师终止学习算法，结果为true 的验证。 因此，我们的调度程序实际上在使用时执行填充约束（ii）n=4。146H. Wehrheim，D.Wonisch/Electronic Notes in Theoretical Computer Science 250（2009）1354执行在本节中，我们首先描述我们如何实现3.1节中提出的学习算法。在此之后，我们比较了我们的算法实现的性能与直接FDR调用的性能我们使用编程语言Java3实现了学习算法。实现读入一个refinement断言，Prop ± T（S1±1||2S2）\X并使用第2.1节中描述的学习算法检查细化是否成立。3.1. 我们使用FDR（[1]）来检查成员查询和等价查询所需的精化实现由两个主要组件（包）组成：解析器和学习算法。解析器简单地解析FDR语法中给出的输入细化（[7]）。在此步骤之后，开始学习算法。学习算法组件可以分为学习者部分和教师部分。对于教师部分，有一个名为Teacher的接口，它主要描述成员查询和等价查询的方法学习者部分直接在GenericLearner类中实现，为了实际实现Teacher接口所需的等价查询和成员查询，我们使用FDR之前所述的。事实上，为了执行等价查询中所需的细化检查，我们使用FDR的批处理模式，它将CSP文件作为输入，并检查文件中给出的所有跟踪细化断言。然后，我们解析结果和反例（如果适用），以便在我们的实现中使用它。由于不需要那么多的等价查询，因此创建包含细化检查的文件的开销是可以接受的。然而，在成员资格查询的情况下，这种开销是不可接受的，因为可能存在 是一个很简单的大量检查成员资格查询。因此，我们使用FDR的Tcl接口来实现此目的。这使我们能够直接检查细化，而无需创建新文件，也无需为每个查询使用此接口，在大多数情况下可以非常快速地处理查询。虽然使用FDR的Tcl接口可以非常快速地处理成员查询，但仍然存在一些优化的可能性。 最明显的是，我们可以通过简单地缓存成员查询来节省许多FDR调用。因此，每当学习器不止一次地请求跟踪t的成员资格时，我们可以只返回缓存的结果。这当然比罗斯福的呼吁要快但是我们可以通过使用CSP的属性来节省CSP进程的迹集是prefix闭的（[18]），因此以下对于某个CSP进程P、迹t和t的prefixs成立：t∈ traces（P）这对于最弱的假设尤其如此我们现在使用这个属性3http://www.cs.uni-paderborn.de/index.php? ID=8967 L=1H. Wehrheim，D.Wonisch/Electronic Notes in Theoretical Computer Science 250（2009）135147∈∈∈∈||\\两种缓存（[3]）。首先，前缀缓存检查跟踪t是否有已经缓存的t的前缀s如果有一个缓存的前缀s和s/traces（Aw），那么t /traces（Aw）也成立。在这种情况下，我们返回false。否则，我们使用所谓的sunix缓存。事实上，我们检查t的最短缓存扩展tJ，使得t是tJ的前缀。如果tJ迹（Aw）成立，我们可以推断，t traces（A w）成立，我们返回true。如果这种缓存策略也失败了，那么将使用FDR检查查询。从 技 术 上 讲 ， 我 们 有 类 CachedAMSTeacher 、 PrefixCachedAMSTeacher 和SuffixCachedAMSTeacher ， 它 们 实 现 了 相 应 的 缓 存 策 略 。 此 外 ， 我 们 有 类FDRAMSTeacher和FDRAEQTeacher，它们分别使用FDR实现成员查询和等价查询。所有这些类都可以添加到一个名为GenericTeacher的类中，这个类基本上协调添加的教师来实际执行查询。通过添加或删除cache-strategy类的实例，我们可以打开或关闭相应的缓存策略默认情况下，启用缓存和前缀缓存FDREQTeacher类的一个替代类是RecFDRAEQTeacher类，它也可以处理等价查询。与FDRAEQTeacher类相反，如果可能的话，这个类通过再次调用学习算法来检查细化。实际上，它递归地检查等价查询的第一步，如果S2由多于c个用户定义的常数c的分量组成。第二步是递归地检查S1是否包含c个以上的成分。第三步是使用FDR检查，因为它基本上只是一个成员查询。在递归检查等价查询的第一步时必须小心，以确保算法终止。 如果我们将学习算法直接应用于Prop ± T（A）w||我们实际上是试图找到一个假设AJ满足相应证明规则的条件AJ± TA\（Events \n W）和Prop ± T（AJ\n W<$2S2）（Events\n P）。这样，我们就进入了一个无限递归循环。因此，在应用学习算法之前，我们必须交换A和S2在这种情况下，我们最终得到了AJ± TS2\（事件\n Jw）和Prop ± T（AJ\nJw||wA）\（Events\递归调用只有在直接调用花费很长时间时才有意义。目前，我们使用以下启发式：如果组件的数量超过c，则直接调用将花费很长时间。 这当然是一个相当粗略的启发式，但由于由于缺乏其他（更好的）启发式，我们使用这种粗略的启发式。我 们 现 在 提 供 一 些 实 验 结 果 。 我 们 在 3GHz （ Pen- tium 4 ） Linux 系 统（OpenSUSE 10.2）上运行了测试，内存为1GB。 在表1中，我们收集了• 直接FDR呼叫，• 学习算法的实现• 学习算法的递归实现148H. Wehrheim，D.Wonisch/Electronic Notes in Theoretical Computer Science 250（2009）1353、、、当检查细化时，CycleProp0± TSCHED\{完成。0，完成。1，. . . ，完成。（n − 1）}的调度程序的不同n.我们使用默认的缓存设置来实现（即缓存和前缀缓存）。此外，对于非递归实现，我们通过将n+1个单元放入第一个组件，将其他单元放入第二个组件来拆分进程SCHED当使用递归实现时，我们将其一分为二，并使用c=8。n直接FDR呼叫学习算法学习算法（递归）100.235s1.348s5.43s132.247s1.99s8.27s1626.42s3.173s72s19297.5s6.663s106s223290年代20.33s145秒25内存不足91.25s222s30内存不足小行星2067385s35内存不足内存不足小行星87440内存不足内存不足小行星1534表1检查属性CycleP rop0时，使用不同方法为调度程序创建在表2中，我们在检查细化时收集了运行时值使用与上述相同的设置进行计划参数±T计划正如我们在这里看到的，对于一个属性，组合验证要好得多，对于另一个属性，简单地使用FDR。这是因为在学习过程中产生的假设的大小。当假设比S1本身小得多时，组合验证将优于FDR，否则学习的开销将使验证慢得多。 因此，我们显然需要一个成功的应用程序，这种技术的一个重要特点是，它是一种预先确定成分验证是否有意义的手段。这将是今后工作的主题H. Wehrheim，D.Wonisch/Electronic Notes in Theoretical Computer Science 250（2009）135149\r\n±||\\n直接FDR呼叫学习算法学习算法（递归）30.043s2.323sN/A40.044s3.999sN/A50.047s6.537sN/A60.051s14.63sN/A70.066s28.81sN/A80.093s80.63sN/A90.163s214.8s268.1s100.366s小行星1056600.3s表2检查属性SchedP rop时，使用不同的方法为调度程序创建5平行证明规则除了基本的假设保证证明规则之外，我们的实现还支持[10]中提出的并行证明规则，这里直接在CSP中改写Prop ± T（A1±W||1S1）\（事件\Prop± T（A2±W ||2 S2）\（事件\traces（A1）traces（A2）=Prop± T（S1±1||2S2）\（事件\其中迹线（Q）被定义为迹线（Q）的互补集（即，t ra ces（Q））。要求CUPΣ11992年举行。然而，假设的主要假设定义如下：w=（与基本证明规则相比，这种并行证明规则的主要优点是它是对称的。因此，我们可以同时独立地学习系统组件的假设。更准确地说，CSP过程A1和A2描述了S1和S2可以保证Prop的假设。证明规则的第三个条件简单地确保两个假设不排除共同的痕迹。这是证明规则合理所必需的，因为，如果我们对两个假设都使用死锁进程STOP（即不允许每个非空跟踪），那么对于任何CSP进程S1和S2，前两个条件都将被平凡地满足。如果证明规则的三个条件都成立，T（S1） （2）（活动（英文）也是（10）。由于现在有两个假设要学习，我们也使用两个学习算法。这两种学习算法再次尝试学习最弱的假设150H. Wehrheim，D.Wonisch/Electronic Notes in Theoretical Computer Science 250（2009）135∩∅联系我们±||\\联系我们1和2。因此，成员查询可以类似于第3节中介绍的成员查询来实现。然后，两种学习算法都为最弱的假设创建候选Ai（i1， 2）检查这些候选项是否可以用于证明规则。乍一看，候选人需要填写细化提案T（Aiw1Si）（事件 （见A/CN.9/647/Add.1）。 这可以在学习算法的等价查询中本地检查当找到填充这个的候选项时，我们需要检查traces（A1）traces（A2）=是否成立。为了检查这一点，我们将此属性转换为细化检查：traces（A1）traces（A2）=惠迹（A1）迹（A2）=w惠迹（A1）迹（A2）=w右侧可以作为CSP过程运行的轨迹集，在字母表上的每个迹线（即，运行=Qe∈N e→运行）。的并集迹 集 可 以 使 用 CSP 中 的 choice-operator 来 表 示 因 此 ， 我 们 只 需 要 检 查A1QA2=Trun，它保持iA1QA2±T运行保持。这个简单的微调可以再次使用FDR进行检查。如果它成立，证明规则完成，我们返回true。否 则 ，我们得到一个反例t. 然后我们检查t在迹（Aw，1）和迹（Aw，2）中的成员关系如果t是不是两个迹（A w，i）的成员，它是一个实反例，我们返回false（[10]）。 否则，如果t是trace（A w，j）中的成员，对于某个j 1，2，我们返回t作为证明，Aj不是相应学习算法的最弱假设（[10]）。我们的实现可以在细化检查期间使用这两个规则。这对于实现并行证明规则的递归版本特别有用。在这种情况下，我们实际上交替调用两个证明规则的算法6结论在本文中，我们提出了一种组合技术的痕迹细化检查CSP。该技术使用基本的假设保证推理以及[4]的假设学习算法。该方法利用了现有的CSP模型检查器FDR，在学习过程中被用作教师。虽然该技术尚未在FDR中实现，而是需要在每次需要教师时调用FDR，但对于某些示例，它比普通使用FDR有相当大的改进。精细优化技术的使用，甚至AG推理的递归应用，使我们进一步加快了速度。在未来，我们打算更深入地研究组合方法何时优于非组合方法，以便能够自动决定支持或反对组合验证。H. Wehrheim，D.Wonisch/Electronic Notes in Theoretical Computer Science 250（2009）135151∞引用[1] Fdr2.http://www.fsel.com，版本2.83。[2] 丹娜·安格鲁因从查询和反例中学习正则集。信息计算，75（2）：87[3] Therese Berg，Bengt Jonsson，Martin Leucker，and Mayank Saksena. 对安格鲁学习的见解电子笔记理论Comput. Sci. ，118：3[4] 杰米森·M Cobleigh，Dimitra Giannakopoulou，and Corina S. 帕萨雷亚努 学习成分验证的假设。在Hubert Garavel和John Hatsaughty，编辑，TACAS，体积2619计算机科学讲义，第331-346页。Springer，2003年。http://dblp.uni-trier.de/rec/bibtex/conf/tacas/CobleighGP03.[5] W.P. de Roever，U.Hanneman，J.Hooiman，Y.Lakhneche，M.Poel，J.Zwiers和F.德布尔。并发验证。剑桥大学出版社，剑桥，英国，2001年。[6] E. A.爱默生和V·卡隆。减少模型检查的数量。In D. A. McAllester，编