CSP模型检验的假设-承诺支持

±ǁ理论计算机科学电子笔记185（2007）121-137www.elsevier.com/locate/entcsCSP模型检验的假设-承诺支持尼克莫在1系统保证组，QinetiQ Malvern，英国迈克尔·戈德史密斯2Formal Systems（Europe）Ltd，Oxford，UK和牛津大学伍斯特学院摘要我们提出了一个简单的公式假设承诺推理CSP。在我们的公式中，一个过程的假设-承诺风格的属性是COM的假设-承诺，对于一些我们陈述了一些证明规则，这些规则允许我们从组合系统的组件的相应属性中推导出组合系统的承诺-承诺风格属性，并给出适当的边条件。大多数规则都有一个表面上吸引人的“同态”性质，在这个意义上，整个假设和承诺过程与整个系统类似。我们还提出了一个“非同态”的规则，相当好地对应于证明规则建立的承诺承诺理论。前因和副条件表示为可由精化风格的模型检查器FDR单独检查的精化。最后给出了具体的应用实例.关键词：假设-承诺，假设-保证，CSP，模型检测，组合推理1介绍组合程序验证的原则是基于组成子程序的程序验证，而不需要知道这些子程序的内部结构[15]。这概括了（硬件和/或软件）系统的组合验证组合验证允许通过分别推理其组件来验证大型系统。所谓的组合证明规则被定义为1电子邮件：N. eris.QinetiQ.com2电子邮件：michael@fsel.com1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.05.033122N. Moffat，M.Goldsmith/Electronic Notes in Theoretical Computer Science 185（2007）121ǁ±ǁ对于程序操作员（更一般地，对于系统操作员）。这些规则的形式是：. .而Pn满足φn则推论P满足φ”。[15]组合验证被广泛认为是大型系统验证的必要条件，以抵消状态爆炸问题。当使用进程代数CSP [4，10]对系统进行建模和推理时，我们对组合推理感兴趣，特别是在精化风格的模型检查上下文中。 CSP的一种组合推理形式在[10]中描述了，由此可以从（单独证明的）其组分的细化性质推断复合系统的细化性质PJ±P<$QJ±QPJQJ±PQ所示的规则隐含在平行算子的单调性和加细的传递性中。类似的规则适用于所有CSP运算符，因为它们都是单调的。这些规则通常用于对系统进行组合推理，其中每个组件都独立于其环境进行指定，即无论组件在更广泛的系统中的上下文如何，相同的规范都是合适的。然而，这些规则实际上足够强大，可以对更一般的系统进行组合推理：其中组件可能仅在某些环境中按需一个特定的过程是可能的，PJ来编码关于进程P的环境的某些跟踪假设，布置为一旦假设被打破，即在执行不允许的跟踪之后，PJ就根据[14]的术语，这相当于具有隐式承诺-承诺规范的承诺-承诺推理。然而，这种风格的规范可能是繁琐的。此外，当可以为真实系统识别出“期望的组件行为”和“假设的组件环境”的清晰、明确的描述时，将假设与承诺分开是很方便的因此，我们希望支持约束-承诺推理，其中规范包括对组件应该正确运行的环境和组件在这种环境中的期望行为的单独、明确的描述。我们使用明确的“假设”和“承诺”过程将承诺-承诺属性公式化为细化 这种形式适合于直接使用一个精化风格的模型检查器进行检查，比如FDR [3]。然而，对于大型系统，这样的属性可能是计算昂贵的，甚至难以直接检查;因此需要一种组合方法。我们陈述了一些结果，这些结果允许从组合系统的相应性质中推导出组合系统的这样制定的承诺-承诺风格性质。 它的组成部分，给予适当的侧条件。例如，两个定理采用以下形式（具有不同的边条件集COM1±101接头 1COM2 ±102接头2COM1ParticipCOM2±（101Participants2）COM（ASS1ParticipantsASS2）操作符Participate表示N. Moffat，M.Goldsmith/Electronic Notes in Theoretical Computer Science 185（2007）121123↔ǁ∩\\12SYS12002年左中期权Fig. 1. 一个开放的复合系统在共享的事件上nised，然后隐藏。这些定理具有表面上吸引人的给出了一个“非同态”的结果，它与已有的承诺理论[6，2]的证明规则相当一致。所有的前因和副条件都表示为可以通过精化风格的模型检查单独检查的精化。最后举例说明所得结果。第2节描述了目标复合系统的类型，第3节解释了我们对作为细化属性的优先承诺属性的表述。第4节介绍了同态定理，并给出了它们的应用的小例子。第五节给出了非同态定理，它更接近于经典的选择-承诺规则，并且比同态定理有一定的优越性。最后给出一个小例子说明了该方法的有效性。由于篇幅限制，我们只能给出证明草图，但[7]包含了所有定理的详细证明。第6节将我们的方法与相关工作进行了比较。第7节给出了我们的结论和未来的工作。2系统模型我们考虑一个系统过程，它有两个组成部分：=中期 2002年其中，进程A1和A2是其字母分别包含在已知字母表A1和A2中的进程，并且mid=A1和A2是同步字母表。[3]对于每一个aushi，一个令人满意的选择是由aushi的通道所诱导的字母表：所有可以在这些通道中的任何一个上交流的事件。4左= a1a2，右= a2a1，系统设计如图1所示。为了简单起见，该图将左、中和右描绘为单个通道，但它们可以对应于多个通道。有时，中间的同步设置会被隐藏，使这些事件内部。在这种情况下，系统可以建模如下：3在这些假设下，=1aa2。4我们避免使用精确的字母表，因为精确的字母表函数，通常表示为α在CSP的机器可读版本中不可用[11]。124N. Moffat，M.Goldsmith/Electronic Notes in Theoretical Computer Science 185（2007）121ǁ∪±ǁ±ǁ∪∪→→∪·→=（中期2）\mid我们称一个系统为开放的，如果left right非空，也就是说，如果它有外部可见的通道，而mid事件被隐藏。否则，它将关闭。3假设-承诺性质如前所述，我们使用“假设”和“承诺”流程将承诺-承诺属性（AC属性）制定为细化。设是一个进程，其相关字母表a包含的所有事件，并设ASS和COM是进程。为了简单起见，我们假设（像JavaScript一样）ASS和COM永远不会在JavaScript之外运行。然后我们说进程满足CSP语义模型M中的请求-提交属性（ASS，COM），如果（一）COMMASYS 屁股正如在[10]中所解释的，精化PMQ意味着，在语义模型M中，Q的行为是P的行为。5我们看到，（1）可以解释为说，在环境ASS中的行为只表现出承诺过程COM“允许”的行为的单调性允许更强的解释。它允许我们将“在环境中ASS”替换例3.1假设一个进程有通道A、B和F，那么aB=A B F包含了所有的事件。（在本文中，我们让通道名称表示在该通道上通信的事件的字母表。此外，假设ASS=RUN（A，B）并且COM=BUFF（A，B），其中RUN（X）=Qx：X xRUN（X）是一个（单态）进程，它可以执行来自X的任何事件序列，并且从不拒绝X的事件，BUFF（chan1，chan 2）=chan1？x chan2！x BUFF（chan1，chan 2）是从chan 1到chan 2的一个位置缓冲器。 然后，轨迹AC属性（ASS，COM）表示，所有的轨迹的轨迹是从A到B的一个buffer，只要环境的buffer从来没有执行的F事件。在此，F可以是导致故障的故障事件。 在这种情况下，假设有一个非常简单的形式，因为它允许在其字母表中的事件的子集，而不管早期的系统活动。本文考虑的所有AC特性都有类似的简单假设，尽管第4节和第5节中给出的结果在假设更复杂时也适用 Q这种AC特性的显式公式适合于直接使用一个细化风格的模型检查器，比如FDR[3]。但这可以通过计算5我们考虑CSP在轨迹模型T中，一个进程稳定故障模型F另外记录了过程的故障（t，X），其中t是到某个稳定状态（其中没有内部活动是可能的），X是该状态下的拒绝（一组事件，所有这些事件都可以同时被拒绝）。故障-分歧模型记录了故障（所有故障，而不仅仅是稳定故障）和分歧，这是一个发散状态的痕迹（如果可能的话，内部行为的无限序列）。我们使用更多的细节可以在[10]中找到N. Moffat，M.Goldsmith/Electronic Notes in Theoretical Computer Science 185（2007）121125⟨ ⟩ ⟨ ⟩⟨ ⟩⟨ ⟩⟨ ⟩⟨ ⟩ ⟨ ⟩对于大型系统来说很昂贵。使用第4节和第5节中的结果，合成方法是可能的。经典的[6，2]，约束-承诺理论是在并发系统的背景下建立的顺序组件，通过消息传递进行交互。系统由子系统（最终由顺序组件）通过并行和顺序组合构建。历史变量记录通信历史。每个组件逻辑变量反映了初始状态下输入变量的值.经典的AC属性被表示为以下形式的拒绝-承诺正确性公式：（二） A，C其中A和C是通信历史和逻辑变量上的假设和承诺谓词，并且φ和φ是通信历史、逻辑变量和程序变量上的实质上，在[2]中，分量P的有效AC公式被解释如下：如果φ最初成立（即，在P开始其执行的状态下），则C最初保持，并且还假设A在所有先前的通信之后保持，C在每次通信之后保持，并且在终止时保持（如果发生这种情况然而，我们的配方省略了前置和后置条件，因为我们只关心状态，因为它表现为进程通信，我们专注于表征单独使用并行进程操作符组成的非参数化系统。6我们基于过程的假设和承诺表述与经典理论的假设和承诺有多接近？我们非正式地解决这个问题的痕迹模型。 回想一下我们对等式（1）的非正式解释：在任何满足ASS的环境中，ASS只表现出“所有由COM提供的”行为。 我不想把所有的东西都输给你。 对于迹t，t-o表示t由单个even扩展到o. 然后，对于满足ASS的一个函数中的所有跟踪t-o，t-o是COM的跟踪。 也就是说，对于所有的跟踪t-o，如果t-o是ASS的跟踪，那么它就是COM的跟踪。我们稍后强加的条件（假设过程对组件输出事件的自由性）然后给出：对于所有的跟踪t-o的COM，如果t是ASS的跟踪，那么t-o是COM的t种族。如果到当前状态的迹线是ASS的迹线，这相当于COM允许的输出，这很好地对应于AC公式的经典解释。我们认为，假设和承诺作为过程的表达是新颖和有趣的。使用CSP工艺的替代配方是可能的，但这里不考虑6我们的方法可以扩展到考虑参数化系统的AC特性，在这种情况下，参数将被视为对初始状态的贡献。我们还期望可以处理其他过程操作符，特别是顺序组合。126N. Moffat，M.Goldsmith/Electronic Notes in Theoretical Computer Science 185（2007）121SR∪⊆∪ǁ±ǁǁǁǁ±ǁǁǁǁF1F2B一个C图二. 一个有缺陷的开放系统。 R和S的行为（在痕迹模型中）是从A到B和从B到B的B到C，而通道F1和F2上分别没有信号出现。4同态定理本节中的定理发现了一个给定节点的承诺-承诺性质。它们要求定义字母a1和a2，并满足第2节和第3节中描述的条件。在形式上，它们要求α（i）α（ASSi）α（COMi） ai，（i=1，2），其中函数α给出过程的精确字母表。简单地说，我们说aa1和aa2是健康的。第一个定理适用于以下情况：当通过对共享事件进行同步并使这些事件可见而组成的x1和x2定理4.1（共享事件可见，允许相互依赖）对于M = T，F或N，COM1±M11COM2 ±M22COM1中期A1COM2M（COM1中期（2）ASYSaSYS2（ASS1）中期 ASS2）其中，aa1、aa2是健康的，mid = aa1 <$aa2，aa1 =aa1 <$a2。前件中的条件仅仅是组件的各个AC特性。结果很容易用代数方法导出。单调性给出COM1COM2M（COM1ASS1）（COM2ASS2）。后果是2016年12月1日然后通过重复应用获得，到右手边及其子公式，X<$Y-对称、X<$Y-对称定律以及PX<$YQ与P<$ Q当α（P）<$X时，[ 10 ]中的α（Q）Y。X∩Y例4.2图2描述了一个有两个组件和五个通道的系统。组件R在A和F1上输入值，在B上输出值;组件S在B和F2上输入值，在C上输出值。我们假设通道A、B和C都传送相同类型的数据。图2的系统在CSP中可以表示为：B假设R和S满足AC性质（ASSR，COMR）和（ASSS，COMS），CSPASSR=运行（A→B）COMR=BUFF（A，B）ASSS=RUN（B/C）COMS=BUFF（B，C）对于字母aR和aS，定义如下：aR=A BF1aS =B CF2N. Moffat，M.Goldsmith/Electronic Notes in Theoretical Computer Science 185（2007）121127±ǁǁ∩±ǁ↔这些单独的AC特性类似于实施例3.1中讨论的AC特性。每一个都表示，只要在相应的故障通道F1或F2上没有事件发生，组件就像从输入到输出的一个位置缓冲器一样工作。我们寻求总体假设和承诺过程ASS和COM，使得复合系统在迹中证明AC属性（ASS，COM模型，即这样COM测试就能让你保持健康。ASYS设mid=aRaS=B，定理4.1是适用的。其假设已获满足，包括字母表条件。考虑到R=R S，我们B推导出COMTASS，其中ASYSASS=ASSRASSSCOM=COMRCOMSB B=RUN（AB）RUN（BC）=BUFF（A，B）BUFF（B，C）B B=运行（ABC）a =aRaS=AB CF 1F2推导出的故障-承诺性质表明，当两个故障通道上都没有信号发生时，组合系统的迹线是一个两个位置的缓冲器的迹线。Q定理4.1的有用性是有限的，因为由此产生的假设过程与所有事件的假设如果个别假设约束了中期事件，这些约束就不能使整个假设变得无用。例如，mid事件可以被适当地认为是在现实环境的控制之外，在这种情况下，可以不实现任何环境来保证满足总体假设。另一方面，对mid事件的约束可以通过一些未建模的监视和控制机制来实现。 此外，目标可能仅仅是验证系统的相比之下，定理4.3和4.5，下面，适用于当101和102是由对称管道组成，即通过同步共享事件（中），然后隐藏它们。由于中间事件是隐藏的，因此没有机会直接约束它们的结果假设在这一点上需要一些额外的术语。 首先，我们回顾一下[10]中描述的惰性抽象和可分性的概念。在CSP的跟踪模型中，延迟抽象等同于隐藏。 在更丰富的模型中，它就像隐藏，除了它避免了引入（操作）分歧。本文中的例子都使用了迹线模型，因此这些例子的区别可以忽略不计128N. Moffat，M.Goldsmith/Electronic Notes in Theoretical Computer Science 185（2007）121\±ǁ±ǁ-参与活动±ǁ--ǁ令LAbsX（ASS）表示通过从字母表X中惰性地抽象ASS而获得的过程。令LProjX（ASS）表示LAbsX（ASS），通过抽象掉X之外的所有事件而获得的过程，我们称之为ASS到X的惰性投影。假设过程ASS是• 在M中X上可分的，如果ASS = MLAbsX（ASS）|||LProjX（ASS）;• 如果ASS = MLAbsX（ASS），则M中X上的中性|||运行（X）。这两种情况都可以使用FDR进行检查。可分性是一个相当强的属性，对应于行为w.r.t.的完全独立性。两组事件：X和它的补码。中立性甚至比可分性更强 对轨迹模型T中的一组事件X保持中立，就是在T中的X上是可分离的，并且能够执行来自X的任何事件序列。（在更丰富的语义模型F和N中，中立性暗示了额外的属性。这一节的其余定理要求在mid上的可分性或中立性。定理4.3给出了一个不约束内部事件的假设，但这个定理同时施加了一个可分离性条件和一个中性条件。定理4.3（隐藏的共享事件，没有相互依赖）对于M = T或F，COM1M1A1ASS1COM2M2A2ASS2LProjmid（ASS1）±MLProjmid（COM2） LProjmid（ASS2）±MLProjmid（COM1）ASS1在M中路中立ASS2在M中路COM1COM2M（201年2月2日）ASYS （ASS1参与ASS2）其中，aa1，aa2是健康的，mid = aa1<$aa2，aa 1 =（aa1<$a2）\mid和·Participate·=（· ǁ ·）\mid。中期除了单独的AC属性之外，还有两个形式为LProjmid（ASSi）M LProjmid（COMj）.这些规定表明，投射到接口字母表mid上的组件j的承诺过程必须细化投射到相同字母表上的组件i的承诺过程。从本质上讲，这些条件是说，每个组成部分不幸的是，证明很长，很难画出来。布里干酪，使用单调性CSP的，中点上的中性为101，RUN（X）是所有模型M中的单位，X不相交交织后共享并行等价于不同分区上的连续共享并行，我们得到COM1COM2M（（n =1中期（2）ASYS（LAbs中段（ASS1）|||LAbsmid（ASS2）\mid。 这可以减少对于这个结果，使用mid上的可分离性和mid上的可分离性，月中旬N. Moffat，M.Goldsmith/Electronic Notes in Theoretical Computer Science 185（2007）121129±ǁ∩∪±ǁ∪∪∪∪D甚至图三.一个简单的管道开放系统，与隐藏的渠道该定理要求ASS2在mid上的可分性和ASS1在mid上的较强的中性性。这种情况的一种发生方式是在单向管道中，mid只包含输出端1和输入端2。例4.4考虑图3所示的管道系统。它由两个组件组成，两个外部通道和两个内部通道。Q输入C上的值并输出A和B上的值;P输入A和B上的值并输出值on D. 它可以在CSP中表示为：AB P）\A\B.假设Q和P满足AC性质（ASSQ，COMQ）和（ASSP，COMP），CSPASSQ=RUN（ABEvenC）ASSP=RUN（OddA OddBD）COMQ=RUN（OddA<$OddB<$C）COMP=RUN（A<$B<$EvenD）其中字母表具有建议的含义，对于字母表aqq和AQP定义如下：aQ=A B CaP =A BD我们寻求假设和承诺过程ASS和COM，使得复合系统满足迹模型中的AC属性（ASS，COM），即等那辆摩托车，为了健康的休息。ASYS设mid=aqqaqp=AB，定理4.3是适用的。其假设得到满足，包括字母表条件。特别是，Q中立在中路。 回想一下，AB P）\AB，我们推断，COMTASSS，其中ASYSASS=ASSQ参与者ASSP=（RUN（A B EvenC）ABRUN（OddA<$OddB<$D））\A<$B=RUN（EvenCD）COM=COMQParticipCOMP=（RUN（OddA OddB C））ABRUN（ABEvenD））\AB=RUN（C=EvenD）aR=（aRQaRP）\mid=CD推导出的承诺-承诺性质表明，D上的是偶数，如果C上的所有（先前）输入是偶数。QCQ奇怪P一个奇怪的甚至B130N. Moffat，M.Goldsmith/Electronic Notes in Theoretical Computer Science 185（2007）121|||\n这个定理也涵盖了许多非流水线系统，因为它允许数据在两个方向上并行：ASS1的中立性（这仅仅是一个假设过程）只要求它不约束共享接口事件。即使值在组件之间双向传递，也可能是这样的：Promise1将满足其承诺并不取决于共享接口处的行为。不幸的是，定理4.3不适用于每个组件定理4.5削弱了允许有相互假设的系统的条件之一：它要求每个分量假设过程是可分离的，而不是一个是可分离的，另一个是中立相互依赖带来的关键挑战是避免循环往复。定理4.5和5.1通过施加额外的条件来避免循环推理，以确保假设不会“错误地”打破，即通过出现以下情况一个单一的通信事件。特别是，这些定理在假设过程上设置了额外的我们说一个过程P在X上是自由的，如果P RUN（X）TRUN（X），其中X表示所有已定义事件的集合。 这个条件等于P永远不能拒绝X的任何事件。与其他定义的条件一样，集合上的自由度可以使用FDR来检查。CSP通道是无方向的-任何进程都可以向特定通道输入值（因此绑定变量）或向其输出值。然而，在进程的“输入”或“输出”事件的定义集上需要自由度。下面的定理适用于将组件事件划分为输入和输出的任何划分，但是当CSP通道被认为具有与建模的系统通信相同的“方向”时，它们最有可能是有用的对于自由性条件，以防止同时打破的组件的假设，下面的定理依赖于进一步的条件：每个共享事件是一个组件过程的输入和输出的其他。我们称之为进出同步。这是一个非平凡的条件，因为CSP能够模拟更复杂经典的承诺理论[2，6]。[7]注意，定 理 4.1 和 4. 3 不 需 要 输入/输出同步。N. Moffat，M.Goldsmith/Electronic Notes in Theoretical Computer Science 185（2007）121131±ǁ±ǁ-参与活动∩ ∩∩定理4.5（隐藏共享事件，允许相互依赖）对于M = T或F，COM1M1A1ASS1COM2M2A2ASS2LProjmid（ASS1）±MLProjmid（COM2）LProjmid（ASS2）±MLProjmid（COM1）ASS1在M中可分离ASS2在M中可分离ASS1在中可分离ASS2在M中可分离ASS 1在M中可分离1COM1COM2M（201年2月2日）ASYS2（ASS1参与ASS2）其中，aa1，aa2是健康的，mid = aa1<$aa2，aa 1 =（aa1<$a2）\mid，·Participate·=（· ǁ ·）\mid，并且101和102是输入/输出同步的。中期这个证明与定理4.3类似。其不同之处在于初始还原步骤更复杂。 这种简化的核心是一个引理，它说：X X（R<$S）±MP<$R，当Q±MLProjX（R<$S），S±MLProjX（P<$Q），和X x X X痕量（Q） 痕量（S），X联合（拒绝）（Q/t）拒绝（S/t））=100。 [7]详细内容。D甚至图四、具有相互依赖的组件和隐藏通道的开放系统例4.6考虑图4所示的系统。Q在通道A和C上输入值，在通道B上输出值;P在通道B上输入值，在通道A和D上输出值。它可以通过将例4.4中的通道A反转来获得。假设Q和P满足CSP的迹模型中的AC性质（ASSQ，COMQ）和（ASSP，COMP）ASSQ=RUN（OddABEvenC）ASSP=RUN（AOddBD）COMQ=RUN（AOddBC）COMP=RUN（OddABEvenD）其中，字母表具有建议的含义，并且aqq和aqp定义如下：aQ=A B CaP =A BD我们寻求假设和承诺过程ASS和COM，使得复合系统=QABCQ奇怪P一个奇怪的甚至B132N. Moffat，M.Goldsmith/Electronic Notes in Theoretical Computer Science 185（2007）121±ǁǁ∪ǁ∪∪ǁ∪ǁ±ǁǁ12满足T中的AC属性（ASS，COM），即， 这样，COM测试系统，ASYS吃点健康的早餐设mid=aQaP=AB，定理4.5是适用的。它的假设是满足的，包括所有的副条件。8我们推断COM±T这是一个很大的问题，ASYSASS=ASSQ参与者ASSP=（RUN（奇数A B 偶数C）中期RUN（AOddBD））\AB=RUN（EvenCD）COM=COMQParticipCOMP=（RUN（A OddB C）中期RUN（OddABEvenD））\AB=RUN（C=EvenD）aR=（aRQaRP）\mid=CD推导出的AC特性表示，如果通道C上的所有（先前）输入都是偶数，则通道D上的所有输出都是偶数。Q下一节给出了一个更有用的结果，并给出了一个应用示例。它将表明，没有一个同态定理产生一个有用的结果，为该例。5更有用的定理下面的定理非常接近于在提交-提交文献[6，2]中并行组合的经典证明规则。 我们预计它比第4节的同态定理更有用，因为它不要求各个假设在共享事件上是中性的，甚至是可分离的。定理5.1（共享事件可见，允许相互依赖，假设给定）对于M = T，COM1±M1组件1COM2 ±M2 屁股22002年8月1日ASS1是自由主义者，在退出时退出，COM1是自由主义者，COM2是自由主义者，1 2ASS1±MLProjaerodynamic1（ASSBCOM2）ASS2±MLProjaerodynamic2（ASSBCOM1）COM1中期A2COM2M（COM1中期（2）ASYS屁股A1[8]注意定理4.3不适用;ASSQ和ASSP在mid上都不是中性的。然而，每一个都是可分离的，并且满足定理4.5的自由性条件。N. Moffat，M.Goldsmith/Electronic Notes in Theoretical Computer Science 185（2007）121133∩∪∧⇒其中，aB1、aB2是健康的，mid = aB1aB2，aB 1 = aB1aB2，并且aB1和aB2是输入/输出同步的。像往常一样，前两个条件只是单独的AC属性。接下来的四个条件是对各个ASSi和COMi过程的自然自由度约束。本质上，每个ASSi自由性条件都声明ASSi的满足不能被从R0i到R0j的输出无效。相反，每个COMi自由性条件都声明COMi的满足不能被从Rj到Rji的输入无效。我们期望这些条件将经常被满足，因为当所有消息都由最多一个组件输出并且组件不能拒绝输入时，使用非自由的ASSi和COMi9后两个条件涉及一个过程ASS，它是后件中的总体假设过程这些条件表明，每个单独的假设ASSi由以下过程来定义：ASS与字母表上的其他承诺COMj同步，然后懒洋洋地投影到字母表上。这些条件可能看起来最不自然，但它们对应于经典AC理论中的自然条件，其形式为它们确保共享接口上的每个单独的组件假设都由其他部分的承诺与总体假设一起[7]有详细的可靠性证明。它使用归纳的跟踪长度，并考虑两个单独的情况下：一个组件，以满足其承诺失败之前，其他已经失败，和失败的两个组件在同一事件。第一种情况是不可能的，因为非失败的承诺和总体假设ASS一起满足“失败”系统的假设，因此其承诺也必须得到满足。第二种情况的不可能性是论证使用在/出同步性和自由性：共同的事件必须是一个组件的输入和输出的其他，和自由性进行满意的假设和承诺之前，这一事件后的满意。重要的是，总体假设ASS只出现在前因的最后两个条件中。由于这些条件确保了共享接口上的假设由B11和B12的承诺强制执行，ASS只需要强制执行组件假设的任何剩余方面（将在B11和B12的外部接口上）。在下面的示例中，没有这样的限制，所以ASS可以是RUN（aeqs）。例5.2这个例子是基于[2]中描述的一个例子，它本身是由于[13]。考虑图5所示的系统，它可以通过连接例4.4中的通道C和D来获得，从而引入反馈回路（通道D; C的名字被删除）。假设Q和P满足约束-承诺性质（ASSQ，COMQ）[9]没有什么必要作出限制一个进程的产出的假设，因为它可以被削弱为不限制产出的假设，而不需要对任何承诺作出令人满意的满足。类似地，在这个并发模型中，任何限制流程输入的提交都不能构成有效AC属性的一部分134N. Moffat，M.Goldsmith/Electronic Notes in Theoretical Computer Science 185（2007）121∪∪ǁ±ǁǁ∪ǁ∪∪ ∪±偶数DQ奇怪P一个奇怪的B图五、具有相互依赖的组件的封闭系统和（ASSP，COMP）在CSP的轨迹模型中ASSQ=RUN（ABEvenD）ASSP=RUN（OddA OddBD）COMQ=RUN（OddA<$OddB<$D）COMP=RUN（A<$B<$EvenD）其中，字母表具有建议的含义，并且aqq和aqp定义如下：aQ=A BD aP =A BD现在假设我们希望获得复合系统的承诺，但在这种情况下不假设任何环境。这导致我们表达期望的顶层假设过程：ASS=RUN（ABD）当与共享字母表A B D，ASS上的系统进程并行时，在跟踪语义模型中没有约束效果;因此，当用作假设过程时，它表示跟踪模型中的假设为真我们寻求一个承诺过程COM，使得复合系统=QABD满足迹线模型中的AC属性（ASS，COM），即使得COM±T屁股，为了一些健康的休息。ASYS定理5.1适用。它的假设是满意的，包括所有方面条件 我们推断COMTASYS 屁股，在哪里COM=COMQ中期COMP=RUN（OddA OddBD）中期 RUN（ABEvenD）=RUN（OddA<$OddB<$EvenD）a= aQaP=A BD推导出的预承诺性质表示在平凡假设下，在信道D上通信的所有值都是偶数，而在信道A和BQ适用于这个例子的同态定理是定理4.1和4.5. 然而，对于这个特定的例子，这两种方法都没有产生有用的结果的前一个定理给出了RUN（OddA OddB EvenC）ABDRUN（奇数A）N. Moffat，M.Goldsmith/Electronic Notes in Theoretical Computer Science 185（2007）121135±∪ǁǁOddBEvenC），这相当于说，在假设它具有期望的行为的情况下，它具有期望的行为。后一个定理给出了STOP STOP，这也是没有用的。（尽管如此，同态定理对于某些开放系统似乎是有用的，如例4.2、4.4和4.6所示。6相关工作有很多工作领域的承诺承诺推理。我们已经提到了[6，15，2]，在第3节中，我们将假设-承诺性质的公式与经典方法进行了比较。Pandya [8]为CSP程序建立了一种基于有限跟踪的一阶逻辑断言的验证-承诺验证风格。同样，Kay和Reed在[5]中提出了关于CSP过程的组合推理的演绎规则。这两种方法都使用谓词，而不是假设和承诺过程。它们适用于CSP过程中使用定理证明而不是模型检查的约束-承诺推理。另一个不同之处是，这些方法仅限于痕迹模型;我们的一些结果也适用于F和N，尽管它们的效用对于这些更丰富的模型尚不清楚Evans，Treharne和Schneider有一个分解规则，用于他们的CSP B架构，允许依赖/保证推理为组合系统建立一致性结果[12]。周朝晨有趣的是，研究得出最弱假设ASS的机会，而不是测试定理5.1是否适用于给定的ASS。Pasarea nuetal. [9]总结了使用SPIN和SMV模型检查器进行软件模型检查的假设保证方法的一些实现这些方法使用时序逻辑规范来捕获假设（LTL）和保证（LTL或ACTL）。7结论和今后的工作我们已经提出了一个简单的公式的约束-承诺性质的CSP使用细化，和一些定理，允许这样的约束-承诺性质的组合系统推导出从其组件的单独可证明的属性。出现在前件中的所有边条件和条件都可以表示为适合于使用FDR检查的形式的精化。此外，此类条件不涉及一个以上的RMBI组件，这有助于降低单个检查的复杂性“同态”定理似乎很有用，但它们有一些局限性：• 在这种情况下，由此产生的假设ASS过于强大，因为它可以限制共享事件，这使得它在现实环境136N. Moffat，M.Goldsmith/Electronic Notes in Theoretical Computer Science 185（2007）121↔这些事件应该被认为是内部事件 定理4.1未能充分利用承诺，这将允许一个较弱的总体假设。• 在这种情况下，所得到的假设ASS过于薄弱，需要严格的边条件来补偿中间事件上ASS、COM和COM之 间 的 对 应 性 损 失 。定理5.1非常接近于已建立的承诺理论，尽管它是在CSP细化风格的模型检查的上下文中表达的。未来的工作将探讨其应用到大的例子。目前的理论支持组成推理系统，可以建模为一个共享的并行组合的两个组件的过程。我们相信这是使用CSP的精化风格模型检查实现有效组合推理的重要一步，因为我们的经验是，许多系统可以以这种方式建模，并且在发生状态爆炸的情况下，它往往是由并行组合过程引起的。此外，经典的AC推理已经找到了应用，即使它只关注简单形式的并行和顺序组合。即便如此，将当前的理论扩展到其他CSP流程操作符的组合（包括顺序组合）可能是值得的;在这种情况下，包含前置和后置条件来解决状态问题似乎是明智的目前对二进制共享并行组成的限制似乎可以取消。 作为当前理论基础的同样的直觉也可以应用于具有许多以重复的字母并行方式组成的组件的系统（它使每个组件进程在其接口上与其他组件同步）。同时，多组分体系可以通过将当前理论以分层的方式连续应用于双组分体系来推理。未来的工作将发展的AC属性使用假设和承诺过程，这是非常不同的经典表达式作为一个历史变量和逻辑变量的谓词的表达指导确认与William Simmonds的早期讨论导致了AC特性的类似表述。我们收到了来自CliJones的有用的早期评论。我们也感谢匿名评论者的有益评论。引用[1] Chaochen，Z.，通信过程的最弱环境，见：NCC '82会议录[2] de Roever，W.- P.，F. de Boer，U. Hannemann，J. Hooman，Y. Lakhnech，M. Poel和J. Zwiers，[3] Formal Systems（Europe）Ltd，N. Moffat，M.Goldsmith/Electronic Notes in Theoretical Computer Science 185（2007）121137[4] 霍尔角A. R.，Communicating sequential processes，Communications of the ACM21（1978），pp. 666-677。[5] Kay，A.和J.N.。Reed，A rely and guarantee method for timed CSP：A specification and design of atelephone exchange，IEEE Trans.软件工程师19（1993），pp.625-639[6] Misra，J.和K. M. Chandy，过程网络的证明，IEEE软件工程学报7（1981），pp. 417-426[7] Mo Chaat ， N. 和 M. Goldsmith ， 通 过 CSP 的 假 设 - 承 诺 ， 技 术 报 告 QINETIQ/S DU/TIM/TR0601826，QinetiQ（2006），可从作者处获得。[8] Pandya，P. K.，关于分布式程序组合验证的验证-承诺框架的一些评论。，in：J. W. de Bakker，W. P. deRoever和G. Rozenberg，editors，REX Workshop，Lecture Notes in Computer Science430（1989），pp.622-640[9] Papouchespouchareanu，C. ，M. B.DWYER和DM。 许志华，软件模型检验的假设-保证与模型检验：比较案例研究，第六届国际模型检验研讨会，LNCS 1680（1999），pp. 168-183。URLhttp://pubs.doc.ic.ac.uk/model-checking-stubs/[10] Roscoe，A. W.，“The Theory and Practice of Concurrency,” Pren