基于减少虚假反例的组件协议一致性算法

理论计算机科学电子笔记263（2010）67-94www.elsevier.com/locate/entcs基于减少假否定的组件协议一致性AndreasBoth，WolfZimmermann和Ren′eFranke1哈雷大学计算机科学学院Halle（Saale），德国摘要在过去的几年中，许多工作考虑了组件的行为协议，并讨论了基于组件的系统中自动检查协议兼容性（协议一致性）的方法。这些方法通常是模型检测方法，即。例如，肯定回答保证所有执行的协议一致性，而否定回答提供可能导致协议违反的示例执行。事实证明，如果行为抽象考虑到无界并发和无界递归，协议一致性检查问题变得不可判定。有两种可能性来克服这个问题：（i）进一步的行为抽象到有限状态系统或（ii）协议一致性检查问题的保守近似。这两种方法都可能导致虚假的反例，即。例如，由于抽象或近似，所示的执行永远不会发生。这项工作考虑了第二种方法，并显示了一个算法，减少了虚假的反例的数量，通过削减o的搜索分支，绝对不包含真正的反例。关键词：验证，协议一致性，基于组件的系统，组件，模型检查，静态分析，过程重写系统1介绍如今，开发软件包含了大量重用以前开发的软件，称为组件。这些组件通常是由不同的开发人员、第三方公司在很久以前用不同的编程语言开发的，以二进制代码或分布式组件（例如，分布式组件）的形式提供。例如，在一个实施例中，web服务）。因此，人们对可以组成可靠系统的组件非常感兴趣创建可靠的有状态组件并不容易，因为开发人员必须防止和捕获每一个可能的错误，这些错误可能是由与该组件的不同交互顺序这一观察结果导致1电子邮件：{andreas.both，wolf.zimmermann，rene.franke}@ informatik.uni-halle.de1571-0661© 2010 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2010.05.00568A. Both等人理论计算机科学电子笔记263（2010）67仅对数据流和结果类型进行加密的计算被省略。相关程序点用pi标记。同步远程方法调用以阻塞方式执行，异步远程方法调用以非阻塞方式执行(b) 基于组件的应用PC0=nPC1=zpm（op|po）PC2=（a+b）(c) 图1b中组件的方案图1.一、具有三个接口和派生组件的示例在过去的几年里，许多关于行为协议或交互协议的工作。我们在这里讨论这些作品的分类。第6节包含更详细的讨论。在这项工作中，我们假设一个组件模型类似于UML组件模型。每个组件可能已经提供了接口（由组件提供的服务）和所需的接口（必须由其他组件提供的接口由一组服务组成，这些服务是过程或函数。一个过程可以同步实现，也可以异步实现。调用同步过程会阻塞调用方，直到被调用方完成该过程的执行如果已经调用了异步过程，则启动新图图1（a）和（b）示出了示例。A. Both等人理论计算机科学电子笔记263（2010）6769组件系统组合B1，...，Bn检查协议Ai好的还是反例抽象系统行为C1P1R1的1B1CiPiRiA我B我CnPnRnAnBn图例：CiPiRiAi组件名称提供的接口Ci所需的接口Ci协议CiBiCi的抽象行为图二. 自动协议一致性检查行为协议有两种基本方法：（1）第一种方法描述了组件的抽象行为模型，指定了对组件提供的接口的调用如何转换为对所需接口的调用。通常抽象行为被指定为CSP或CCS中的进程代数表达式（见e。例如，在一个实施例中，[33、31]）。根据此规范检查兼容性。(ii)第二种方法除了指定组件行为之外，还为每个有状态组件指定一个协议（参见e。例如，在一个实施例中，[30、21]）。该协议指定了对组件提供的接口的服务调用的合法序列。组件的行为用于确定对特定组件的服务调用的可能序列集。这两种方法都非常适合自动协议一致性检查，因为许多方法都限制在有限数量的状态。在这项工作中，我们考虑第二种方法，因为它明确规定了组件开发人员和组件用户的响应：组件用户必须遵守协议，而开发人员必须确保一些理想的属性（例如，如果遵守协议，组件不会中止）。 图1（c）示出了 一个协议被指定为正则表达式的例子。在这个例子中，C2的协议保证了在p16的除法永远不会失败. 如果调用它，b首先，它被零除而崩溃图2总结了自动协议检查的基本方法。每个组件都分别使用协议（由组件设计者提供）部署或发布，该协议指定对其提供的接口的服务调用的合法序列，以及（自动导出的）抽象组件行为，该抽象组件行为指定从对提供的接口的调用到对组件的所需接口的调用的转换。在构件系统中，抽象构件行为根据构件系统的体系结构组合成抽象系统行为此系统行为可用于检查组件系统中每个组件的协议一致性。在部署或发布组件之后，我们假设所提供和所需接口的签名、协议和抽象行为是组件唯一可用的信息特别是，组件用户可能无法使用源代码或二进制代码。因此，该方法还可以处理e。例如，在一个实施例中，Web服务。如果70A. Both等人理论计算机科学电子笔记263（2010）67如果发现协议违规，则提供了一个演示违规的示例（反例）。由于组件的抽象行为（以及系统行为）是一种抽象，因此它可以对执行路径进行建模，被处决在这种情况下，反例被称为假阴性。肯定的答案保证没有发生协议违反有两种基本方法可以确保抽象组件的行为。在自顶向下的方法中，组件开发人员指定抽象行为，然后对其进行细化（例如：例如，在一个实施例中，[33、31]）。自底向上的方法从源代码中确定抽象行为（例如，例如，在一个实施例中，[43，7]）。自上而下的方法的优点是可以在实现组件之前检查协议一致性，而自下而上的方法的优点是可以使用标准控制流程分析来机械化该方法。这项工作考虑自下而上的方法。协议一致性检查方法的能力取决于组件行为和协议的建模技术。虽然组件协议经常被建模为有限状态机（参见E。例如，在一个实施例中，[30]），行为可以被建模为有限状态转换器（e。例如，在一个实施例中，[21]），下推系统（e.例如，在一个实施例中，[43]，Petri nets（e.例如，在一个实施例中，[35]），过程代数表达式（e.例如，在一个实施例中， [33]有限状态方法只能对有界递归进行建模（i.例如，到一个cer-tain递归深度）和有限并发（e.例如，在一个实施例中，通过使用Shuange自动机）。Petri网能够模拟无限并行，但无法处理递归。下推系统可以模拟无约束递归，但不能模拟并发。无界递归和无界并发可以通过使用进程重写系统来充分建模[7，39]。不幸的是，协议一致性检查问题变得不可判定，因为LTL模型检查对于进程重写系统是不可判定的[29，7]。然而，可达性检查仍然是可判定的进程重写系统。有三种可能性来克服一般协议一致性检查的不可判定性：（i）进一步抽象到例如有限状态系统，（ii）有界检查（通过限制递归深度和数目的并发线程），（iii）近似的协议一致性检查。第一种和第三种可能性可能会导致更多的假阴性。第二种方法可能导致假阳性答案（在分别以比给定递归深度和并发度更大的递归深度或更大的并发度发生协议违反的情况下）。如[43]所示，（i）的天真实现可能会在递归回调的情况下导致误报，即使每个组件内部只包含非递归过程。因此，本研究考虑了第三种可能性。协议检验问题的近似解应该是保守的，即：例如， 如果近似没有发现协议违反，那么确实没有协议违反。然而，由于近似，协议违反的示例可能是假的。利用抽象系统行为和协议的信息，可以检测这样的反例是否是真实的反例（至少w。R. t.抽象系统行为）或不。对于后一种情况，人们可能A. Both等人理论计算机科学电子笔记263（2010）6771改进排除该反例的协议检查问题的近似，并继续搜索进一步的反例。这种后验方法类似于软件模型检查中的CEGAR循环。这项工作认为，作为一种替代的先验方法：在寻找反例 启发式算法在搜索树中切割不排除实负数的分支w.r.t.抽象系统行为（分支可能包含实负数，但这些也包含在其他分支本文的结构如下。第2节介绍了过程重写系统如何用于抽象。第3节介绍了近似协议一致性检查的方法，分析了产生伪反例的原因，第4节介绍了如何使用特殊的搜索策略来避免这些伪反例。第5节显示了一个案例研究的结果。最后，本文对第六节的相关工作进行了总结，并给出了结论第七节未来的工作2递归和并发本节总结了[7]中的结果，并解释了为什么这些技术工作得很好。特别是，我们提出了一个基于进程重写系统的抽象执行模型[29]，用于潜在递归程序的并发执行，并鼓励它们的使用。然后，它示出了如何抽象的组件被-重写器可以被建模为过程重写系统，以及如何将这些粘在一起，以获得一个抽象的系统行为。最后，我们表明，特殊情况下，导致从文献中已知的组件模型众所周知，命令式编程语言的状态包含一个堆栈来表示当前过程调用层次结构。一个堆栈只需要 如果编程语言允许递归过程。通常堆栈帧的数量是无限的。如果这些被抽象为一个有限数，抽象模型就变成了下推自动机（如果允许递归过程）或有限状态机（如果禁止递归过程）。这些方法被用于软件模型检测，因为可达性，LTL和CTL模型检测是可判定的用于捕获无界递归和无界并发的自然执行模型使用表示为仙人掌堆栈（堆栈树）的状态。这个模型是由[17]提出的。图3示出了组件系统的示例执行。堆栈帧包含指向接下来要执行的语句的程序指针。程序点PJ2和PJ3分别表示主程序中在调用a和b如果执行进程中的过程调用，则将堆栈帧压入堆栈。如果一个新的并行进程启动，一个新的堆栈会为这个进程增长（就像在一个saguaro堆栈中）。如果cactus堆栈中的一个堆栈只包含一个堆栈帧，则只能在这些堆栈中的两个顶级元素之间执行同步。因此，执行将cactus堆栈转换为cactus堆栈。在Cactus stacks和process-algebraic之间有一种自然的对应关系72A. Both等人理论计算机科学电子笔记263（2010）67第二p13p3p26λ||||||n||32λ3232O32p32λ323λλ23λ2λ3λp2p6p17p13p3p6p17p23p2p24p3mainpardocall a调用zexec p21呼叫我调用bexec p12呼叫我exec p15呼叫;召唤exec p15呼叫;召唤p6p18p10p10exec p24execp25exec p6呼叫我exec p6呼叫O呼叫P调用b返回exec p24(a) 崩溃计算p15第二十三页p5p14p5p4p3p24p2p3p26p2p2p3p2第二p3p24p2第二p3p24p2p3p24 p11p3p24 p17第二十三页p11p3p24调用bexec p15返回execp11返回返回执行程序p24p25返回同步呼叫P返回返回(b) 终止计算图三. 图1中组件系统的示例执行p1λp3||p2和p3||p2 0.pJzp3||（第11页）||p2 1）.pJ<$λp3||（第11页）||p2 2）.pJmp3||（第11页）||p15.p23）.PJ2bJ JλJ2JmJ2J2λp2 4.p3||（第11页）||p15.p2 3）.p2p2 4.p3||（第12页）||p15.p2 3）.p2p2 4.p3||（第15页，第13页||p15.p2 3）.p24.pJ||（第16页，第13页||p1 5.p2 3）.pJnp2 4.pJ||（第6页、第1页、第13页||p1 5.p2 3）.pJ<$λp2 4.pJ||（第6页、第1页、第13页||p16.p2 3）.PJλp2 4.pJ3||（第6页、第1页、第13页||p6.p1 7.p2 3）.PJ2<$λp2 5.PJ3||（第6页、第1页、第13页||p6.p1 7.p2 3）.PJ2p26.PJ3||（第6页、第1页、第13页||p6.p1 7.p2 3）.PJ2p2 6.PJ3||（第6页、第1页、第13页||p7.p1 7.p2 3）.PJ22002年2月6日||（第6页、第1页、第13页||p1 5.p1 0.p1 7.p2 3）.pJ<$λp2 6.pJ||（第8页，第1页，第13页||p15.p10.p17.p23）.PJ2.pj3||（（第18页||第9页）。第1 7页。第13页||p15.p10.p17.p23）. pj 2.PJ2.PJ2.pj 6.PJ3||（（第18页||p14.p10）.p17.p13||p15.p10.p17.p23）.PJ2λp2 6.pJ3||（第24页）||第十九页||p14.p10）.p17.p13||p15.p10.p17.p23）.PJ2j3||（第24页）||第十九页||p14.p10）.p17.p13||p15.p10.p17.p23）.PJ2(a) 崩溃计算（cf. 图3a）198年bp2 4.pJ||（第11页）||p1 5.p2 3）.pJ<$λp2 4.pJ||（第11页）||p1 7.p2 3）.pJ<$λp2 4.pJ||（第11页）||p2 3）.pJ<$λp2 4.pJ||（第13页）||p2 3）.pJλp2 4.pJ3||（ε||p2 3）.pJ2=p2 4.pJ3||p2 3.pJ2p2 4.pJ3||pj2pj2PJ3||pj2pj2 6.PJ3||pJ2pJ3||pJ2p4p1 p5500万美元(b) 终止计算（参见 图3b）图四、作为对应于图1中的执行的进程重写的示例执行3表情设Q是原子进程的有限集合（在我们的例子中是程序点的集合）。Q上的过程代数表达式归纳定义如下：i. 任何q∈Q是一个过程代数表达式，空过程ε是一个过程代数表达式（其中ε∈/Q）。ii.如果q1和q2是过程代数表达式，则q1q2（并行合成）和q1.q2（顺序合成）是过程代数表达式。空过程ε是恒等式w。R. t. binary operator的 和. 这两个二元算子都是结合的，并p2p20p3p2p3p13p3p26p2p17第二十三页p6p17p24p24p18第十九页第十九页p17pp17pp17pp10101013p13p13p3p26p3p26p3p26p2p17第二十三页p15p10第十p2p17第二十三页p15p10第十p2p17第二十三页p15p10第十p3p2p3p115页13页p6p17p13p21p11p11p3p25p3p24p3p24p3p24p11p11p6p17p13p15第二十三页p15第二十三页p15第二十三页p15第二十三页p6p17p13p9p17p13p15p17第二十三页p15p17第二十三页p6p17第二十三页A. Both等人理论计算机科学电子笔记263（2010）6773且算子是交换的。为了避免括号，我们假设运算符。优先级高于。仙人掌堆栈中的堆栈由顺序组合表示仙人掌的分枝74A. Both等人理论计算机科学电子笔记263（2010）67||||∈⇒⇒⇒⇒--⇒堆栈由并行组合表示。 图4显示过程-代数表达式表示图中的仙人掌茎。3.第三章。Thederivationq1acactusstackq2succeedsq1andpro cactusawascalledandq1<$λq2表示问2：没有过程调用发生。请注意，并非所有进程代数表达式都对应于cactus堆栈。例如，表达式p1。（p2p3）不能对应于仙人掌堆栈，因为p2p3将表示仙人掌堆栈中的两个分支，因此不清楚将p1放在仙人掌堆栈中的何处如果只考虑程序点，则抽象状态对应于程序点上的进程代数表达式，并且抽象执行是进程代数表达式的序列。抽象状态转换将进程代数表达式重写为进程代数表达式。流程重写系统（PRS）[29]是一种描述这种转换的技术。 设PEX（Q）是有限原子过程集Q上的过程代数表达式集。一个过程重写系统是一个元组n=n （Q，n， I，→， F），其中Q是原子过程的有限集合，n是作用上的有限字母表，I∈Q是初始过程，→ nPEX（Q）×（n）{λ}）×PEX（Q）是一组过程重写规则，F∈EX（Q）是一个有限的最终过程集，λ∈/λ（无关互动或空字）。流程重写规则定义了一个派生关系通过以下推理规则（a∈N，x∈ N），可以得到N ∈PEX（Q）×N∈PEX（t1→at2）本发明公开了一种复合材料，t1at2本发明公开了一种复合材料，t1at2本发明公开了一种复合材料，t1at2一t1xt2t2at3xat1t2t1.t3t2.t3t1||t3t2||t3t3||t1t3||t2t1=t3集合L（f）=f{w：f∈F|Iwf}是一种被语言所接受的语言。在我们的例子中，Q对应于程序点的集合，而C对应于接口中过程名的表1显示了如何从程序中导出一组重写规则它假设所有的程序点都是显式的2。调用顺序过程继续进行，并将过程的第一个程序点的新元素推入堆栈相反，异步过程调用派生一个新的并行进程。过程返回只是将一个进程重写为空进程。此外，在我们的例子中，我们只考虑F=ε，因为执行通常以空的cactus堆栈终止。仔细观察派生规则可以发现，它们精确地形式化了抽象执行模型：定义的第二条规则形式化了转换仅应用于仙人掌堆栈顶部的元素。第三和第四条规则指定可以考虑仙人掌堆栈中的任何堆栈（即。例如，可以选择当前正在执行的每个进程进行状态转换）。因此，这两个规则模型交错语义。如果所有组件都被认为是白盒组件，那么通过表1中的转换获得的PRS会产生一个定义抽象系统行为的PRS。图5示出了图1中的基于组件的系统的抽象系统行为的重写规则。图4中的推导可以用图5的PRS构造。2这在每一个编译器中都是如此、A. Both等人理论计算机科学电子笔记263（2010）6775{p→p：p∈N<$p：whilen=p：s）}1 12Aoidm（· · ·）s）As）（Ⅲ）（）（）（）（Ⅲ）A：返回）{p→ε}）m（2）（2）λ一λBA<$p1：ifnthenp2：s）A<$s）<${p1→p2} <${p1<$krelλ→p3：p3∈N<$p1：ifnthenp2：s）}||λλA<$p1：ifnthenp2：s2elsep3：s3）A<$s1）nA<$s2）n{p1→p2，p1→p3}p1：pardop2：s2;PJ||p3：s3;PJ）A<$s2）λA<$s3）λ{p1→λp2||p3}λλMλA分1;s2）A分1）A分2）λA<$p1：当p2：s）A<$s）<${p1→p2} <${p→p1：p∈L<$s）}<$λ2 3{pJ||pj→λp4：p4∈N<$p1：pardop2：s2;PJ||p3：s3;PJ）}2 3 2 3A jJp：m（）{p→first（m）.p：p∈ Np：m（）} 如果m是同步的A p：m（）{p → first（m）||pJ：pJ∈ N p：m（）}如果m是异步的Ap：s{p→λpJ：pJ∈Np：s}，如果s是原子的，并且没有伪随机调用或返回程序1;程序2Aproc1Aproc2项目点在报表上注明Ls表示语句序列s中最后一个程序点的集合Ns表示语句s之后的程序点的集合first（m）是过程m的第一个程序点。表1处理重写系统主p→p|| p，p→p.PJ，p→ p|| pJ,PJ||pJ→λp， pp p.p，p→ε1 3 2220232433 24p4→14 5 5np6→λp7，p6→λp8，p7→mp15，p10，p8→op18||p9，p9→p14，p10，p10→λεzp11→λp12，p11→λp13，p12→mp15，p13，p13→λεpp14→λεmp15→λp16，p15→λp17，p16→np6，p17，p17→λεop18→bp24||p19，p19→λεap20→zp11||p21，p21→λp2 2，p22→mp15，p2 2，p23→λεbp24→λp2 5，p25→λp2 6，p26→λε图五、图1中组件系统的抽象系统行为（作为进程重写系统）1注：从表1中可以看出，进程重写规则在其LHS上至多包含并行运算符，RHS是至多包含并行运算符或顺序运算符的进程代数表达式。在[29]中，这种限制被称为进程代数网（PAN）。它可以处理无限的重复- 和无限并行性，包括同步。 这项工作使用PAN作为抽象系统行为的表示（以及组件的抽象行为）。 Mayr在[29]中表明，任何PRS的规则都可以转换为一个正常的形式，我。例如， LHS和RHS具有q1、q1、q2或q1q2的形式之一，其中q1和q2是原子过程。 因此，我们隐含地假设PRS是标准形式。□注：有限状态自动机由PRS的特殊类表示，其中 进程重写规则仅将原子进程重写为原子进程。下推自动机用PRS类表示，它不允许并行操作. 流程重写规则的LHS仅由以下部分组成的特殊情况原子过程是足够的。 相反，Petri网由类表示的PRS，它不允许顺序运算符。因此，PRS允许使用这两个操作符统一的下推自动机和Petri网的行为抽象组件行为基本上可以类似于抽象系统行为从其实现中导出。唯一不同的是待遇-76A. Both等人理论计算机科学电子笔记263（2010）67λ一→λ→m∈B→0∈1322I2，a2333244→I1，p5567λ687I1，m108I1，o99→I1，p1010λ一2bλMλBC：主P→p || p , p → q.pJ, p→qλ λm|| pJ→ Λ P，p||pJ→λp,ppq.p，p→λελopn p →p，p→p，p → q.p，p→ q||p，pq.p，p→εC1：zp11→p12，p11→λp13，p12→mql，m.p13，p13→λε1pp14λελ λ n λmp15→bp16，p15→p17，p16→qI0，n.p17，p17→εop18→q||p19，p19→ εC2：ap20→λqI1，z||p21，p21→p2 2，p22→qI1，m.p22，p23→εbp24→p2 5，p25→λp2 6，p26→λε图第六章图1中组件系统的抽象系统行为（作为进程重写系统）1组件所需接口的服务调用的部分在将组件C的所需接口连接到另一组件CJ的所提供接口之前，不存在已知的程序点。对于组件C的单独考虑，我们为C的所需接口I的每个服务m使用虚拟程序点qI，m。 在与组分CJ、qI的提供的界面I组合之后，m是由分量C j的第一个程序点firstCJ（m）代替。因此，组件C的抽象行为可以建模为元组BC（P，R，QC，firstC，→），其中P和R是C的提供接口，R是C的所需接口的集合，firstC：PQC是一个映射，指定C中的第一个程序点，本服务及 是字母表P上的进程重写规则的有限集合IRI和原子过程QqI，m：IR，mI. 图6示出了 抽象图中组件的组件行为1.一、流程重写规则类似于图1中的流程重写规则 5：如果qI0，n被替换yp6=第一C0（n），qI1，z被替换yp11=第一C1（z），qI1，p被替换yp14=第一C1（p），qI1，m被替换yp15=第一C1（m），qI1，o被替换byp18=第一个C1（o），qI2，a被yp20=第一个C2（a）取代，dqI2，b被y取代p24=第一个C2（b），然后图2中的抽象系统行为。5已获得。上面的替换是根据图1中的架构定义的：如果C的所需接口I是由C j的所提供接口I限定的，则组件C的抽象行为中的每个qI，m都被第一个CJ（m）替换。因此，如果部署的组件发布其抽象组件行为，所有信息可供获取组件系统作为进程重写系统的抽象系统行为因此，抽象的组件行为可以通过一组流程重写规则来建模。可以从组件的源代码中自动导出它们。对于一个基于构件的系统S，可以按照体系结构将其构件的抽象行为组合起来，从而得到S的抽象系统行为。此步骤只需要组件的抽象行为，但不需要它们的实现。由于有限状态机、下推机和Petri网是进程重写系统的特殊情况，因此可以对基于有限转换器、下推系统或Petri网的先前方法以及进程重写系统进行建模在[29]中，显示可达性问题（因此，单词prob），lem）对于一般PRS是可判定，LTL模型检查对于仅使用顺序运算符或仅使用并行运算符的PRS是可判定的，而LTL模型检查对于使用并行运算符以及顺序运算符的PRS变得不可判定。对可判定性的限制对应于推-一2bA. Both等人理论计算机科学电子笔记263（2010）6777|⊆∈⊆下系统（仅顺序运算符）和Petri网（仅并行运算符）。3协议一致性检查组件协议（简称：协议）描述了所有可调用操作的允许使用（参见：接口）的单个组件。它指定了允许的对组件的传入调用序列，因此表示仅基于接口描述的合约在其他应用范围中，协议可以用于避免未捕获的异常（参见。[7]）在执行组件期间或遵守业务规则（参见[6，8]）例如，SSO组件3可以执行以下服务：注册和登录（服务a）、登录（b）、可选地改变密码（c）、注销（d）。 该组件可以具有以下协议（业务规则）被公式化为正则表达式：（（a b）cd）。 必须遵守由组件的每个调用者协议可以通过执行转换来动态验证，（传入的远程调用）。 在这项工作中，我们专注于静态验证的协议，即。例如，在执行基于组件的系统之前，验证组件是根据其协议来使用的。根据其他作品[43，36，20]，协议由有限状态机（简称：FSM）定义：组件C的协议PC是FSMPC=（QPC，PC，→PC，IPC，FPC），其中QPC 是一组有限的状态， 是服务的有限集合，→PC<$QPC× <$PC×QPC是转移规则的有限集合，IPC QPC是初始状态，FPC QPC是最终状态的集合。 图1显示了实现不同接口的组件系统的示例。组件的协议显示为正则表达式（相当于FSM）。我们将只考虑组件C24的协议.例如，如果使用序列ab b调用该组件，则该组件可能会在被零除异常时崩溃。 如果协议（a+b）是有效的，则可以避免这种崩溃。设RNS是组件系统S（指定为PRS）的抽象行为，C是S的组件，协议为PC。对组件C的调用可以从抽象系统行为λS中获得，方法是用λ替换除C提供接口的服务之外的所有动作。这种PRS称为组件C的使用。因此，协议一致性检查等价于检查L（PNS，C）L（PC），其中L（PC）是由组件C的协议PC定义的正则语言。表2总结了本文的注释。图7示出了用于图1中的示例的部件C2的使用。图7（b）显示abb是违反C2协议的用法.该推导对应于图1中的示例执行3（a）和图。4（a）分别。使用并行和顺序运算符的PRS下LTL模型检查的不可判定性[29]意味着协议一致性检查变得3单点登录。一个提供登录/注销/会话管理功能的组件，因此不同的应用程序可以使用此机制来验证用户。4所有其他协议都可以使用类似的方法进行检查78A. Both等人理论计算机科学电子笔记263（2010）67λλλ2λ332λλSSS主p1→λp3||p2，p2→ap20.PJ，p3→bp24||pJ，pJ||pj→λp4，p4→λp14，p5，p5→λεnp6→λp7，p6→p8，p7→p15，p10，p8→p18λ||p9，p9→p14，p10，p10→εzp11→p12，p11→ λ p13，p12 → λ p15，p13，p13 → εzp11 →p12，p11→λp13，p12→ λp15pp14→λεmp15→λp16，p15→λp17，p16→λp6，p17，p17→λεop18→bp24||p19，p19→λεap20→λp11||p21，p21→λp2 2，p22→λp1 5，p2 2，p23→λεbp24→λp25，p25→λp26，p26→λε图第七章组分C2在图1的实施例中的用途1符号描述PC组件C的协议（表示为FSM或正则表达式）公司简介完全组件系统的抽象系统行为卡斯角抽象系统行为，只考虑组件C的交互CQCS组件C的组合抽象PEX（Q）用Q可计算的一组过程代数表达式s和t过程代数项s，t∈PEX（Q）v（反向）协议的状态，v∈PCa，b，λ在所考虑的系统中，a，b∈λ，无相互作用λ∈/λ，w，x，y相互作用序列，w，x，y∈θλ相互作用的空序列p，ε原子过程（p∈Q），空过程（ε∈Q）表2本文中使用的符号不可判定[7]，前提是使用的组件包含并行和顺序运算符。然而，可达性仍然是可判定的[29]。 解决协议一致性检查的不可判定性问题有以下几种方法：（i）有界协议一致性检查限制递归深度和并行度，（ii）进一步近似抽象组件行为和抽象系统行为，（iii）用可达性问题近似协议一致性检查问题。第一种选择通常被用作使用有限状态系统来建模抽象组件行为的论据。虽然它很可能会发现协议违反有界approach，误报不排除，因为协议可能会违反使用一个更大的递归深度或一个更大的程度的并行性比给定的界限。乍一看，第二种方法似乎很有希望。然而，[43]显示了一个具有两个组件的（顺序）组件系统的示例，两者都具有作为抽象行为的有限状态转换器，但协议一致性检查由于递归回调而导致误报。此外，它更有可能发现没有组件实现就无法发现的假阴性。因此，我们考虑第三种方法，因为这至少允许在抽象系统行为的层面上检查反例是真实的还是虚假的。近似协议一致性检查的基本思想是构造一个PRS_C，使得L（P_C）<$L（P_C）<$L（P_S，C）.因此，CQC包含所有序列A. Both等人理论计算机科学电子笔记263（2010）6779CC1λ1λ1λCεS/RSSRCCEURREURRPFork EURREURREURRRWSSSCCSeqSeqPForkPForkPSyncCSeqPForkPSyncCPSyncR1={（v，p，vJJ）−→a（vJ， pJ，vJJ）：（v→aPvJ）（p→aS、CPJ）}Rλ={（v，p，vJ）→λ（v，pJ，vJ）：（p→λ S、CPJ）}R序列 ={（v，p，vJJJ）−→a（vJ， pJ，vJ J）。（vJJ， pJJ，vJJJ）：（v→aPvJ）（p→aS、CPJ.PJJ）}R序列 ={（v，p，vJ J）→λ（v，pJ，vJ）。（vJ， pJJ，vJJ）：（p→λS、CPJ.PJJ）}RPFork ={（v，p，vJJ）−→a（vJ， pJ，vJ J）||（vJ， pJ J，vJJ）：（v→aPvJ）（p→aS、CPJ||PJ J）}RPFork ={（v，p，vJ）→λ（v，pJ，vJ）||（v，pJ J，vJ）：（p→λS、CPJ||PJ J）}RPSync ={（v，p，vJ J）||（v，pJ，vJ J）−→a（vJ， pJJ，vJJ）：（v→aPvJ）（p||pJ→aS、CPJJ）}RPSync ={（v，p，vJ）||（v，pJ，vJ）→λ（v，pJ J，vJ）：（p||pJ→λΠS、CPJJ）}R0={（v，p，vJJ）→λ（vJ， p，vJJ）：（v→aPvJ）}R={（v，ε，v）→λεJJJJJJJJJ}v，v，v，v∈QA;p，p，p∈QS;a∈PC见图8。 创建组合抽象的规则。由一个组件C的协议PC禁止的交互的5个（即，例如，PC），并存在于程序S中。由于可达性对于PRS是可判定的，因此可以判定L（λC） 是否=λ。 因此，L（PC）=P，意味着L（PS，C）<$L（PC）.此外，反例w L（PC）是伪的，即w L（PC）L（S，C）.由于单词问题是一个特殊的可达性问题，因此可以判定反例是否是虚假的。跃迁规则→ →<$C=R1<$Rλ<$R1λAIR1λ1000万美元λPSync 组合抽象法的<$R0<$Rε是通过使用在Fig. 八、 所有的过程常数都是三元组（vi，pk，vj），其中vi，vj∈QPC且pk∈QS. 一个三元组（vi，pk，vj）表示pk应重写的情况到empty过程，而FSMPC的状态vi被变换为vj接受相同的命令w：viwPvj. 一个常数t（vj，ε，vj）等于空字，因为已达到目标协议状态，且过程常量已被删除（cf。图8中的ε）。联合提取装置的建造技术细节 可以在[7]中找到。 综合抽象 是一S SPRS层级的同一类中的PRS（参见”[29]如《说文》。组合抽象的构造类似于PDA接受的语言与FSM接受的语言（参见[23]）：这产生了由规则R1组成的PDAλ1SeqλSeq Rε。的规则R1λPFork1PSyncλPSync 是对的方法[23]。规则 0 需要进一步的解释。考虑 例如 在图9（a）中。图9（b）示出了组合抽象。的集R1， Rλ、Rλ、R1和Rλ都是空的。为了检查无论是否达到不期望的状态V3，检查是否存在是组合抽象中的导数（v0，p0，v3）ε图9（c）示出了CCCC80A. Both等人理论计算机科学电子笔记263（2010）67RR不使用0-规则就没有这样的推导在组合抽象中，除了0-规则之外，没有任何规则可以分别应用于最后一个过程-代数表达式。因此，这两个推导不能继续。导子CJ0 cJ1在某种意义上是有代表性的，因为每一个5这些序列由反向协议表示，即。例如，反向FSMPC接受补数L（PC）=补数L（PC）。A. Both等人理论计算机科学电子笔记263（2010）6781RRλλBλλR||||||||||CRBB0λλλBλλλp0→ap2||p1，p1→bp5.p3，p2→λε，p2→bp5.p4，p2→bp5.p2，p3→λε，p4→λε，p5→λε(a) 具有禁止交互序列的抽象系统行为和（反向）协议Rλ={（vi，p3，vj）→λ（vi，ε，vj），（vi，p4，vj）→λ（vi，ε，vj），（vi，p5，vj）→λ（vi，ε，vj）：0≤i，j≤3，}1Seq1PFork={（v1，p1，vj）→a（v2，p5，vk）. （vk，p3，vj），（v1，p2，vj）→（v2，p5，vk）. （vk，p4，vj）：0≤j，k≤3}={（v0，p0，vj）→（v1，p1，vj）||（v1，p2，vj）：0≤j≤3}Rε= {（vi，ε，vi）→ε：0 ≤i ≤3}R0={（v0，pi，vj）→λ（v1，pi，vj），（v1，pi，vj）→λ（v2，pi，vj），（v2，pi，vj）→λ（v3，pi，vj）：0≤i≤5，0≤j≤3}(b) 组合抽象cJ：（v0，p0，v3）a（v1，p2，v3）||（v1，p2，v3）b（v1，p2，v3）||（v2，p5，v2）。（v2，p4，v3）b（v1，p2，v3）||（v2，ε，v2）. （v2，p4，v3）<$λ（v1，p2，v3）||（v2，p4，v3）（v1，p2，v3）||（v2，ε，v3）λ（v2，p5，v2）. （v2，p3，v3）||（v2，ε，v3）<$（v2，ε，v2）. （v2，p3，v3）||（v2，ε，v3）阿格拉（v2，p3，v3）||（v2，ε，v3）<$b（v2，ε，v3）||（v2，ε，v3）cJ1：（v0，p0，v3）<$λ（v1，p2，v3）||（v1，p2，v3）（v1，p2，v3）||（v2，p5，v3）。（v3，p4，v3）λ（v1，p2，v3）||（v2，ε，v3）. （v3，p4，v3）（v2，p5，v3）. （v3，p3，v3）||（v2，ε，v3）. （v3，p4，v3）ε（v2，ε，v3）. （v3，p3，v3）||（v2，ε，v3）. （v3，p4，v3）(c) 如果规则R0将被省略，则组合抽象中的派生抽象系统行为返回返回 返回返回议定书(d) 方案违背（v0，p0，v3）a（v1，p2，v3）||（v1，p2，v3）b（v1，p2，v3）||（v2，p5，v3）。（v3，p4，v3）<$λ（v2，p2，v3）||（v2，p5，v3）。（v3，p4，v3）λ（v3，p5，v3）. （v3，p3，v3）||（v2，p5，v3）。（v3，p4，v3）（v3，p5，v3）. （v3，p3，v3）||（v3，p5，v3）。（v3，p4，v3）λ（v3，p5，v3）. （v3，p3，v3）||（v3，ε，v3）. （v3，p4，v3）（v3，p5，v3）. （v3，p3，v3）||（v3，p4，v3）λλ（v3，p5，v3）. （v3，p3，v3）||（v3，ε，v3）<$（v3，p5，v3）. （v3，p3，v3）