Reo组件连接符的形式语义及分析

理论计算机科学电子笔记154（2006）83-99www.elsevier.com/locate/entcsReo中构件连接符的形式语义及分析MohammadReza Mousavi1，Marjan Sirjani2，3，FarhadArbab21TU/Eindhoven，埃因霍温，荷兰2CWI，阿姆斯特丹，荷兰3德黑兰大学和IPM，德黑兰，伊朗摘要我们提出了一个名为Reo的组件组合语言的操作语义。Reo连接器外生地组成和协调组成复杂系统的各个组件之间的交互，使其成为一个连贯的协作。 我们在这里提出的形式语义铺平了道路，严格的研究行为的组件组合机制。为了证明这种严格的方法的可行性，我们给一个忠实的翻译Reo语义到Maude长期重写语言。这种转换允许我们利用Maude工具集中的重写引擎和模型检查模块来象征性地运行和模型检查Reo连接器的行为关键词：协调语言，Reo，结构操作语义学，术语重写，Maude1介绍大规模并行和分布式系统提供了一个平台，用于构建大型和复杂的应用程序，它们为软件技术带来了新的挑战。基于敏捷的软件开发已经被提出作为一种手段来解决软件开发的日益复杂性。组件被假定为分离的、独立的功能和部署单元，通过使用组件组合机制，可以构建出完整的应用程序。组件组合的一个重要方面是，连接代码段必须匹配组合组件的不同需求，1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.03484M.R. Mousavi等人理论计算机科学电子笔记154（2006）83实现位于单独组件边界之外的系统行为的各个方面。这段代码被称为胶水代码。系统中胶水代码的复杂性可以从简单的同步和排序原语到复杂的分布式协调协议。通常需要能够指定和设计这些连接设备，并单独分析和推理它们的行为，以及在组件的（抽象）行为模型的上下文中。尽管如此，在这个方向上已经做了一些工作，组件连接器通常使用没有精确语义的文本或图形符号进行未指定或未指定，通常体现为《双城之战》通信和专门的脚本语言代码。Reo [2]是一种协调语言，它通过创建一个表达模型和一种图形语言来解决这个问题，该语言用于通过原始通道的组合来构建组件连接器。Reo可用于建模和构造实现某些特定行为的连接器，并对它们进行形式化推理。因为所构建的Reo电路直接构成所谓的粘合代码，一旦被证明是正确的，它们可以很容易地用作系统中的连接器。因此，使用Reo可以实现构建组件连接器的正确构造方法。在本文中，我们提出了一个形式语义的Reo在Plotkin的风格结构操作语义学（SOS）[15]。使用这种语义，我们从SOS的研究结果和可用工具中受益。特别地，我们可以正式地观察和推理组件连接器的操作行为。为了实现这一潜力，我们已经实现了我们的SOS语义在重写逻辑语言的Maude [1]。这种实现为Reo中指定的连接器的符号执行铺平了道路，并进一步使用线性时态逻辑（LTL）对其属性进行模型检查。本文其余部分的结构如下。在第2节中，我们对Reo做了一个简洁而非正式的介绍。然后，在第3节中，我们定义了Reo的一个可行子集的语法和语义，以及Reo连接器的相等和细化的概念。我们在Maude中实现的Reo将在第4节中给出，并提供一些我们使用该实现进行实验的例子。我们将我们的方法与其他相关的建模组件连接器的方法进行比较，并在第5节中详细说明Reo的其他现有语义。最后，第6节总结了我们的贡献。由于篇幅所限，我们在此不介绍具体的实现细节。这篇论文的更详细的版本可以在[14]中找到。Maude中的实现代码及其附带的文档和几个示例可在以下URL中获得M.R. Mousavi等人理论计算机科学电子笔记154（2006）8385http://www.win.tue.nl/www.example.com2Reo：一种协调语言Reo [2]是一种基于通道的外生协调语言，其中复杂的协调器（称为连接器）是由简单的协调器组成的Reo中的基本连接器（称为通道）具有由用户提供的明确定义的行为。组件可以通过连接器实例化、组合、连接和执行I/O操作。REO连接器以与逻辑和电子电路相同的精神构造：采用基本元件（例如，导线、二极管和晶体管）并将它们组合以构建电路。一个复杂的连接器有一个图形表示，称为一个Reo电路，它可以通过应用Reo的连接组合运算符产生Reo电路通过其基本连接器协调数据流，该基本连接器互连某些组件的输入/输出端口。 在本文中，我们不考虑组件对连接器的动态创建、组合和重新配置，这是Reo固有的。我们将注意力限制在具有静态图形表示的连接器上，如Reo电路。Reo对通道的概念远比其常见的解释更普遍，它允许任何具有两端的原始通信媒介。信道端被分类为数据进入的源端和数据离开信道的宿端。Reo允许一组开放的通道类型，具有用户定义的语义，每个通道类型具有不同的排序、同步、缓冲、计算和数据丢失特性。组合连接器由通道和节点组成。一组通道末端重合在一个节点上，并且每个通道末端正好重合在一个节点上。仅源信道端在其上重合的节点是源节点，并且仅宿信道端在其上重合的节点是宿节点。具有源和汇重合通道端的节点称为混合节点，在本文中，混合节点是连接器的内部或隐藏节点节点是Reo中一个重要的逻辑概念，不应与组件或位置混淆节点可以四处移动并驻留在Reo中的各种物理位置上，从而提供了移动性的基本和自然概念。然而，我们在本文中不涉及流动性。直观地说，电路本身也可以被认为是一个组件，其中它的源节点对应于输入端口，它的汇聚节点对应于组件的输出端口，而混合节点和内部基本连接器构成了它的隐藏内部结构。组件不能连接到混合节点，也不能从混合节点读取或写入混合节点。相反，通过混合节点的数据流是完全指定的86M.R. Mousavi等人理论计算机科学电子笔记154（2006）83它们所属的电路组件可以将数据项写入它所连接的源节点。仅当在节点上重合的所有（源）通道末端接受数据项时，写入操作才成功，在这种情况下，数据项被透明地写入到在节点上重合的每个源末端。因此，源节点充当复制器。组件可以从它通过输入操作连接到的汇聚节点获得数据项。只有当至少一个（汇）通道末端在节点上重合或包含合适的数据项时，输入操作才成功;如果多个重合通道末端包含合适的数据项，则非确定性地选择一个。一个汇节点，因此，作为一个非决定性的合并。混合节点是自包含的组件行为可以建模为Reo的一个侧面规范，这样人们也可以分析组件与Reo连接器的交互。在其余部分中，我们假设组件的输出值可用作初始数据序列，这些序列用作Reo连接器的输入。这个假设在我们的语义中可以很容易地放松，正如我们在本文的扩展版本中所说明的那样[14]。在那里，我们还提出了如何系统地定义新渠道类型并在我们的框架内使用它们的初步想法3Reo的语义和操作语义每个通道代表一个具有两端的简单连接器。在本文中，我们使用基本连接器的概念来表示Reo中的通道概念，并添加了两个基本连接器：Fork和Merge。这两个连接器分别对Reo节点中的复制数据项和从多个可用数据项中选择数据项进行建模。这一添加简化了给定的语义，因为节点被简化为连接点，而不是复制点，泵点和选择点。 在这种简化的电路中，每个节点最多有一个重合的源和一个重合的汇通道端。这种简化在这里是合理的，因为在本文中，我们只限于静态Reo电路，对于每个静态Reo电路，都存在一个具有简化节点和Fork和Merge连接器的简化Reo电路，反之亦然。在本节中，我们将自己限制在基本连接器类型的固定集合上，这些连接器类型具有足够的表达能力来指定大多数实际系统（事实上，这个子集是图灵完备的[2]）。在[14]中，我们展示了如何推广M.R. Mousavi等人理论计算机科学电子笔记154（2006）8387−−→系统：：={BCI}|Sys SysBCI：：=BCTNodeSet BCT NodeSetNodeSet：：= nodeSet|节点集{Node}BCT：：= −→|>−<|−−·|−Q→| −a→|−[u] →| −{pat}→| −−<|>−−Fig. 1. 玲央这个子集。3.1语法抽象语法图1给出了我们在本节中考虑的Reo子集中的连接器的抽象语法。在此图中，Reo连接器Sys（也称为电路或系统）由一组基本连接器实例BCI组成。每个基本连接器实例都从基本连接器类型BCT实例化，连接两个节点集。为了简化演示，我们将基本连接器实例的源节点收集在基本连接器类型的左侧，将其接收节点收集在其右侧，每个节点形成（可能是空的）节点集。我们用一个名字来标识每个节点，这个名字取自一个集合Names，典型的成员是A、B、C、.. 以及变量a、b、c、. . . 在他们之上徘徊。 变量ci、ci0、. 范围覆盖基本连接器实例和sys、sys0、. 从Reo系统的语法中提取术语。在没有混淆的地方，为了更简洁的表达，我们可以跳过系统和节点周围的大括号。 在这种情况下，必须记住通道实例和节点的顺序和重复是无关紧要的。BCT中的基本连接器类型代表以下直观性：(i) 同步连接器（）：同步连接器实例在每一端都有一个源节点和一个接收节点。它通过将数据项从源原子地（因此同步地）传递到接收器来同步其源和接收器。(ii) 同步漏极连接器（><）：一个同步漏极连接器实例同步地从它的两个源节点读取数据.它没有sink节点，因此它会丢失从其两端获得的所有数据项(iii) 同步有损连接器（−−·）：同步有损连接器有一个源节点和一个接收节点，并将接收节点与源节点连接，但不88M.R. Mousavi等人理论计算机科学电子笔记154（2006）83⊆- -- -- →−−联系我们−−反之亦然换句话说，它在其接收端阻塞读取器组件/连接器，直到写入器在源上写入数据项，但是如果读取器不存在，则写入器执行其写入操作并且数据项丢失。(iv) 一个空的一个位置FIFO连接器（Q）是定义异步架构的基本连接器。当一个数据项存在于这个连接器的唯一源节点时，它被带入FIFO缓冲器，缓冲器变满（用a表示），从而阻止进一步的写操作。只要缓冲器不为空，读取器就可以通过其接收节点(v) UnboundedFIFO connector （ [u] ） ： 一 个 unbounded FIFOconnector允许在其源节点和汇节点上进行异步操作，接受任意数量的连续写入，并允许读取，只要其缓冲器不为空。当前驻留在缓冲器内的数据项序列（可能为空）由u表示。(vi) 过滤连接器（pat）：过滤连接器，由模式pat参数化数据（其指定数据项的集合）将数据项从其源传送到其汇节点，如果数据项在（即，匹配）模式pat，否则从源接受数据项并丢失。(vii) Fork connector（<）：fork connector将数据从其唯一的源节点同步复制到其所有的sink节点。在本文中，我们只考虑具有一个源节点和两个汇节点的分叉连接器。然而，使用这个连接器，可以将具有更多接收节点的分叉连接器作为语法糖添加到我们的基本连接器类型集合(viii) 合并连接器（>）：合并连接器将数据项从其源节点之一同步传输到其唯一的接收节点。如果多个源节点有合适的数据项要操作，则非确定性地选择其中一个。同样，我们只考虑剩余部分中具有两个源节点和一个汇聚节点注意上面的分叉和合并连接器不是Reo通道。在本文中，我们使用它们来明确表示Reo节点（具有多个重合源或汇通道端）的行为中固有的复制和合并方面。因为我们在本文中没有处理Reo电路的动态重构，所以任何涉及具有多个重合源或汇通道端的节点的Reo电路总是可以转换为具有等效行为的另一个Reo电路，其中上述分叉和合并连接器的实例使其各自的固有复制和合并节点行为显式。由此产生的电路M.R. Mousavi等人理论计算机科学电子笔记154（2006）8389−−−−−−→−{}→涉及不超过一个重合源和/或汇信道端节点（本文中我们只处理这几种对抽象概念的限制我们的Reo子集的具体语法对图1中给出的抽象语法施加了一些额外的约束。这些约束条件分类如下：• 源和接收基数：基本连接器有不同的类型。基本连接器、Q、一、[u]和专利是类型1到 1，这意味着它们具有单个源节点和单个汇聚节点。 同步漏极连接器>是2到 0类型，这意味着它有两个源节点，没有汇节点。 叉形连接器是1到 2类型，其双重类型是的类型为2到 1（1到N分叉连接器和N到1合并连接器可以作为语法糖添加到我们的语言• 插入原则：连接器实例可以相互“插入”（即，通过将一个连接器的汇节点组合到另一个连接器的源节点来连接）。组合节点通过共享名称来表示，即，当一个连接器的接收器与另一个连接器的源具有相同的名称时，这两个连接器被连接。在我们的Reo子集中不允许其他连接方案。组合节点隐藏在我们的电路中（标记为hid（Sys）），不能用于插入其他节点。• 拥塞自由：电路的隐藏节点只能传递数据。因此，它们不能初始地或在电路缓冲器数据的任何稳定状态（即，包含非空数据序列）。换句话说，在Reo连接器的内部节点请注意，上述约束仅在Reo连接器的初始指定中有效，并且我们的SOS语义在电路执行定义1（源/宿/隐藏节点集）基于它们的直观含义，Reo连接器的源、宿和隐藏节点集归纳定义如下。(i) 对于一个基本的连接器实例ci=cnos0ct nos1（ct∈BCT），我们定义：hid（ci）=Δ\hid（ci）.nos0≠nos1，source（ci）=Δnos0\hid（ci）andsink（ci）=ΔNos1(ii) 对于电路Sys=ci<$SysJ：• hid（Sys）=Δsink（i））;hid（ci）hid（SysJ）（source（ci）sink（SysJ））（source（SysJ）90M.R. Mousavi等人理论计算机科学电子笔记154（2006）83⟨⟩→• source（Sys）=Δ （sou rce（ci）sou rce（SysJ））\hid（Sys）and• 汇（Sys）=Δ （sink（ci）sink（SysJ））\hid（Sys）.请注意，在上面的定义中，我们不排除指定循环Reo电路的可能性（即使对于基本连接器）。3.2语义Reo系统的操作状态由一对Sys，Val组成，其中Sys是Reo系统术语，语法定义如上，Val是节点上数据的赋值。每个节点上的数据赋值是一个有限的（可能是空的）数据序列，用DataSeq表示（空数据序列用[]表示）。 在数据序列上变化的变量由u、v、w表示，我们使用d-u（类似地，u-d）来表示数据项d到序列u的头（尾）的级联。DataSeq是一个定义每个节点的数据值的函数。 变量范围覆盖数据估值由σ，σJ，. . .定义2（一致性和数据值）一个系统在数据赋值下是一致的，如果该数据赋值为其每个隐藏节点分配一个空序列。观察基本连接器实例大多是一致的，因为它们通常没有隐藏节点。由两个连接器的并集产生的系统在数据赋值下是一致的，如果每个连接器在该数据赋值下是单独一致的，并且赋值将空序列分配给它们的每个共享（隐藏）节点。对于一致系统sys，当数据赋值被理解时，节点x的数据值由sys（x）表示。Reo连接器的结构操作语义的第一部分在图2中定义。这一部分涉及基本连接器实例的语义。第一个规则（Syn）通过将数据从其源节点复制到其汇节点来定义同步连接器的行为。请注意，数据是以先到先服务的方式处理的：数据从源节点序列的末尾获取（获取最旧的数据项），并放在相应的sink序列的开头表达σ σJ表示作为数据赋值函数的两个不相交部分的σ和σJ 规则（Synd）指定同步漏连接器读取数据当两个源节点都访问一个数据项时，数据在两个源节点上的存在是唯一的必要条件，并且两个数据项不需要相同。在规则 （LSyn0 ）和（LSyn1）中，我们指定了有损同步连接器的两种可能的行为过程，即，将数据从其源复制到其接收器，或者从其M.R. Mousavi等人理论计算机科学电子笔记154（2006）8391（Syn）a−→b，{a<$→u-d，b<$→v}σa−→b，{a<$→u，b<$→d-v}σ（Synd）<$（a，b）>−<$，{a<$→u-d，b<$→v-dJ}σ< $ →（a，b）>−（LSyn0）a−−·b，{a<$→u-d，b<$→v}σ< $ →a−−·b，{a<$→u，b<$→d-v}σ（LSyn1）a−−·b，{a<$→u-d，b<$→v}σ}a−−·b，{a<$→u，b<$→v}σ（OFifo0）a−Q →b， {a<$→u-d}σ<$→a−d→b，{a<$→u}σ（IFifo0）a−[u]→b，{a<$→v-d}σ< $ →a−[d-u]→b，{a<$→v}σ（OFifo1）a−d→b，{b<$→u}σa−Q →b， {b<$→d-u}σ <$（IFifo1）a−[u-d]→b，{b<$→v}σa−[u]→b，{b<$→d-v}σ（Filter 0）d∈pata−{pat}→b，{a<$→u-d，b<$→v}σa−{pat}→b， {a<$→u，b <$→d-v} σ（过滤器1）d∈/pata−{pat}→b，{a<$→u-d，b<$→v}σa−{pat}→b，{a<$→u，b<$→v}σ（叉）<$a−−（b，c），{a<$→u-d，b<$→v，c<$→w}σ< $ →<$a−−（b，c），{a<$→u，b<$→d-v，c<$→d-w}σ<$<（合并0）<$（a，b）>−−c，{a<$→u-d，b<$→v，c<$→w}σ<$ →<$（a，b）>−−c，{a<$→u，b<$→v，c<$→d-w}σ<$（合并1）<$（a，b）>−−c，{a<$→u，b<$→v-d，c<$→w}σ< $ →<$（a，b）>−−c，{a<$→u，b<$→v，c<$→d-w}σ<$92M.R. Mousavi等人理论计算机科学电子笔记154（2006）83图二. Reo语义：第1部分，基本连接器语义M.R. Mousavi等人理论计算机科学电子笔记154（2006）8393→（加入）sys0，σsys1，σjsys0<$sys1=<$$>x∈hid（sys0<$sys1）σJJ（x）=[]sys0sys0，σsys0<$sys < $x∈hid（sys）σJ（x）=[]（子系统）sys0，σ（Sys）syS0，σsys0sys1=sys2sys0sys1sys1sys2sys2，σ~sys0sys1sys0图三. Reo语义：第2一位FIFO和无界FIFO连接器的行为分别由规则（OFifo 0）-（OFifo 1）和（IFifo 0）-（IFifo 1）描述。规则（Filter0）指定过滤器可以传递pat中存在的数据项，规则（Filter1）显示如果pat中不包含数据项，则数据项将丢失。Fork连接器的行为在规则（Fork）中定义为将可用数据项从其源节点复制到其接收节点。类似地，规则（Merge0）和（Merge1）规定合并连接器将其源节点之一（如果两个源节点都有可用数据项，则不确定地选择）上可用的数据项复制到其接收节点。SOS Reo语义的第二部分如图3所示。在这一部分中，我们将详细说明系统的语义是如何由其子系统（最终是其基本连接器实例）的语义组成的。这种组合是以分层的方式呈现的，由三个层次组成第一个层次由规则（连接）描述。该规则规定，如果系统可以分解为两个不相交的部分，使得第一部分进行总转换，并反过来为第二子系统提供输入以执行其总转换，则系统可以执行总由于拥塞自由原则必须由我们的语义来维护，94M.R. Mousavi等人理论计算机科学电子笔记154（2006）83→⊆[aa]BD一FCE我们还在（Join）的前提中检查该总转换的结果在隐藏节点中不包含数据项。但是，由于Reo连接器的阻塞和同步约束，在Reo连接器中并不总是可以进行完全转换。因此，作为第二层，（Subsys）定义了Sys的子系统可以执行一致（部分）转换的标准，由Sys表示。最后，第三层，定义为（Sys），选择一个最大的（部分）转移，表示为~，并将其定义为系统的转移。注意，由于在一些基本Reo连接器中固有的非确定性，最大转换不一定是唯一的（即，合并）。Reo的操作语义是最小关系~，满足图2和图3。为了更好地说明我们的语法和语义，我们在下面的示例中指定了两个典型的Reo连接器，并使用我们的语义描述它们的转换。见图4。 复制器连接器示例1考虑图4所示的系统。在该图中，节点处的所有数据序列最初都是空的，但节点A的数据序列包含序列[aa]。根据图2和图3的语义，系统的第一步可以通过以下方式推导：（1）将第一个数据项传送到节点B和C，随后，（2）填充FIFO缓冲器，然后（3）将未决数据项从C移动到E，最后（4）将同一数据项从E移动到F。 因此，在第一步，整个系统这导致FIFO缓冲器中第一项的副本和节点F（电路的汇节点）中的另一个副本。通过研究语义，可以发现在下一步中只涉及系统的两个连接器（即FIFO和合并连接器）。因此，第二步导致将FIFO缓冲器内的数据项复制到节点F。我们已经使用第4节中描述的实现模拟了这个连接器的行为。M.R. Mousavi等人理论计算机科学电子笔记154（2006）8395⟨ ⟩ ⟨ ⟩∈≤↔3.3Reo电路定义相等和精化的概念是用转换系统语义推理形式主义的标准实践。在文献中存在几种不同的相等和修饰概念，它们被用于不同的目的[10]。在本节中，我们定义了以下初始无状态（双向）相似性的概念（遵循[12]），它将连接器的行为与数据序列的所有一致初始化联系起来。这个概念应该为我们提供了足够的工具，用它们更具体的实现来替换（部分）Reo电路定义3关系R称为Reo构形上的模拟关系，当且仅当对所有对（σSys0，σjj，σSys1，σJJ）∈R，σ=σJ，σ与Sys0和Sys1都相容，并且如果对某些相容的σJJ，σSys0，σjj~<$SysJ0，σJJ<$$> 则存在SysJ1使得<$Sys1，σjj ~<$SysJ1，σJJ<$ 且（SysJ0，σJJ，SysJ1，σJJ）R. 对称模拟关系称为互模拟关系当且仅当两个Reo连接器Sys和SysJ具有相同的源节点集和汇聚节点集并且存在（双）模拟关系R使得对于Sys SysJ（Sys SysJ），两个Reo连接器Sys和Sysj被称为初始无状态（双）相似，表示为SysSys j（Sys Sysj）。所有相容的σ，（σSys0，σSys1，σSys1）∈R.4工具支持为了机械化Reo模型的推理，我们已经将我们的操作语义转换为Maude重写逻辑。翻译是可能的，由于我们的语义的操作性质，并允许在Maude工具集中的Reo连接器的符号执行和模型检查。在本节中，我们将解释这一翻译的概要4.1Reo in Maude与大多数其他Maude规范一样，我们在Maude中的操作系统规范包括两种类型的模块：功能模块和系统模块。功能模块定义了我们规范的基本数据类型（集合，序列等）。以及对它们的操作（交集、连接等）。对于Reo语义，我们实现了三个功能模块：Node、Channel和System。这些模块除了定义上述基本分类和操作外，还定义了数据估值和配置等概念以及提取连接器的源、汇和隐藏节点等操作。96M.R. Mousavi等人理论计算机科学电子笔记154（2006）83Reo的Maude规范的第二部分是系统模块的定义。 这一部分将系统的动态不确定性行为具体化为重写理论。在我们的例子中，我们系统的原始行为是根据SOS规则指定的，因此我们必须将演绎规则转换为条件重写规则。对于我们语义学的公理，是一个简单的翻译：几乎相同的SOS规则可以用作Maude条件重写规则。例如，下面的重写规则是Maude中规则（Syn）crl[Syn]：*（a Syn b）-（a mapsto（u; d）），（b mapsto w）），sig）>=><（a Syn b）-（a mapsto u），（b mapsto（d ; w），sig）> if（d =/= emptyE1）。上面的规则是条件重写规则，其指定如果同步信道在其源节点上有一个非空的数据项序列，它将被重写到一个同步信道，第一个数据项被移动到它的sink节点（crl关键字代表条件重写规则，=>是重写的符号）。类似地，所有其他公理都是它们在操作语义中对应规则的副本（模语法变化）。在Maude中重写是模自反性、同余性和传递性，这三个问题都不利于SOS语义的实现。换句话说，在我们的语义学中，对于任何状态，自转换都是可能的，这是不正确的（因此，与反射性相矛盾）。 类似地，如果Reo电路的子系统可以执行总转换，则它可以在任何上下文中执行它（由于拥塞自由约束），因此与同余相矛盾，这不是情况。类似地，重写的传递性也对我们的语义有害。为了克服这个问题，我们在转换之前用 * 注释每个操作状态，以便我们可以区分到期的总转换SOS规则和那些由于一致性和传递性而导致的重写。我们使用相同的技巧来区分全部转移和部分转移，即通过用特殊的符号.例如，操作规则（Subsys）如下实现crl[Subsys]：*（sys0; sys1）-sig>subtranssys=>（sysp0; sysp1）-sigp>if（sys0 subseteq sys）/\* =>sysp0 -sigp0>/\（hidden（sys）isEmptyIn sigp）.为了翻译规则（系统），我们需要一种方法来指定否定前提（不可能转换或重写）。 为此，我们必须使用Maude的反射特征，它允许我们将重写理论解释为普通对象。通过这种方式，我们可以从元级别检查重写理论是否允许特定的重写。下面给出了Meta级操作和（系统）规则的代码M.R. Mousavi等人理论计算机科学电子笔记154（2006）8397Reo模型基本连接器实例单个重写步骤/时间总计行为重写/时间实施例143 .第三章。0×10/的。04s1 .一、8× 10/的。22s交织器6二、1× 10 /2. 9s 1 .一、2× 10/19. 3sExRouter8二、0×10/350秒四、1×10/818s表1模拟结果crl[System]：*sys0 ; sys1 - sig>=>（sysp0; sys1）-sigp>if*sys0 - sig>subtranss（sys0 ; sys1）=>sysp0 -sigp>/\不能在（sys 0; sys 1）中移动sys 0-sig>和sys 1。 Bool.ceq sysMove（T）=canMove？：：Result4Tuple如果可以移动？ ：= metaXapply（在上面的代码中，我们指定了一个Reo系统可以进行转换如果它的所有部分都可以参与过渡，或者它可以进行最大移动。最大移动谓词然后通过以下方式指定：元级函数sysMove，检查前面指定的Sybsys重写规则的某个实例是否适用。4.2仿真与模型检验在Maude中嵌入我们的操作语义之后，我们实现了示例1和另外两个示例中指定的Reo连接器，并模拟了它们的行为。 表1总结了重写的次数和用于模拟单个步骤的时间量，以及这些组件在大小为2的输入序列上的总行为（单个步骤语义的传递闭包）。时间是在一台配有奔腾700处理器和128兆RAM、运行Redhat Linux 7.3的个人计算机上测量的。我们还应用模型检查技术来验证[3]中详细描述的独占路由器连接器的行为，并验证其特征化LTL属性的正确性。重写引擎执行7. 4× 107重写耗尽状态空间，在同一台计算机上花了大约25分钟来模型检查正确性。我们参考本文的扩展版本[14]以获得示例和验证性质的细节98M.R. Mousavi等人理论计算机科学电子笔记154（2006）834.3从执行中我们的操作语义的Maude实现帮助我们获得了对其底层SOS语义的洞察力和信心。使用模拟工具包，我们能够观察不同连接器的行为，并将它们与它们背后的直觉相匹配。在几种情况下，我们能够在我们最初的SOS语义中找到错误或缺点。因此，我们相信，原型语言语义在模拟和模型检查环境，如Maude，是主要的帮助和重要性。Maude对于我们的目的来说是一个非常方便的选择，因为我们可以获得SOS规则到Maude重写规则的忠实翻译。这样，我们节省了大量的时间来证明我们翻译的正确性。因此，我们可以推荐Maude作为具有结构操作语义的形式主义和语言的快速原型环境。然而，从我们的模拟结果中可以看出，臭名昭著的组合爆炸，不允许使用基于模型（检查）的技术来分析任何实际系统的整体。一个可行的方法是使用组合验证技术，并结合模型检查和定理证明技术。5相关工作5.1协调和组成部分Reo可以被视为控制驱动协调语言Manifold的继承者Reo的主要优点之一是它支持连接器（和架构风格）的组合构造。Alfa [11]是一种架构描述语言，遵循类似于Reo的连接器隐喻，并使用Reo的基于自动机的语义来验证其组合软件架构的行为。我们在这里提出的想法也可以用于阿尔法的机械化和形式化。在[6]中，对于无状态连接符（例如，不包括FIFO连接符）的语言，给出了范畴语义和可靠且完整的等式理论（关于[9为Reo连接符找到合理和完整的公理化是未来研究的一个有趣主题（例如，关于本文中给出的初始无状态双相似性的概念）。5.2Reo语义在[4]中，Reo连接器的共代数形式语义是根据无限时间数据流上的关系开发的。 我们把这种语义看作是Reo的参考语义，因为它精确地指定了背后的初始直觉。M.R. Mousavi等人理论计算机科学电子笔记154（2006）8399REO连接器。 这种语义的声明性、关系性是一个 然而，它也使得它难以直接操作和执行模拟或模型检查等应用程序在[5]中，提出了一种基于自动机的形式主义，称为约束自动机，在约束自动机中，用表现出数据流活动的节点的名称来标记（例如， 读或写）和所涉及的数据项必须满足的约束方程。与[5]相比，我们的语义的一个优点是它使用了结构操作语义学的事实标准。这使得语义更容易为研究社区的其余部分所访问，并允许利用现有的理论和实现工具可用于SOS语义（如第4节所示）。此外，使用约束自动机来建模无界图元甚至具有无界数据域的有界图元是不可能的。有界的大数据域会导致约束自动机模型的爆炸，这会成为问题。然而，在SOS语义中，我们从实际的数据域中抽象出来，因此大的甚至无限的数据域都不存在问题。5.3SOS在Maude还有其他尝试将结构操作语义学翻译成Maude重写逻辑。在[17]和[16]中，CCS和LO-TOS的SOS语义分别被翻译成Maude.此外，模块化SOS（具有标签结构的SOS）到Maude的翻译在[8]中定义并在[7]中实现。受本文最初尝试的启发，我们最近将SOS的翻译推广到Maude，并在Maude中原型化SOS元理论的通用工具[13]。6结论在本文中，我们提出了一个结构化的操作语义的Reo。然后将此语义转换为Maude重写逻辑，以便从Maude周围可用的现有工具中受益。由于在相似性SOS和Maude的基本形式理论，所提出的翻译是相当直接的，并证明是一个忠实的代表性的原始语义。翻译允许系统设计人员评估基于组件的软件体系结构，通过动画和模型检查其相应的Reo连接器模型在Maude工具集正式。致谢。Michel Reniers对本文的早期版本提出了有益的评论。FOCLASA匿名裁判的评论100M.R. Mousavi等人理论计算机科学电子笔记154（2006）83研讨会也受到了热烈的欢迎。引用[1] Maude系统 可从http://maude.cs.uiuc.edu/。[2] F.阿巴布Reo：一个基于通道的组件组合协调模型。Mathematical Structures in ComputerScience，14（3）：1[3] F.阿巴布角Baier，J. J. Rutten，and M. Sirjani.用约束自动机对Reo中的组件连接器进行建模在FLOCASA'03的会议记录中25[4] F. Arbab和J. J. Rutten。 分量连接符的共归纳演算。 法律程序中的WADT'02，LNCS的第2755卷。pp. 34[5] C. Baier，M. Sirjani，F. Arbab和J. J. Rutten。用约束自动机对Reo中的组件连接器进行建模。计算机科学，2004年。出现。[6] R. 布鲁尼岛Lanese和U. 蒙塔纳里， 无状态连接器的完整公理 在CALCO'05会议记录出现。[7] C. D. O. Braga.重 写 逻 辑 作 为 模 块 化 结 构 操 作 语 义 学 的 语 义 框 架 。PhDthesis ，DepartamentodeInform'atica，Pon ti f'ıciaUni veradicationCat'olica deRio de Janeiro，Brasil，2001.[8] C.德·奥Braga，E. H. Haeusler，J. Meseguer，and P. D. Mosses：Mapping Modular SOS toRewriting Logic.Proceedings of LOPSTR[9] F. Gadducci和U.蒙塔纳里瓷砖模型。《证明、语言与互动：纪念罗宾·米尔纳的论文》（Proof，Language and Interaction：Essays in Honour of Robin Milner）一三三一六六。麻省理工学院出版社，2000年。[10] R. J. van Glabbeek 线 性 时 支 时 间 谱 2 。 在 大 肠 Best ， 编 辑 ， International Conference onConcurrency Theory（CONCURSpringer，1993年。[11] N. R. Mehta和N.梅德维多维奇 从建筑基元组成建筑风格。 在ESEC-FSE 03会议记录中，第347ACM SIGSOFT，2003年。[12] M. R.穆萨维，M。Reniers和J.F.格鲁特 SOS与数据一致。 法律程序中LICS'04，第302-313页。IEEE CS，2004年。[13] M. R. Mousavi和M. A.雷尼尔Maude中的SOS元理论原型。SOS'05会议记录出现。[14] M. R. 穆萨维， M. 西尔贾尼， 和F.阿巴布组件连接器的规范和验证。技术报告CSR-04-15，埃因霍温理工大学，2004年。[15] G. D.普洛特金操作语义学的结构化方法。Journal of Logic and Algebraic Programming（June），60（1-2）：17[16] A. Verdejo。建筑 工具 为 Lotos 象征性 Maude的语义学Forte'02会议录施普林格，2002年。[17] A. Verdejo和N. 我的天-奥列。在Maude 2中实现CCS。WRLA'02的出版物Elsevier Science，2002年。