服务兼容性检测：重写逻辑系统Maude实现的方式

理论计算机科学电子笔记255（2009）65-81www.elsevier.com/locate/entcs使用Maude检查协议兼容性FranciscoDura′n1MeriemOuederni2GwenSalau′n3部Ma'laga计算机科学大学Ma'laga，Spain摘要检查通过其行为接口访问的服务的兼容性是面向服务计算的一个关键问题，其目的是从现有的软件服务构建新的系统在本文中，我们考虑了一个模型的服务，它考虑到价值传递和不可观察的行动我们提出了一种方法来检查在一个统一的方式使用重写逻辑系统Maude的两个服务协议之间的几个兼容性概念特别是，我们用三个广泛使用的兼容性概念来说明我们的方法，即相反的行为，未指定的接收和无死锁。这些概念以及处理不可观察行为的几种策略已经正式化并完全实现为一个原型工具，该工具能够自动检测两个服务是否兼容，如果不兼容，则返回一个反例。关键词：符号转移系统，不可观测的行动，兼容性，莫德。1介绍基于组件的软件工程（CBSE）和面向服务的计算（SOC）的主要原则是在构建新系统时重用现有的软件组件或Web服务4，在这种情况下，必须避免互操作性问题，并且重用的服务必须与正在开发的系统中的其他服务相适应因此，兼容性检查是确保服务能否成功互操作的关键。然而，当服务模型考虑到交互协议时，验证兼容性特别困难，这对于避免一起执行一组服务时的错误行为或死锁情况1电子邮件：duran@lcc.uma.es2电子邮件：meriem@lcc.uma.es3电子邮件：salaun@lcc.uma.es4在本文的剩余部分中，我们将使用通用术语服务来指代软件组件和Web服务。1571-0661 © 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.10.02566F. Durán等人/理论计算机科学电子笔记255（2009）65基于服务接口的几种描述模型，已经提出了许多兼容性概念，例如[23，9，20，2]中的自动机，[4，10]中的π演算，[14，16，17]中的Petri网和[1，5]中的状态机。最这些方法的重点是一个独特的兼容性概念，对于特定的应用领域，参见例如[17]服务组合，[1，5，14]服务替换，[10]服务编排等。与现有工作相比，我们的建议的新贡献如下：（i）我们的模型考虑到账户价值传递以及不可观察或内部行为（τ行为），以及认为不同的策略来处理它们;（ii）我们提出了一个框架，其中几个概念的兼容性可以自动检查，这个框架可以扩展新的兼容性概念和新的策略来处理内部的行动。请注意，接口模型中的内部操作非常重要，因为从可观察的角度来看，某些服务可以兼容，但由于不受控制的内部行为，它们的执行我们的服务接口模型允许指定交互协议（消息及其应用顺序）。还考虑了价值传递和内部行动。我们的框架提供了一个统一和系统的方法来检查不同的兼容性概念，考虑不同的策略来处理内部行动。在这里，我们关注三个广泛使用的兼容性概念，即相反的行为[21]，未指定的接收[3，23]和无死锁[2]。但其他在我们的框架中已经有了一些概念，将来可以考虑更多的概念。此外，我们考虑了三种不同的τ处理策略，即Robin Milner在在80年代[21]，等价性检查的上下文，类似地，其他的也可以添加到框架中。请注意，考虑不同的策略是很重要的，因为每个策略都有意义，这取决于兼容性检查的目标。因此，例如，如果想要比较外部行为，跟踪策略非常适合，而弱策略允许在组合服务时检测一些细微的错误。当两个服务必须从内部和外部的角度完全匹配时，就需要一个强有力的战略，因为它是一个服务替代另一个服务的情况。我们的解决方案，检查协议兼容性是独立于任何特定的应用程序，因此可以是有用的几个问题，如自动服务组合，软件适配，服务替换，服务发现，代码重新设计等，我们的建议已实现在重写逻辑系统Maude [7]。其强大的重写引擎和搜索能力打开了非常广泛的可能性。此外，它的表达能力使我们能够在非常高的抽象层次上实现不同的概念和策略，而不会牺牲效率，并允许这样一个灵活和可扩展的通用框架。本文其余部分的结构如下。第2节正式确定了我们的服务模式。第三节介绍了本文中所使用的一些概念和兼容性的概念。在第4节中，我们将介绍如何使用Maude检查服务兼容性第5节与相关方法进行了最后，第六节得出了一些结论。F. Durán等人/理论计算机科学电子笔记255（2009）6567−−→bτJ（s−−→s）∈TS，E（TAU）一个！vJJa？XJ（s−→s）∈Tv=ev（v，E）（s−−→s）∈T（EM）（REC）一个！沃日是吗？XJs，EFig. 1.一个STS2服务模式我们假设服务接口都配备了签名（一组必需的和提供的操作）和由符号转换系统（STS）表示的协议。服务之间的通信使用与对应于操作调用的消息的发射和接收相关的事件来表示。事件可能带有一个参数列表，这些参数的类型与操作签名相关。在我们的模型中，标签是内部动作τ或元组（m，d，（p1，.，pn））其中，m是消息名称，d代表通信方向（发射！还是接待处？），和（p1，. ..定义2.1[STS]一个符号转换系统或STS是一元组（A，S，I，F，T）其中：A是对应于与转换相关联的标签集的字母表，S是状态集，I∈S是初始状态，F∈S是最终状态，T：S×A×S是转换函数。在本文的其余部分，我们使用元组（s，l，sJ）描述转换，使得s和sJ分别表示源状态和目标状态，l代表标签。我们的STS是在[15]中引入的STG（符号转换图）的简化版本。在此，防护被抽象为τ转变，其表示针对服务的内部（非服务性）活动。STS（−→b）的操作语义是：定义有三个规则（TAU，EM，REC，图1）。n（n>1）STSs（−→c）的操作语义是为了使用一个同步通信规则（COM，图2），其中值传递和变量替换依赖于后期绑定语义[19]，以及一个独立的进化规则（INE τ，图2）。 {作为1，. ，因为n}是一组对i，s，E由活动状态s∈S和数据环境E组成。数据环境是一组耦合，其中x是变量，v是基础值。我们使用一个函数类型，它返回变量或值的类型，我们定义环境更新Ex，vE（x）=v ev（E，x）E（x）ev（E，f（v1，. ，vn））f（ev（E，v1），. ，ev（E，vn））选择STS形式模型是因为它简单、图形化，并且可以很容易地从现有的实现平台的语言中派生出来68F. Durán等人/理论计算机科学电子笔记255（2009）65Jτ服务器登录？usr：string，pwd：用户S1S2searchFlight？dis：string，dep：tdate，登录！usr：string，搜索航班！dis：string，dep：tdate，searchFlight？dis：string，dep：tdate，u1u2S3搜索航班！Id：int，price：u3S4u4searchFlight？Id：int，searchCar？d1：date，d2：date，searchHotel？dep：tdate，ret：tdate，cat：stringS5u5搜索车！d1：date，d2：date，type：stringu6u7S9搜索车！id：intsearchHotel！searchHotel！dep：tdate，ret：tdate，cat：stringS6S10searchCar？ID：u8searchHotel？dep：tdate，ret：tdate，cat：stringsearchHotel？id：S7u9searchHotel！id：intS8一个！vi，j∈ {1.. n}iJJ是吗？XJsi，Ei sj，Ejtype（x）=type（v）EJ=Ej<$$>x，v<$（COM）一个！vJ J J{作为1，..，你好，我爱你，..sj，Ejasn}−→c{as1，.，你好，我爱你，..sj，Ej作为n}i∈ {1.. n}Jsi，Ei（INE）τJτ{作为1，..，你好，我爱你，..asn}−−→c{as1，.，你好，我爱你，..作为n}图二. n个STS的操作语义图3.第三章。用户和服务器行为接口阳离子、成分或适应目的）。由于篇幅的原因，在本文的其余部分，我们将只描述带有STS的服务接口。签名将保持隐式，但它们可以从STS标签中的参数类型（在这里显式）推断出来。Example. 我们使用一个旅行建议系统作为运行示例，该系统为旅行者提供信息。如图3所示，用户界面首先可以通过发送用户名和密码（login！）.然后，它可以请求（searchFlight！）和接收（searchFlight？）根据所希望的目的地和出发及返回日期的机票标识符和价格。根据其偏好（用户协议中τ转换指定的内部选择），用户可以开始一个新的预订请求，要求酒店建议（searchHotel！），以及然后它收到的答案（searchHotel？），或询问汽车建议（搜索汽车！），得到答案（searchCar？），然后开始酒店建议请求。服务器服务通过接收用户名和密码（登录？）. 接下来，该服务可以接收并回复若干个预订请求，直到接收并回复对汽车和/或酒店建议的请求。F. Durán等人/理论计算机科学电子笔记255（2009）65693服务协议兼容性我们从一些对服务协议兼容性的形式化有用的定义开始，我们将在3.4节中介绍这些定义。由于我们的模型考虑了τ动作，不同兼容性概念的定义取决于如何处理这些不可观察的动作在本文中，我们考虑了三种广泛使用的τ处理策略，即强、弱和迹[21]，检查这些策略中的每一个。此外，我们形式化的不同概念的协议兼容性使用的概念的全局可达状态集和转换兼容性。3.1预赛在本文中，我们专注于使用STSSTSi =（Ai，Si，Ii，Fi，Ti），i∈ {1， 2}描述的两个服务的情况。我们定义了一个函数outT（s），它返回从状态s出发的转移集T。最后，函数reachableT（s）和reachableT，l（s）分别返回从给定状态s可以到达的状态集合，以及使用转换集合T中标记为l的转换从给定状态s可以到达的状态集合：• 输出T（s）={（sJ，l，sJJ）|（SJ，l，SJJ）∈ T，s = SJ}• 可达T（s）={s1，.， sm}可达T（s1）可达. 可达T（sm），其中{s1，.， sm}={sJJ|（SJ，l，SJJ）∈ T，s = SJ}• 可达T，l（s）={s1，...， sm}可达T，l（s1）可达. 可达T，l（sm），其中{s1，.，sm}={sJJ|（SJ，LJ，SJJ）∈T，s = SJ，l = LJ}标签的比较对于检查交换的消息是否兼容非常有用。正式地，我们定义标签兼容性如下：定义3.1[标签兼容性]标签l1与标签l2兼容，如果：• l1=（m1，d1，（p11，. ，p1 n）），l2=（m2，d2，（p2 1，. ，p2 m）），使得m1= m2，d1=d2，n=m，并且nk= 1，.， ntype（p1 k）=type（p2 k）或，• l1=τ和l2=τ。在哪里！=？，？=！3.2继承国给定两个STS STSi=（Ai，Si，Ii，Fi，Ti），i ∈ {1，2}，我们将全局状态定义为一对状态（s1，s2），其中si是STSi的当前状态。然后，将针对所有全局可达状态检查协议兼容性因此，我们使用辅助函数后继TS（（s1，s2））和可达TS（（s1，s2）），它们分别提供在一个步骤中，从当前全局状态（s1，s2）可以到达的全局状态的集合，以及两个STS的所有全局可达状态的集合，其中TS代表所考虑的τ处理策略，即强、弱或跟踪等。注意，通过应用图2中给出的COM和INEτ规则来获得后继TS（（s1，s2））和可达TS（（s1，s2））集合。70F. Durán等人/理论计算机科学电子笔记255（2009）651122在我们的方法中，后继状态函数取决于处理τ作用的不同方式。在下文中，我们提出了强，弱和跟踪策略的后继状态函数。我们从定义强后继状态开始，其中从一个服务的状态出发的转换所持有的每个标签必须与从另一个服务的状态出发的转换所持有的标签匹配，即使是τ动作。定义3.2[强后继状态]强从当前全局状态（s1，s2）一步可达的定义如下：后继者强（（s1，s2））={（sJ，sJ）|（s1，l1，SJ）∈ T1，（s2，l2，SJ）∈ T2使得l11 2 1 22、兼容我们现在定义弱继承国。就τ作用量而言，我们要求每个τ作用量被零个或多个τ作用量匹配。定义3.3[弱后继状态]弱后继状态在一个步骤中，从当前全局状态状态（s1，s2）可达到的定义如下：子空间w∈k（（s1，s2））={（sJ，s J）|（s1，l1，SJ）∈T1，（s2，l2，SJ）∈T2，l1=/τsuch1 2 1 2L1和L2是兼容的}{（sJ，s2）|sJ∈reachableT，τ（s1），且reachableT，τ（sJ）=1 11 11n或n（SJ，l1，SJJ）∈T1使得l1/=τ}1 1{（s1，sJ）} |sJ∈ reachableT，τ（s2），且reachableT，τ（sJ）=2 22 2 2n ∈ T 2或n（SJ，l2，SJJ）∈T2使得l2/=τ}2 2后继状态的一个较弱的定义包括确定从当前状态可以到达的全局状态集，在一个步骤中，通过执行相同的跟踪。通过这样做，服务协议中不考虑τ定义3.4[跟踪后继状态]跟踪的全局状态集从当前全局状态（s1，s2）一步可达的定义如下：后继跟踪（（s1，s2））={（sJ，sJ）|（s1，l1，SJ）∈ T1，（s2，l2，SJ）∈ T2，l1τ和1 2 1 2L1和L2是兼容的}继承者跟踪（（sJJ，s2））（s1，τ，SJJ）∈T1∪（s2，τ，SJJ）∈T2后继跟踪（（s1，sJJ））Example. 我们专注于我们的运行示例的一小部分，以说明如何可以获得强，弱和跟踪策略的后继状态。让我们考虑全局状态（u1，s1）：强后继者（（u1，s1））=弱后继者（（u1，s1））=后继跟踪（（u1，s1））F. Durán等人/理论计算机科学电子笔记255（2009）6571={（u2，s2）}由于从u1和s1出发的转移不存在τ作用量，我们得到了根据任何τ策略从（u1，s1现在，让我们考虑全局状态（u4，s4）：后继者强（（u4，s4））=后继弱（（u4，s4））={（u2，s4），（u5，s4），（u7，s4）}后继跟踪（（u4，s4））={（u3，s3），（u6，s5），（u8，s9）}如图3所示，从u4出去的所有转换都保持τ个动作，即{（（u4，τ，u2）），（u4，τ，u5），（u4，τ，u7）}，而从s4出去的转换所保持的所有动作都与τ不同，即{ （ s4 ， searchFlight ？ dis ： string ， dep ： tdate ， ret ： tdate ， s3 ） ， （ s4 ，searchHotel？dep：tdate，ret：tdate，cat：string，s9），（s4，searchCar？d1：date，d2：date，type：string，s5）}。 通过应用强后继状态定义，u4处的τ动作与s4处的任何动作都不匹配，并且s4处的预期接收都不能在u4处发射。因此，不存在从（u4，s4）强可达的全局状态。考虑到弱后继状态的定义，状态u4处的τ动作被跳过，因为从该状态出去的所有转换都被标记为τ。因此，从（u4，s4）一步弱可达的全局状态集为{（u2，s4），（u5，s4），（u7，s4）}由于可达T用户，τ（u2）= π，可达T用户，τ（u5）= π和可达T用户，τ（u7）= τ.最后，在跟踪后继状态定义之后，如图3所示，全局状态集{（u3，s3），（u6，s5），（u8，s9）}可以在一个步骤中从（u4，s4）使用兼容标签的跟踪到达。为了获得从初始全局状态（s1，s2）开始的两个STS的所有全局可达状态的集合，我们给出以下定义：可达TS（（s1，s2））={（s1，s2）}可达TS（（sJ，sJ））1 2（SJ，SJ）∈successorsTS（（s1，s2））1 23.3转换兼容性作为后继状态，从全局状态（s1，s2）出去的转换的兼容性取决于如何处理τ动作转换兼容性在于检查在状态s1处发送的（相应地，接收的）消息是否可以被接收（相应地，发送），反之亦然。为此，我们从米尔纳[21]提出的等价概念中得到启发，提出了以下定义：定义3.5[强转换兼容性]给定一个全局状态（s1，s2），comp-em-recstrong （（s1，s2））=true i <$i <$i（si，li，sJ）∈Ti，其中i∈ {1，2}，<$i（sj，lj，sJ）∈I jTj，其中j=i mod 2 + 1，使得li和lj兼容。定义3.6[弱转换相容性]给定一个全局状态（s1，s2），comp-em -recweak（（s1，s2））=true i：72F. Durán等人/理论计算机科学电子笔记255（2009）65我• 其中i∈ {1，2}，li/=τ，<$（sj，lj，sJ）∈Tj，其中j=i mod2+ 1I j使得L1和L2是兼容，以及• 其中i∈ {1，2}，comp-em-recweak（（sJJ，sj））=true，并且我我其中j=i mod 2 + 1，comp-em-recweak（（si，SJJ））=true.J J定义3.7[跟踪转换兼容性]给定全局状态（s1，s2），comp-em -rectrace（（s1，s2））=true i {\displaystyle i}：• 其中i∈ {1，2}，li/=τ，<$（sj，lj，sJ）∈Tj，j=i mod2+ 1I j使得L1和L2是兼容，以及• <$（si，τ，sJJ）∈Ti，其中i ∈ {1，2}，n（s，l，sJ）∈我，我τ， 使得s∈可达T，τ（si）则<$（SJ，SJ）∈后继迹（（s1，s2））其中SJ= SJ.ii j iExample. 图4显示了我们正在运行的示例的一部分。考虑到全局状态（u4，s4），如果TS是强或弱，则com-em-recTS（（u4，s4））返回false，如果TS是trace，则返回true。由于在u4处（分别在s4处）存在与s4处（分别在u4处）的转换标签不匹配的转换标签，所以com-em-recstrong（（u4，s4））=false。通过应用弱转移相容性概念，com-em -recweak（（u4，s4））=true i：com-em -recweak（（u2，s4））=true和com-em-recweak（（u5，s4））=true和com-em-recweak（（u7，s4））=true。让我们把重点放在（u2，s4）上。转换标签（searchCar？d1：date，d2：date，type：string）与u2处的任何转换标签都不匹配，因此com-em-recweak（（u2，s4））=false。因此，com-em-recweak（（u4，s4））=false。最后，通过跳过在u4处保持τ动作的转换，我们总是有从（u4，s4）开始的兼容标签的踪迹。因此，com-em-rectrace（（u4，s4））=true。3.4规范一些服务兼容性概念服务兼容性的各种概念存在[4，17，14，1，5]，对服务如何兼容提出了不同的要求。没有标准的或唯一的服务兼容性概念，所有这些都适用于不同的应用程序域。为了说明的目的，我们在这里集中在三个广泛使用的概念，即相反的行为，未指定的接收和无死锁。相反的行为。最强烈和最直观的兼容性概念是相反的行为。在本文中，我们对相反行为相容性的定义受到Mil- ner最初提出的双相似性概念的启发[21]。这里，相反行为兼容性在于这样的事实，即当一个服务可以发送消息时，则另一个服务必须愿意接收该消息，并且当一个服务等待接收消息时，则另服务必须发送该消息。因此，对于任何τ处理策略TS，我们将相反行为相容性概念形式化如下：两个STSSTSi =（Ai，Si，Ii，Fi，Ti），i={ 1， 2}是相反的行为相容的，当且仅当对于每个全局状态（s1，s2）∈可达TS（（I1，I2））：F. Durán等人/理论计算机科学电子笔记255（2009）6573用户搜索航班！dis：string，dep：tdate，u2服务器searchFlight？dis：string，dep：tdate，u3S3u4u7s4searchHotel？dep：tdate，ret：tdate，category：stringu5搜索车！d1：日期，d2：日期，文字：字串searchCar？d1：date，d2：date，searchHotel！dep：tdate，ret：tdate，category：S5S9u8FIG。 四、StrongandWeakIncompatibleEmissionsReceptionsat（u4，s4）• comp-em-recTS （（s1，s2））=真，并且• 若s1∈F1（s2∈F2），则s2∈F2（s1∈F1）。Example. 考虑我们的运行示例，正如我们在前一节中所解释的，如果TS是强或弱，则com-em-recTS（（u4，s4））=false。然后，用户和服务器协议不是相对于强弱的战略。然而，这些协议是根据跟踪策略兼容的相反行为。对于用户和服务器协议，我们可以检查每个跟踪的全局可达状态（ui，sj），来自（u1，s1）com-em-rectrace（（ui，sj））=true。我们也可以很容易地检查在相反行为定义中给出的第二个条件。不确定的接待。有一个相容性概念比相反的行为限制性更小，那就是未指定的接受。在这里，我们的未指定接收定义接近于[3，23]中给出的定义，该定义认为两个服务协议是兼容的，即使一个服务可以接收另一个服务不能发送的消息，即。 额外的接待，这在两个方向上都有效。然而，这个定义要求，如果一个服务可以在可达状态下发送消息，那么该发送必须愿意被另一个服务接收。 通过这样做，也有可能一个协议持有一个发射，只要这个发射的状态在建立的交互期间是不可到达的，它的伙伴就不会接收到这个发射。两个STSSTSi=（Ai，Si，Ii，Fi，Ti），i∈ {1， 2}是非指定接收相容的当且仅当对于每个全局状态（s1，s2）∈可达TS（（I1，I2））：• comp-em-recTS（（s1，s2））=true，并且如果s1∈F1（分别为s2∈F2s2∈F2（分别为s1∈F1），或• 其中i={1，2}，li=（mi，？，pl），f ∈（sj，lj，sJ）∈Tj，其中j=I ji mod2 + 1，使得li和lj兼容。Example. 在我们的旅行建议运行示例中，根据强策略，用户和服务器协议是不兼容的未指定接收，因为在全局状态（u4，s4）处，在u4处存在与接收不同的转换标签（分别为s4），其与s4（分别为u4）处的转换标签不匹配。74F. Durán等人/理论计算机科学电子笔记255（2009）65用户服务器searchFlight？ dis：string，dep：tdate，u7S3searchHotel！dep：tdate，ret：tdate，category：u8searchCar？d1：date，d2：date，s4searchHotel？dep：tdate，ret：tdate，category：stringS5S9FIG。 五、Additio nlRe p e tio nsat（u4，s4）然而，这两个协议都是关于弱和跟踪策略兼容的未指定接收，因为对于所有全局可达状态（ui，sj），如果在ui（分别为sj）处存在不能与sj（分别为ui）处的转移标签匹配的转移标签l，则l是接收。例如，让我们来--图 5 中 的 全 局 可 达 状 态 （ u7 ， s4 ） 。 在 状 态 s4 ， 有 两 个 额 外 的 接 收 ， 即（ searchCar ？ d1 ： date ， d2 ： date ， type ： string ） 和 （ searchFlight ？ dis ：string，dep：tdate，ret：tdate），其与U7处的发射不匹配。僵局的自由。这个概念比前两个概念限制性更小。它认为两个服务协议是兼容的，当且仅当，从它们的初始状态开始为了形式化我们的无死锁兼容性，我们从[2]中获得灵感。两个STSSTSi =（Ai，Si，Ii，Fi，Ti），i={ 1， 2}是无死锁兼容的当且仅当对于每个全局状态（s1，s2）∈可达TS（（I1，I2））：• （s1，s2）∈（F1×F2），或• 后继者TS（（s1，s2））Example. 回到旅行建议系统，用户和服务器关于强策略是不兼容的，因为不存在来自（u4，s4）的全局强可达状态，并且u4和s4不是最终状态。 然而，尽管如此，这两个协议是无死锁兼容的，根据弱和跟踪策略，因为，从它们的初始状态开始，对于每个弱（或迹）全局reablestate（ui，si），sucsS（（ui，si））=/如果TS是弱或痕量，则不需要对一个finalglobalste进行加密。3.5兼容性检查现在，我们提出了一个协议兼容性定义UPC，用于使用STS描述的两个给定协议，兼容性概念CN和τ处理策略TS。这个定义使人们能够检查是否有两个服务协议，使用STS描述，是兼容的CN和TS，并报告一个反例CE，如果他们不是。F. Durán等人/理论计算机科学电子笔记255（2009）6575UPC：{STS1，STS2} ×CN×TS→布尔，CE><4编码到Maude和工具支持在本节中，我们分别简要介绍了Maude，兼容性检查框架的Maude编码，以及自动化兼容性验证的原型工具。4.1Maude概述Maude [6，8，7]是OBJ [13]代数规范家族中的一种高级语言和高性能解释器和编译器，支持成员资格等式逻辑和重写逻辑规范以及系统编程。因此，Maude将函数式编程的等式风格与重写逻辑计算相结合。在本节中，我们提供了一个非正式的描述，这些Maude特征是理解论文所必需的;感兴趣的读者可以参考[8，7]了解更多细节。Maude 这样的逻辑扩展了序排序的等式逻辑，并支持排序、子排序关系、子排序多态运算符重载以及具有等式定义域的部分函数的定义。在Maude中，有三种不同类型的模块：功能模块、系统模块和面向对象模块。我们在这里关注功能模块（更多信息请参见[8，7]）。例如，下面的Maude函数模块定义自然数（排序Nat为自然数，NzNat为非零自然数），使用Peano符号，具有零（0）和后继（s_）操作符作为构造函数（注意ctor属性）。然后，定义加法运算（_+_），它的行为由两个等式公理指定运算符s_和_+_使用mix fix语法定义（下划线表示参数的位置fmod MY-NAT是sortNzNatNat。NzNat< Nat. op 0：->Nat [ctor].op s_：Nat -> NzNat [ctor].op_+_：Nat Nat -> Nat [asphalt_id：0].varsMN：Nat.eqsM+sN=s（M+N）。endfm如果一个等式指定是连续的、终止的和排序递减的，那么它可以被执行。函数模块中的计算是通过使用方程作为从左到右的简化规则来完成的，直到达到规范形式。一些方程，比如表示二元算子的交换性的方程，不是终止的，但是它们通过算子属性来支持，因此Maude对这些属性提供的方程理论进行模简化，这些属性可以是结合的（asynchronous），交换性76F. Durán等人/理论计算机科学电子笔记255（2009）65见图6。Maude模（1）身份（id）。因此，上述性质必须在更一般的简化模这样的方程理论的背景下理解。在Maude中，规格可以是通用的，也就是说，它们可以与其他规格一起定义为参数。数据类型必须满足的要求由理论描述。参数化模块通过视图实例化。一个视图显示了一个特定的模块如何满足一个理论，通过将理论中的排序和操作映射到目标模块中的排序和操作，以这种方式，导出的公理在目标模块中可证明4.2莫德编码在本节中，我们将概述用于编码我们的方法的不同Maude模块（参见图6）：STS规范。一个名为STS的模块指定了服务模型。STS被表示为以下形式的对象：.STS对象有一个标识符（Oid），一个类型（STS）和一个属性集，该属性集由一个初始状态（is），一组最终状态（fss）和一组转换（ts）组成。转换是St 1-L-> St 2形式的元组，其中St 1和St 2分别是源和目标状态，L是标签。标签是τ（T）或M d（PRS）形式的元组，其中M是消息名称，d代表方向是？ 或者！PRS表示参数列表。Tau策略两个操作successors和comp-em-rec分别将后继TS和comp-em-recTS函数编码为三个Maude模块，分别称为STRONG、WEAK和TRACE。由于空间的原因，我们不能给出实现这些函数的所有Maude规范。例如，图7显示了successors跟踪函数的编码。successors操作从一个global开始探索两个STS对象（第1行中的第一个和第三个参数）。state（第1行中的第二个和第四个参数），以返回全局概念相反的行为STS使用战略强弱使用微量未指明的接待无死锁使用兼容性使用F. Durán等人/理论计算机科学电子笔记255（2009）65771234567891011121314151617181920212223242526272829图第七章跟踪策略下后继函数的模编码状态（Set{Pair{State，State}}），使用兼容标签的跟踪从当前状态一步可达。关于标签兼容性，在行8-9中的表达式St 1-Md1（PRS 1）->St 1'和St 2 -Md 2（PRS2）-> St 2'要求在St 1和St 2处的两个转换标签具有相同的名称和相反的方向然后，兼容参数（PRS1，PRS2）调用检查参数列表PRS1和PRS2是否具有相同的类型列表（相同顺序的相同类型）。兼容性概念。 第3.4节中提出的相反行为、未指定的接收和无死锁兼容性概念是指定的 成 三 操作 相反的行为，未指定的接待和无死锁性。 这些操作中的每一个都评估compat-关于τ策略，两个STS在所有可达全局状态下的最优解。例如，图8显示了相反行为兼容性观念在第一步中，opposite-behaviors操作（第1行）接受两个STS对象作为参数 ， 并 返 回 一 个 由 布 尔 值 和 反 例 组 成 的 元 组 （ Tuple{Bool ，Tuple{List{Transition}}）。 然后，为了使用递归执行在所有全局可达状态下检查协议兼容性，调用辅助相反行为操作（第8-10行）。如第13行所示，辅助相反行为操作调用针对每个全局可达状态（St1，St 2）的comp-em-rec操作。取决在返回的布尔值上，可以递归地调用（第14- 15行）SPS中每个全局状态的相反行为操作，即，可以从（St 1，St 2）到达的全局状态的集合。的情况中comp-em-rec操作返回false，辅助的get-counterexample操作返回一对从初始状态开始直到到达不兼容源的转换序列。如果当前全局opsu c c e s s s o r s：对象状态对象状态−>设置{对{状态，状态}}。CEQsuccess or rs（连续的，连续的<：st s|（ts：St1−M！（PRS1）−>St1TS）的情况下，ATS>，St1，<奥：国家统计局|（ts：St2−M？（PRS2）−>St2'，TS′），AtS'>，St2）=（，s u c e sso r s（，St1，<奥：国家统计局|ts：TS'，AtS'>，St2））I f兼容−参数（PRS 1，PRS 2）。CEQsuccess or rs（连续的，连续的<：st s|ts：（St1− M？（PRS1）−>St1TS）的情况下，ATS>，St1，<奥：国家统计局|ts：（St2−M！（PRS2）−>St2'，TS '），AtS'>，St2）=（，s u c e sso r s（，St1，<奥：国家统计局|ts：TS'，AtS'>，St2））I f兼容−参数（PRS 1，PRS 2）。EQs u cce sso r s（O<：s t s |ts：（St1- T-> St1ATS>，St1，<奥：国家统计局|ts：TS'，AtS'>，St2）=（success or rs（，St1<奥：国家统计局|ts：TS'，AtS'>，St2），success or rs（连续的，连续的<：st s|ts：TS、ATS>，St1，<奥：国家统计局|ts：TS'，AtS'>，St2））。EQs u cce sso r s（O<：s t s |ts：TS，ATS>，St1，<奥：国家统计局|ts：（St2−T−>St2'，TS '），AtS'>，St2）=（success or rs（，St1，<奥：国家统计局|ts：TS'，AtS' >，St2success or rs（连续的，连续的<：st s|ts：TS、ATS>，St1，<奥：国家统计局|ts：TS'，AtS'>，St2））。78F. Durán等人/理论计算机科学电子笔记255（2009）6512345678910111213141516171819见图8。相反行为概念可达状态（St1，St 2）之前已经被访问过（第17行），以避免在循环协议的情况下无限执行。兼容性检查。模块COMPATIBILITY{TSNOTION}实现兼容性定义。参数TSNOTION指的是一个兼容性概念（相反的行为，未指定的接收或无死锁），根据τ策略（强，弱或跟踪）作为参数编码到一个名为NOTION{STRATEGY}的4.3工具支持我们在前几节中介绍的兼容性检查框架已经完全实现为一个原型工具（参见图9的概述）。STS Maude规范是使用我们在Python中实现的脚本STS2Maude自动生成的。 为了检查协议的兼容性，我们调用Maude的red（uce）命令来执行所选择的兼容性概念（例如，相反的行为）和τ处理策略。返回一个布尔值和一个反例，指示是否根据检查的兼容性概念并分别识别不兼容源，两个STS是兼容的。到目前为止，我们的原型工具已经在超过75个示例上进行了验证，这些示例从小型示例到真实世界的示例都有。我们数据库中最大的例子由两个服务组成，每个服务都包含超过85个状态和大约90个转换。这个例子的最大计算时间大约是7秒，这是检查跟踪无死锁兼容性所需要的5相关工作在过去的25年里，兼容性作为软件工程的一个主要问题得到了广泛的研究。让我们调查一些关键的相关工作在这一领域。[3，23]使用基于自动机的形式主义正式定义了软件组件的兼容性概念它们的兼容性概念包括检查两个协议属性，即未指定的接收和死锁。最近，[1，5]op反对我们：对象Object −>Tuple{Bool，元组{List{Tr an siti on}}。op反 对 我们：对象对象设置{Pair {State，State}}设置{Pair{ State，State}}−>Tuple {Bool，元组{List {Tr an si t i on}}。EQopposi te − pouvi ours（，<奥：国家统计局|是：St2，AtS' >）=opposi te − pouvi ours（，<奥：国家统计局|是：St2，在S