软件体系结构描述语言的重写语义及CBabel工具——一种形式化验证软件架构设计的方法

理论计算机科学电子笔记130（2005）345-377www.elsevier.com/locate/entcs软件体系结构描述语言的重写语义亚历山大·拉德梅克2InsttutodeComputacooooUniversidade FederalFluminenseNiteroi，Brazil布拉加3InsttutodeComputacooooUniversidade FederalFluminenseNiteroi，BrazilAlexandre Sztajnberg1InstitutodeMatem′aticaeEstat′sticaUniversidade do Estado do Rio de Janeiro里约热内卢，巴西摘要分布式和并发应用程序总是有协调需求。这些应用程序的设计，由几个（可能是分布式的）组件组成，必须考虑协调要求，包括组件间的交互风格，组件内的并发性和同步方面。在我们的方法中，协调方面在软件架构级别进行处理，并且可以在CBabel ADL的高级合同中指定。给出了软件体系结构描述语言CBabel的重写逻辑语义，重新访问和扩展了一些作者以前的工作，现在包括修改以前的语义和增加新的功能，涵盖了所有的语言。还介绍了CBabel工具。CBabel工具是CBabel的原型执行环境，它实现了给定的CBabel重写逻辑语义，并允许在Maude系统中执行和验证CBabel描述，这是重写逻辑的实现。通过这种方式，描述复杂应用程序的软件架构可以在其生命周期的软件架构设计阶段就死锁和同步一致性等属性进行形式化验证。保留字：软件体系结构描述语言，重写逻辑，Maude，契约1571-0661 © 2005由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2005.03.018346A. Rademaker等人理论计算机科学电子笔记130（2005）3451介绍分布式和并发应用程序总是有协调需求。这些应用程序的设计，由几个（可能是分布式的）组件组成，必须考虑协调要求，包括组件间的交互风格，组件内的并发性和同步方面。例如，组件可以使用同步或异步方法调用进行交互。另外，两个或多个方法的调用协调需求通常在编程阶段通过使用操作系统提供的语言结构[19，17]或库服务[3，2]来这通常会导致特别的方法，协调代码与功能代码纠缠在一起，导致可重用的模块较少，并且容易出错[14，25]。即使在使用现代技术（如设计模式）时，也要由设计师使用递归设计[34]，并考虑到关注点的分离和模块化。在CR-RIO框架[ 21，37 ]中使用软件体系结构描述语言（ADL）的目的是将分布式组件如何连接的描述与每个组件内部行为的描述由架构描述提供的关注点分离有几个有趣的属性，包括架构描述的模块化，不同架构中组件的重用，以及架构的（动态）重构。CBabel是一种ADL，除了通常的架构原语[35]，如组件和端口，还提供契约[33，16，4]作为第一类构造。通过这种方式，协调方面可以用CBabel合同来描述。基本上，设计者可以描述互斥属性，该互斥属性约束功能模块的输入端口（或简称为输入端口）的使用，并指定保护来管理这些输入端口的同步和一致性属性。所描述的协调方面被封装在连接器中，该连接器调解功能模块之间的所有交互。通过这种方法，我们将协调方面的问题与功能方面的问题分开，这些方面不需要包括在功能模块的设计或实现事实上，同一组件的不同实例可以提交到不同的协调规范。1电子邮件地址：alexszt@ime.uerj.br2电子邮件地址：arademaker@ic.uff.br3电子邮件地址：cbraga@ic.uff.brA. Rademaker等人理论计算机科学电子笔记130（2005）345347在[5]中提出了CBabel [21]的重写逻辑[28]语义的基本思想。本文给出了CBabel在重写逻辑中的完全形式化，即它的重写语义，并给出了CBabel工具--在Maude系统中实现的CBabel执行环境[8]。CBabel工具是CBabel重写语义的直接实现，它允许执行和验证CBabel描述。我们专注于CBabel的形式化和CBabel工具的使用。关于CBabel工具实施情况的详细报告将在其他地方提供。重写逻辑是一个逻辑和语义框架，由于其统一的计算和逻辑视图，计算，逻辑和特定语言的几个模型已经映射到[24]。Maude是重写逻辑的高性能实现和强大的元工具，当其元编程设施与系统中内置的分析工具（如LTL模型检查器[12]）或Maude本身开发的分析工具（如ClavelMaude还在Full Maude中实现了一个可扩展的模块代数[11]，这也赋予了Maude系统一个面向对象的语法。CBabel工具是作为Full Maude的一个保守扩展来实现的，遵循了对CBabel概念在面向对象术语中的非常自然的解释。粗略地说，组件由类表示，组件重写语义，我们已经给CBabel使用面向对象的符号重写逻辑，并实现为一个转换，形成功能在Maude使用Maude的元编程能力。这个转换函数是CBabel工具执行环境原型的核心。本文件的其余部分组织如下。第2节举例说明CBabel语法。第三节介绍了Maude的重写逻辑和面向对象重写理论的必要背景第4节定义了CBabel的重写语义。第5节介绍了使用CBabel工具在Maude中执行和验证CBabel描述。第6节讨论相关工作。第7节以我们的最后评论结束本文。2CBabel描述在本节中，我们通过经典的生产者-消费者-购物者示例的三种变体来介绍CBabel的语法稍后在第5节中，我们将使用CBabel工具在Maude中验证这些规范。值得强调的是，Maude规范是由CBabel工具自动生成的，因为348A. Rademaker等人理论计算机科学电子笔记130（2005）345与我们以前的工作[5]相反在生产者-消费者-购买者示例中，存在愿意访问购买者（其可以是有界的）以添加其刚刚生产的物品的生产者，以及愿意访问购买者以消费来自购买者的物品的消费者。在这种情况下存在至少两个问题：（i）生产者和消费者不应该同时访问缓冲器，这是所谓的竞争条件，以及（ii）缓冲器是有界的，并且生产者不应该添加比缓冲器可以容纳的更多的项目，并且消费者不应该从空缓冲器中移除项目。（实际上，在第5节中，我们还检查了死锁。）第一个CBabel架构，它指定了生产者-消费者-购物者，以及相应的非正式图形表示，如图1所示。请注意，在图形表示中，表示了组件的名称及其各自的输入和输出端口，以帮助读者遵循CBabel代码。模块指定将在架构配置中使用的组件一个特殊的模块，称为应用程序，声明每个组件应该如何实例化，以及它们应该如何链接在一起。在图1中，应用程序模块被命名为PC-DEFAULT。它为每个组件创建一个实例，并通过它们的端口将它们链接在一起。有输入和输出端口。输入端口可以非正式地理解为组件提供的因此，在我们的例子中，生产者需要一个服务来交付或放置一个物品，而消费者则需要一个服务来获取。缓冲器模块提供将项目放入其内部存储器和从其内部存储器获取项目的服务。服务的实际请求通过端口激励发生，也就是说，生产者请求放置一个项目的事实由其放置端口的激励表示。以同样的方式，一个服务商或提供其服务，以把（或。得到）一个项目（或 从）它的内部缓冲器是由一个刺激表示以其为例，get）端口。[4]一系列这样的端口刺激称为交互作用。端口可以异步和同步通信。在后一种情况下，输出端口期望来自链接到它的输入端口的返回或确认激励异步端口使用oneway关键字指定。图1、2和3中的示例声明了同步端口。正如我们之前提到的，这种架构既有竞争条件问题，4例如，人们可能已经注意到，实际的项类型没有被声明为producer@put的参数。这是因为我们实际上感兴趣的是验证与架构中消息的控制流相关的属性，而不是消息所携带的数据的属性A. Rademaker等人理论计算机科学电子笔记130（2005）345349模块PRODUCER {应用程序PC-DEFAULT {输出portproducer@put;将BUFFER实例化为buff;}将PRODUCER实例化为prod;将CONSUMER实例化为cons;模块CONSUMER{instantiateDEFAULTas default1;out portconsumer@get;instantiateDEFAULTas default2;}link prod.producer@put to default1.default@in ; link default1.default@out tobuff.buffer@put;connectorDEFAULT {link cons.consumer@get to default2.default@in;in portdefault@in;link default2.default@out to buff.buffer@get;outport default@out;}互动default@in> default@out; moduleBUFFER {} varint n=int（0）;} varint buffer@maxitems =int（2）;in port buffer@put;在port buffer@get中;}生产者@put默认buffer@put默认值@in缓冲默认消费者@getbuffer@getdefault@outFig. 1. 生产者-消费者-消费者基本结构lem之间的prod和cons，PRODUCER和CONSUMER的实例，分别，也可能有过流和欠流问题，如果缓冲器是有界的。 为了解决竞争条件问题，可以使用互斥合约来协调生产者和消费者对缓冲器的访问，因为交互将通过端口mutex@in1或mutex@in2发生。图2展示了一个新的应用程序模块，它连接生产者、消费者和通过一个互斥连接器连接到缓冲器，该互斥连接器介导对缓冲器的访问。在图2的体系结构中仍然存在对缓冲器的有界访问的问题。为了解决这个问题，可以使用保护交互契约或简单的保护契约。它规定，如果某个条件成立，两个端口可以相互作用。一旦条件成立，就会执行合约的before块。当确认激励到达输出端口时，执行保护合同的after块。另一个通常与守护契约一起使用的概念是状态变量。状态变量是共享内存变量。在CBabel中，状态变量在共享这些变量的组件中声明，应用程序模块将它们绑定在一起，指定当其中一个变量制片人消费者350A. Rademaker等人理论计算机科学电子笔记130（2005）345连接器MUTEX{应用PC-MUTEX{在端口mutex@in1;将BUFFER实例化为buffer;在端口mutex@in2;将PRODUCER实例化为prod;输出端口mutex@out1;将CONSUMER实例化为cons;输出端口mutex@out2;将MUTEX实例化为mutx;exclusive{linkprod.producer@putto mutx.mutex@in1; mutex@in1 > mutex@out1;link mutx.mutex@out1to buff.buffer@put;mutex@in2 > mutex@out2;link cons.consumer@getto mutx.mutex@in2;}link mutx.mutex@out2to buff.buffer@get;} }个文件夹生产者@putmutex@in1mutex@out1buffer@putMUTEX缓冲液buffer@getconsumer@getmutex@out2 mutex@in2图二、MUTEX连接器和PC-MUTEX应用有了变化，对方应立即注意到变化。图3在连接器GUARD-PUT和GUARD-GET中指定了两个保护，分别控制生产者和消费者对缓冲器的访问。它们通过检查选定的状态变量来控制对缓冲器的访问，以转发或阻止交互流。 变量gp@nEmpty绑定到gg@nEmpty，变量gg@nFull绑定到gp@nFull，如PC-GUARDS-MUTEX应用程序模块中所述。每当缓冲器中的空白空间数gp@nEmpty变为零时，GUARD-PUT相反的情况发生在缓冲器根本没有任何项目，gg@nFull等于零，然后GUARD-GET一个重要的观察是，在警卫合同本地变量用于驱动同步机制。在BUFFER模块中，还有其他局部变量控制缓冲器的实际状态。这有助于进一步将协调关注点与业务实现分开。请注意，在图形表示中，仅描述了添加到此新配置的连接器的端口（GUARD-PUT和GUARD-GET）。还要注意这些连接器之间的虚线双箭头，表示代码中描述的局部变量的绑定。在架构级别中指定的协调合同（如刚才描述的）可用于生成可部署代码[37]，并允许在进入实现阶段之前采用形式化技术来验证预期设计的几个属性[23]。在第4节中，我们提出了应对这一挑战的方法。消费者制片人A. Rademaker等人理论计算机科学电子笔记130（2005）345351连接器GUARD-PUT{连接器GUARD-GET{var intgp@nFull = int（0）;varintgg@nEmpty=int（2）;staterequired intgp@nEmpty;staterequired intgg@nFull;in portgp@in;in portgg@in;输出端口gp@out;输出端口gg@out;interaction {相互作用{gp@in> gg@in>guard（gp@nEmpty >int（0））{guard（gg@nFull >int（0））{ before {before {gg @nEmpty = gg @nEmpty- int（1）;gg@nFull = gg@nFull- int（1）;} }个文件夹在{after {gg @nFull = gg @nFull +int（1）;gg@nEmpty = gg@nEmpty +int（1）;} }个文件夹} > gg @out;} > gg@out;} }个文件夹} }个文件夹应用程序PC-GUARDS-MUTEX{将BUFFER实例化为buff;将 PRODUCER实例化为prod;将 CONSUMER实例化为cons;将 MUTEX实例化为mutx;将 GUARD-GET实例化为gget;将 GUARD-PUT实例化为gput;将producer@put链接到gput.gp @in;将cons.consumer@get链接到gget.gg@in;将gput.gp @out链接到mutx.mutex@in1;将gget.gg @out链接到mutx.mutex@in2;链接mutx.mutex@out1到buff.buffer@put;链接mutx.mutex@out2到buff.buffer@get;将intgget.gg @nFull绑定到 gput.gp @nFull;将intgput.gp@nEmpty绑定到 gget.gg @nEmpty;}gp@in防护装置gp@out缓冲互斥gg@in防护装置gg@out图三.防护连接器和PC-GUARDS-MUTEX应用3重写逻辑与莫德重写理论R是一个元组（E，E，R），其中E是重写理论 集合假设方程的E是连续的和终止的，这大致意味着每一项都应该有一个唯一的标准形式，并且应该是无条件的。制片人消费者352A. Rademaker等人理论计算机科学电子笔记130（2005）345我我JJ方程简化步骤的nite链。规则R应该是连贯的，即在方程和规则之间交替不会丢失重写计算。规则被应用于模E，也就是说，重写关系被定义在具有变量T（X）的方程规范（E，E）重写逻辑由其底层的等式逻辑参数化。(In在Maude系统中选择了一个特殊的隶属度方程逻辑[30]，它是顺序排序方程逻辑的推广。此外，冻结算子的概念[6]已经被添加到重写理论中，使它们一般化。然而，为了保持表达的简单性，在下面的重写逻辑的演绎规则中，我们选择顺序排序的等式逻辑作为底层逻辑和不考虑冻结运算符的重写逻辑版本。• 回复性。对于含 变 量 的 初 始 代 数 中 的 每一 项t，T（X），• 平等的（X）t−→t（X）u−→vE（X）u=uJE（X）v=vJ（X）uJ−→vJ• 一致性。 对于每个f：k1. 其中ti，TJ∈T∈（X）k，1 ≤i≤n，我我（X）t1−→tJ. （X）t−→ tJ1mm（X）f（t1，. t m）−→（nX）f（tJ，. tJ）1m• 更换. 对于每个有限置换θ：X→T（Y），对于每个形式的规则1：（X）t−→tJ（i=i（wj−→wJ）（Y）θ（u）=θ（uJ）（Y）θ（w）−→θ（wJ）iiijjj• 传递性。（Y）θ（t）−→θ（tJ）（X）t1−→t2. （X）t2−→t3（X）t1−→t3重写逻辑是描述并发系统的计算逻辑。上面的推理规则允许我们推断出所有可能的无穷并发A. Rademaker等人理论计算机科学电子笔记130（2005）345353一个系统的计算被指定为重写理论如下：（i）自反性是有空闲转换的可能性，（ii）相等意味着状态是模E相等的，（iii）同余是横向并行的一般形式，（iv）替换在替换中使用嵌套并发的规则在顶部组合原子转换，以及（v）传递性是顺序组合。一类重要的并发系统是并发对象系统。重写逻辑有一个基于对象的符号，这对我们在给出CBabel的语义时非常有用，因为用面向对象的术语来考虑CBabel原语是非常自然的，正如我们在第1款.特别是，Maude语言中的面向对象语法[29]将并发状态或系统配置表示为对象和消息的多集，并与以下操作符声明并列。操作 ：配置配置→配置[ctorasynchronid：null].关键字op用于在Maude中声明运算符。关键字ctor、ascurve、identifier和id是并置运算符的属性，意味着它是一个满足结合性和交换性结构定律的构造函数，并且具有标识null，声明为排序Configuration的常量运算符。对象和消息是单例配置，是配置排序的子排序，因此通过多集并可以从它们中对象表示为项中文（简体）|a1：v1，. ，a n：v n其中O是对象属性的顺序并不重要，因此_，_操作符也通过属性ascurve和ascurve声明为关联和可交换的。类在Maude中用语法C类|a1：s1，. ，a n：s n。其中C是类名，si是属性ai所需的排序。也可以给出子类声明，这样超类的所有属性和重写规则都可以被子类继承，子类可以拥有自己的附加属性和规则消息的语法是使用msg关键字以类似于运算符声明的方式声明的例如，一个名为to的消息，由发送者对象的对象标识符参数化，接收者对象的对象标识符和一些数据可以声明为：MSG 到 ：Oid Oid 数据 →Msg.构形的多重集构造函数的结合性和交换性354A. Rademaker等人理论计算机科学电子笔记130（2005）345I1IkI1QIk使其成为重写规则将对象间的并发交互公理化。这种规则的一般形式在Maude中给出如下：crl[r]：M1... M nO1：F1|atts1 ... 单位：mm|阿茨米茨1999年1月1日J | attsJ 我... ⟨ OikJ | attsJ⟩第一季第1集|Attsjj ... Q p：D p|AttsjjJ1如果C.1个p...MJ其中r是规则标签，M是消息表达式，i1，.，i k，是原始1，.，m，C是规则的条件。4CBabel软件体系结构原语CBabel的基本软件架构元素可以非正式地定义如下。组件可以是模块或连接器。模块是执行计算的实体（如对象或函数）的“包装器”。连接器调解模块之间的交互，控制它们如何通信和协调。组件通过端口相互通信，请求功能或“服务”。端口遵循消息传递模型进行通信。协调合同定义了一组港口应该如何互动。它可以是顺序的、互斥的或由条件保护的。应用程序是一个特殊的模块，它声明每个组件应该如何实例化，组件应该如何链接，以及状态变量应该如何相互绑定。链路建立两个端口的连接，使它们能够相互作用. 状态所需变量允许组件原子地交换信息，也就是说，在通信的共享内存模型中。下面的部分根据表1中CBabel元素到面向对象概念的映射来形式化这些概念。在下文中，我们使用小写字母表示集合中的元素，大写字母表示集合本身。：女：女MA. Rademaker等人理论计算机科学电子笔记130（2005）345355构件→面向对象理论构件实例→对象应用程序状态→多组对象端口→消息声明端口激励→消息传递（重写规则）链路→无条件方程协调契约→重写规则本地或状态所需变量→类属性变量约束表1从CBabel概念到重写逻辑的4.1组件组件可以是模块或连接器。模块可以声明局部变量、输入端口和输出端口。 除了可以在模块中完成的相同声明之外，连接器还可以声明协调契约并声明所需的变量。在重写逻辑中，组件被映射到重写理论。每个组件都在相关的重写理论的签名中产生一个类声明，以组件的名称命名，并带有构造方法。组件实例由此类的对象实例表示。表示模块的对象可以应答消息do和done。这些消息表示或表示模块可解释的内部行为的开始和结束(This在验证问题上很重要，我们将在第4节中看到。）连接器，轮到他们，对所描述的协调合同指导的消息作出反应。消息在给定的交互中携带对象标识符的序列，即，通过链接声明相关的端口的端口刺激的有限序列。交互序列是必要的，以便当有多个组件实例链接到给定的输入端口时，组件实例可以在同步交互中被正确地确认。CBabel模块中的局部变量映射到重写理论签名中关联类中的类属性让我们在重写逻辑中形式化组件。但是，请注意，端口声明将在4.2节中正式化，协调合同的正式化在4.3节中给出。CBabel模块声明M是一个元组（n，V，I，O），其中n是表示模块的356A. Rademaker等人理论计算机科学电子笔记130（2005）345name，变量声明的集合V包含三元组（v，l，t），其中v是表示变量名称的标识符集合I和O都是分别保存输入和输出端口声明的标识符集合。上面非正式描述的交互的概念被形式化为一堆对，其中第一个投影是对象标识符，第二个投影是一个端口标识符，在重写理论CBA-BEL-CONFIGURATION中声明，它包含基本声明，这些声明将在接下来的章节中与消息声明一起明确说明do， done：Oid PortId交互→消息CBabel模块n的重写语义由重写理论R =（R，E，R）给出，其签名R_n导入CBABEL-CONFIGURATION重写理论的声明，以及类声明类n|S，其中S是类n的属性集，其元素以V的元素命名。签名实例还包括类构造函数操作符声明instantiate-n：Oid→Object。方程组E包括：(1)eq instantiate-n（ω）= <ω ：n|a1：l1，. ，an ：l n>。其中ω是一个对象标识符，每个ai是一个以vi命名的对象属性，li是vi的值。等式1说明，给定一个对象标识符，instantiate-n产生一个类n的对象实例，其属性初始化为V中CBabel组件变量声明的值l。4.2端口CBabel组件可以具有输入端口和输出端口。 输入端口用于提供给定组件的服务，而输出端口用于由组件用于向其他组件请求服务。此外，端口通信可以是同步的或异步的。后一种情况在CBabel中通过关键字oneway声明。没有oneway关键字作为端口声明修饰符意味着通过该端口的通信应该是同步的。在给定的CBabel组件中，端口声明被映射到相关重写理论签名中的消息声明。当然，端口激励表示为将消息传递给适当的对象，即传递给表示链接到该端口的组件的对象。 (See第4.4节，CBabel的链接声明的形式化。）然而，我们没有为每个端口声明一个消息，而是选择声明两个通用消息send和ack，因为它大大简化了语义。的A. Rademaker等人理论计算机科学电子笔记130（2005）345357端口然后被映射到参数化这些通用消息的常数。消息send和ack，就像do和done一样，在给定的交互中携带对象标识符的序列。端口的声明还包括相关重写理论中的规则。然而，规则生成的处理对于模块和连接器是不同的，因为连接器与模块相反，声明协调交互的契约，即表示架构实例的对象之间的消息流，也称为拓扑。在本节的后面，我们将解释规则是如何从模块中的端口声明中派生出来的，第4.3节将详细解释规则是如何从连接器中的端口和协调契约声明中派生出来的模块中有四种不同的端口声明可能性，它们是由同步和异步通信与输入和输出端口交互相结合而• 当在CBabel组件中声明同步输入端口时，必须创建两个规则：（i）一个规则指定向该端口发送消息应触发该组件的内部行为，（ii）另一个规则指定一旦内部行为完成，应将确认消息发送回激活该端口的组件。触发一个组件一旦一个组件完成了它的内部行为，它就会向自己发送一个完成的消息，然后将其转换为一个确认消息。• 当一个异步输入端口被声明时，一个规则应该被添加到重写理论• 声明一个同步输出端口需要向相关重写理论的规则集添加两个规则。第一条规则规定，当一个组件正在执行其内部行为时，可以通过该端口请求来自另一个组件的“服务”。此外，该请求应该阻止该端口，直到对该请求的应答到达，从而解锁该端口，这由第二重写规则指定。然后，该内部行为的执行被认为已经完成。锁定和解锁端口的效果是通过更新对象中该端口的status属性来捕获的，该对象表示持有该端口的CBabel组件实例• 异步输出端口的声明将规则添加到相关重写理论的规则集。该规则规定，一旦该端口被激活，相关的消息可以无条件地重写，因为异步端口不需要确认消息，因此358A. Rademaker等人理论计算机科学电子笔记130（2005）345不需要我们在上一个项目符号中描述的同步输出端口的处理。现在让我们把这篇散文形式化。首先注意，从CBabel组件端口声明到相关重写理论签名的映射对于模块和连接器都是相同然而，需要不同的处理来指定行为。正如我们上面的非正式解释，在本节的剩余部分中，我们将形式化重写理论签名如何由关联的CBabel组件中的端口声明来验证，以及重写理论的规则集如何由关联的CBabel模块中的端口声明来验证。在CBabel连接器中，如何从端口声明和协调契约中生成规则的形式化将在4.3节中给出。给定一个CBabel模块声明（n，V，I，O）或一个连接器声明（n，V，I，O，c），其中n是组件与CBabel组件相关联的重写理论的签名包括：（i）对于I中的每个端口声明p，排序PortInId的常数p，（ii）对于O中的每个端口声明p，排序PortOutId的常数p。排序PortInId和PortOutId是PortId的子排序，PortId是参数化发送的一般消息的排序，ack：Oid PortId Interaction→Msg。排序PortId、PortInId和 PortOutId 以 及 消 息 send 和 ack 在 重 写 理 论 CBABEL-CONFIGURATION中声明，包括在XML中。CBabel模块中端口声明的形式化如何在相关的重写理论中产生规则应该考虑上面非正式给出的港口申报的四种给定一个CBabel模块声明（n，V，I，O）：• I中的同步输入端口i的声明产生相关联的重写理论规则集R中的规则2和规则3：(2)rl send（ω，i，i）<ω：n|中文（简体） do（ω，i，i）<ω：n|A>.(3)rl done（ω，i，i）<ω：n|中文（简体） ack（i）<ω ：n|A>.其中ω是表示CBabel模块实例的对象的对象标识符，i是交互，A是对象• 异步输入端口的声明产生规则2和规则4：(4)rl done（ω，i，i）<ω ：n|联系<我们 ：n| A>.• 同步输出端口o∈O的声明产生规则5和6，(5) rl do（ω，o，none）<ω ： n|o-状态 ：unlocked，A >解锁A. Rademaker等人理论计算机科学电子笔记130（2005）345359send（ω，o，[ω，o]）<ω ：n|o-状态 ：锁定，A >。(6) rl ack（[ω，o]）<ω ：n|o-status：s，A > 0< ω ：n|o-状态 ：unlocked，A > done（ω，o，none）.其中s是排序PortStatus的变量，在重写理论C中声明BABEL-配置和常量锁定，解锁：→端口状态，而none是Interaction的单位。• 异步输出端口的声明产生规则7：(7)rl do（ω，o，none）< ω ：n|中文（简体）send（ω，o，[ω，o]）<ω ：n| A>.第4.3节继续CBabel原语的形式化，描述协调契约如何在重写逻辑中形式化。4.3协调合同协调契约是连接器内部交互流的规范，可以声明端口之间的顺序、互斥或受保护的交互。输入端口和输出端口之间的顺序协调契约规定，当后者被激励时，前者也被激励。应在两个输入端口之间声明互斥声明与输入端口和输出端口相关的受保护协调契约。一个受保护的协调契约有一个条件，一个before块和一个after块。一旦输入端口被激励并且条件保持，则执行before块并且输出端口被激励。一旦对输出端口激励的应答到达，则执行after块。但是，如果将消息发送到输入端口，并且保护条件不成立，则该消息将排队并保持，直到保护条件变为真。在给出契约语义之前，让我们解释一下形式化的直觉。输入端口和输出端口之间的顺序对同步输出端口的确认（也由规则指定）弹出交互的顶部，并将确认转发给其标识符是5参与互斥协调契约的每个输入端口都有一个相关联的输出端口，也就是说，指定了顺序契约的互斥360A. Rademaker等人理论计算机科学电子笔记130（2005）345在交互堆栈中的新顶部。此处理方法处理1：1或n：1交互样式，即当一个组件和一个连接器或多个组件和一个连接器之间存在链接时。在需要1：n交互风格的情况下，顺序契约可以与并行协调契约一起使用，这意味着当输入端口被无条件地激励时，连接器这就产生了一个规则，该规则将表示对输入端口的激励的消息重写为表示对每个输出端口的激励的n个消息。如果输出端口是同步的，则对表示应答段的n个消息的处理是一旦接收到所有n个应答段就转发一个确认如果输出端口是异步的，则没有关于确认消息的规则。两个同步输入端口之间的互斥协调契约具有二进制信号量语义，由状态属性（即，标记属性）表示，具有两个规则6，其被非确定性地应用于选择要演进的消息应用其中一个规则后，它将从配置和表示连接器实例的对象中选择如果状态属性未锁定，则重写消息，并将状态属性设置为锁定，从而防止应用选择规则之一，并因此防止选择另一个要重写的消息。到达表示连接器的对象的确认消息也由一个规则指定，该规则将status属性设置为unlocked，因此允许再次非确定性地应用规则。互斥只允许在同步输入端口之间。一个警卫合同由三个方程和两条规则形式化。一个等式是一个谓词，它根据表示连接器的对象中的一组属性值来计算守卫的条件。另外两个等式表示之前和之后的动作，它们本身是表示守卫契约之前和之后语句的等式的组合。第一条规则规定，一旦消息到达输入端口，如果保护条件成立，则before等式将应用于表示连接器的对象，并将发送消息发送到输出端口。否则，如果保护条件不成立，则到输入端口的消息将简单地等待未写入的配置。这精确地保持了保持消息的效果，直到守卫准备好以一种比实例化队列数据类型更通用的方式处理它。现在让我们用正式的术语来说明这些定义。给定一个连接器dec（n，V，I，O，c），其中n是组件6一个不同的映射，它将连接器的输入端口声明为PortInId的一个子类，这将允许生成一个规则。A. Rademaker等人理论计算机科学电子笔记130（2005）345361声明集，I是输入端口声明集，O是输出端口声明集，c是顺序合同声明，c是一对端口（i，o），第一个投影i∈I是输入端口，第二个投影o∈O是输出端口。合约c的声明产生相关联的重写理论（R，E，R）的规则集R中的规则8(8)rl send（ω，i，i）<ω ：n|中文（简体） send（ω，o，[ω，o]：：i）<ω ：n| A>.其中操作[、]：Oid PortOutId→Oid PortIdPair和：：：互动互动→互动分 别 是 OidPortIdPair 和 Interaction 的 构 造 函 数 操 作 符 ， 其 中OidPortIdPair 是 Interaction 的 子 排 序 ， 都 在 重 写 理 论 CBABEL-CONFIGURATION中声明，ω是表示CBabel连接器实例的对象的对象标识符，i是interaction，A是对象当使用并行协调契约时，规则8在规则右侧的每个输出端口都有一个发送如果输出端口o是同步的，则规则9也被添加到R。当使用并行协调契约时，规则9在规则的左侧具有用于每个输出端口的一个ack消息。如果o是异步的，则不添加规则9(9)rl ack（[ω，o]：：i）<ω ：n|中文（简体） ack（i）<ω ：n|A> .给定一个连接器声明（n，V，I，O，c），其中n是组件标识符，V是变量声明集，I是输入端口声明集，O是输出端口声明集，c是互斥合约声明，c是一个四元组（i1，o1，i2，o2），其中i1，i2∈I，o1，o2∈O。合约c的声明产生了一个类属性status：PortStatus→Attribute在重写理论CBABEL-CONFIGURATION中声明，并被类n的每个实例ω使用。规则10、11、12和13包括在R中，(10) rl send（ω，i1，i）<ω ：n|地位 ：Unlocked，A >解锁< ω ：n|地位 ：locked，A > send（ω，o1，[ω，o1]：：i）.(11) rl send（ω，i2，i）<ω ：n|地位 ：Unlocked，A >解锁< ω ：n|status：locked，A > send（ω，o2，[ω，o2]：：i）.(12) rl ack（[ω，o1]：：i）<ω ：n|地位 ：锁定，A >锁定< ω ：n|地位 ： unlocked，A > ack（i）。(13) rl ack（[ω，o2]：：i）<ω ：n|地位 ：锁定，A >锁定< ω ：n|地位 ： unlocked，A > ack（i）。其中ω是表示对象的实例的对象标识符，362A. Rademaker等人理论计算机科学电子笔记130（2005）345CBabel连接器，i是交互，A是对象给定一个连接器声明（n，V，I，O，c），其中n是组件(We我将不给出语句和表达式的详细语法和含义，因为它们是直接的，这里我们希望集中在守卫契约的含义上。它比把β和α理解为函数的合成更有意义，这些函数赋予这些陈述和表达式以意义。）c的条件b产生一个函数，它是b 中语句的合成。 另外，一个方程关系到抽象函数的开通？：Object→Bool到函数，它是保护条件表达式b的含义。函数β和α分别由CBABEL-CONFIGURATION中描述的函数before、 after：Object→Object表示。β和α的声明产生两个方程。每个方程都是代表β和α中语句序列的函数的组合。（同样，为了使演示文稿专注于合同的含义，这里将不显示它们。）最后，将规则14和15添加到R中。(14)crl send（ω，i，i）<ω：n| A>在（<ω：n）之前|A>）send（ω，o，[ω，o]：：i）if opened？（<ω：n|A>）。(15)rlack（[ω，o]：：i）<ω：n|中文（简体） 在（<ω：n| A>）ack（i）。4.4应用CBabel应用程序模块声明了架构的组件应该如何它可以实例化组件，然后通过它们的端口将它们链接在一起，并绑定它们的状态变量。（见第4.5节）形式上，CBabel应用程序模块是一个三元组（x，Y，L，B），