Reo中约束自动机：组件连接器的模型检查与验证的语义模型

理论计算机科学电子札记97（2004）25-46www.elsevier.com/locate/entcsReo中构件连接器的约束自动机（延伸摘要）Farhad Arbaba，Christel Baierb，Jan Ruttena，c，MarjanSirjania，daCentrum voor Wiskunde en Informatica，Department of SoftwareEngineering Kruislaan 413，P.O.Box 94079，1090 GB Amsterdam，TheNetherlands{Farhad.Arbab，Jan.Rutten，Marjan.Sirjani} @ cwi.nlbInstitut für Informatik I，University ofBonn Römerstraße 164，D-53117 Bonn，Germanybaier@cs.uni-bonn.dec自由大学De Boelelaan 1081，1081 HV Amsterdam，荷兰谢里夫理工Azadi Ave.，伊朗德黑兰摘要Reo是一种外生的协调语言，用于基于通道演算的组件连接器的组合构造。构建自动化工具来解决诸如两个给定连接器的行为的等价性或包容性、连接器的行为的验证等问题，需要适合于模型检查的操作语义模型。在本文中，我们引入约束自动机，并提出他们作为一个语义模型的Reo。关键词：约束自动机，Reo，共代数语义，流，协调，组件，组合1介绍Reo是一种基于通道的外源协调模型，其中复杂的协调器（称为连接器）是由简单的协调器组成的Reo中最简单的连接器是一组具有定义良好的行为的通道，1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.04.02826F. Arbab et al. / Electronic Notes in Theoretical Computer Science 97（2004）25-C3C2C1C6C3C5C2C4C1C2C3C1用户[1]。Reo的重点是连接器、它们的行为和它们的组成，而不是通过它们连接、通信和合作的实体Reo中每个连接器的行为都对通过该连接器执行正常I/O操作的实体施加了特定的协调模式，而这些实体并不这使得Reo成为一种强大的ReoReo中的每个连接器依次由更简单的连接器组成，这些连接器最终由基本通道组成。例如，图1.a中的连接器实际上可能是流量调节器（如果其三个组成通道是正确的类型，如[1]中所述）。图1.a表示由两个写入器组件实例（C1和C3）和一个读取器组件实例（C2）组成的系统，它们通过我们的流量调节器连接器粘合在一起。每个组件实例都按照自己的时序和逻辑执行其I/O操作这些组件实例都不知道其他组件实例的存在，也不知道用于将其与其他组件粘合在一起的特定连接器的存在，甚至不知道它自己在组合系统中的角色尽管如此，我们的流量调节器粘合代码（参见[1]和[2]）所施加的协议确保了只有当C3写入数据项（其实际值被忽略）时，数据项才从C1传递到C2：C3写入的连接器的行为又独立于它所连接的组件：在它们不知情的情况下，它在C1、C2和C3之间强加了一种协调模式，该模式根据C3产生图1中的其他连接器实现了更复杂的协调模式。(a) 一个3路连接器（b）一个6路连接器（c）两个3路连接器和一个6路连接器Fig. 1. 部件和连接器Reo连接器的共代数形式语义在[2]中根据无限时间数据流上的关系发展。以这种语义为出发点，本文引入了约束自动机，并利用它们给出了一个可操作的C6C5C4F. Arbab et al. / Electronic Notes in Theoretical Computer Science 97（2004）25-27Reo中连接器行为的模型约束自动机可以被认为是概率自动机的概念概括，其中简单的约束，而不是概率，影响适用的状态转换。Reo中最重要的组合操作符join相当于该模型中自动机的一个产物。我们的约束自动机的概念是在I/O自动机和定时端口自动机的精神[6，3]。与此相反，我们不区分输入和输出端口（因此，我们不需要输入启用），并使用约束而不是特定的数据值。 与I/O或定时端口自动机不同，我们不遵循严格的时间同步方法，这在我们组成约束自动机时变得很重要。相反，约束自动机A1和A2允许在输入/输出端口发生数据时进行转换，自动机只从一个自动机Ai继承，而不涉及它从另一个自动机继承的转换或状态（因为在那一点上，时间，在其任何对应端口上都没有数据）。这样的转换不存在于本文的其余部分组织如下。第2节是对Reo的简要概述。在第3节中，我们定义了约束自动机，并通过描述一些简单的Reo通道的行为作为例子来展示它们的实用性。约束自动机和隐藏的产品，这是必要的模型Reo的连接运算符，定义并应用于第4节的几个在第5节中，我们研究了各种等价概念，为验证和推导Reo连接器属性的算法和工具奠定了基础我们在第6节中总结，暗示我们当前和未来在模型检查和自动化工具方面的工作，用于推理Reo连接器。2A Reo引物Reo为组件定义了许多操作，以便通过连接器（动态）组成、连接和执行I/O。原子连接器是通道。在REO中，通道的概念远比它的常见解释更普遍。通道是一种原始的通信媒介，它有两个端点，每个端点都有自己的唯一标识。有两种类型的信道端：数据进入的源端和数据离开信道的宿端。一个通道必须在其两端支持一组特定的基本操作，比如I/O;除此之外，Reo对通道的行为没有任何限制。这允许在Reo中同时使用一组开放的不同通道类型，每个通道类型都有自己的同步、缓冲、排序、计算、数据保留/丢失等策略。连接器是在节点和边的图形中组织的一组通道末端，28F. Arbab et al. / Electronic Notes in Theoretical Computer Science 97（2004）25-认为：• 零个或多个通道末端在每个节点上重合• 每一个通道末端都恰好在一个节点上重合• 在两个（不一定是不同的）节点之间存在边，当且仅当存在其一端在这些节点中的每一个上重合的通道。节点是Reo中的一个重要概念。不要与位置或组件混淆，节点是表示一组通道末端重合的基本拓扑属性的逻辑构造，其对这些通道末端之间和通过这些通道末端的数据流具有特定含义。a b c d e图二. Reo节点在节点N上重合的信道端的集合被不联合地划分为集合Src（N）和Snk（N），表示在N上重合的源信道端和宿信道端的集合。一个节点称为源节点，如果Src（N）/=Sn k（N） 。类似地，如果Src（N） =Sn k（N）/=，则N被称为汇聚节点。节点N是如果Src（N）/Snk（N）/，则称为混合节点。图2.a和b显示sink节点分别具有两个和三个重合的通道端部。图2.c和d分别示出了具有两个和三个重合通道端的源节点图2.e显示了一个混合节点，其中三个汇点和两个源通道端重合。Reo提供的操作使组件能够连接到源节点和接收节点并仅在源节点和接收节点上执行I/O;组件不能连接到混合节点、从混合节点读取或写入混合节点。一次最多只能将一个组件连接到一个（源或宿）组件可以将数据项写入它所连接的源节点。仅当在节点上重合的所有（源）通道末端接受数据项时，写入操作才成功，在这种情况下，数据项被透明地写入到在节点上重合的每个源末端。因此，源节点充当复制器。组件可以通过破坏性（take）和非破坏性（read）输入操作从连接到的汇聚节点获取数据项。只有当至少一个（汇）信道端在节点上重合时才能成功，如果多个重合信道端提供合适的数据一个汇聚节点，因此，作为一个（公平的）不确定性合并。混合节点是一个自包含的F. Arbab et al. / Electronic Notes in Theoretical Computer Science 97（2004）25-29通道结束并将其复制到其所有重合的源通道结束。只有当数据项可以被在混合节点上重合的所有源通道末端接受时，该数据项才适合于在迭代中选择因此，每个通道表示一个具有两个节点的（简单）连接器在Reo中，更复杂的连接器是使用其连接操作从简单的连接器构造出来的连接两个节点会破坏这两个节点，并生成一个新节点，在该节点上，它们的所有重合通道端点都重合。这个单一的操作允许任意复杂的连接器的结构，涉及从用户定义的通道类型的开放式分类中挑选的通道的任何组合连接符的语义被定义为其（1）组成通道和（2）节点的语义的组合通道的语义由提供通道的用户定义。Reo定义了上面提到的三种节点类型的语义。F在出来E BaB图三. 专用路由器和移位有损FIFO 1图3.a和b显示了两个Reo连接器。我们在第4节的例4.5和4.6中分别更详细地考虑这些连接子。在这里，我们使用它们来介绍我们的可视化语法，用于呈现Reo连接器图和一些常用的通道类型。这些图中的封闭粗框表示隐藏：框内的节点（及其边缘）的拓扑被隐藏并且不能被修改，产生具有多个输入/输出端口的连接器，表示为边界框的边界上的节点，其可以由框外的其他实体使用以与连接器交互并通过连接器交互。这些连接器中使用的最简单的通道是同步（Sync）通道，用简单的实线箭头表示。同步通道有一个源端和一个接收端，没有缓冲区。它通过它的源端接受一个数据项当且仅当它可以同时通过它的接收端分发它有损同步（LossySync）通道类似于XZMW UN一FIFO2F专用路由器CEDOB30F. Arbab et al. / Electronic Notes in Theoretical Computer Science 97（2004）25-同步通道，除了它总是通过其源端接受所有数据项如果它有可能通过其接收器同时分发数据项（例如，在其接收器上存在未决的Take操作），则信道传输数据项;否则数据项丢失。丢失同步信道被描绘为虚线箭头，例如，在图3.a中。图3.b中的边BD表示容量为1（FIFO 1）的异步通道，箭头中间的小方框表示其缓冲区。这个通道可以有一个初始空的缓冲区，或者如图3.b所示，包含一个初始数据值（在这种情况下，框中的类似地，图3.b中的边缘AF表示具有有界容量2（FIFO2）的异步FIFO通道，具有明显的语义。Reo中允许的更多外来通道的示例是同步排出通道（SyncDrain），其视觉符号分别在图3.a和b中显示为边缘XZ和ACSyncDrain通道具有两个源极端。由于它没有接收端，因此无法从该通道获得任何数据值。它通过它的一端接受一个数据项，如果一个数据项也可以通过它的另一端同时接受 。 此 通 道 接 受 的 所 有 数 据 都 将 丢 失 。 SyncDrain 的 近 亲 是 异 步 排 出（AsyncDrain）通道（图3中未显示）：它有两个源端，通过这两个源端它接受和丢失数据项，但不会同时进行。3用约束自动机Reo连接器的语义可以根据[2]中提出的定时数据流（TDS）的关系来定义。在本节中，我们将介绍约束自动机的概念，并通过将这些自动机的语言与定时数据流相关联，展示它们如何作为Reo连接器行为的操作模型在这里，与[2]一样，我们在创建和组成连接器时不考虑组件的动态行为。我们的重点是Reo电路，通过join和hide操作从基本连接器（通道和合并）构建，而不考虑join或split的进一步可能性。我们使用约束自动机来指定的操作语义的Reo，因为这使我们能够适应已知的方法进行分析的有限状态自动机与约束自动机。普通的有限自动机不足以表达Reo的语义。约束自动机允许我们对Reo连接器的微妙时序和输入/输出约束进行建模，特别是它们的同步和异步转换组合这反映在我们的约束自动机的定义中，我们将在我们的例子中进一步展示它。设V为任意集合。 我们定义V上所有流（无限序列）的集合V当V={|：{0，1，2，.. . } →V}。 为了方便起见，我们只考虑无限F. Arbab et al. / Electronic Notes in Theoretical Computer Science 97（2004）25-31++..G 布吕格G 布吕格行为和无限流，对应于我们的自动机的无限“运行”，省略了包括死锁在内的最终状态。我们将各个流表示为k=（k0，k1，k2，.. .）（或a=（a0，a1，a2，. .））.我们称之为初始值。流的（流）导数定义为：.）.注意，对于所有的n≥0，（n_J）n=_n+1我们还回顾了[2]中定时数据流的定义TDS=.⟨,a⟩ ∈ Data× IR|n ≥ 0：a，c<$其中（A，a <$，b <$，b<$，c<$）∈R在约束自动机中，隐藏运算符删除了关于C的所有信息。定义4.2 [隐藏在约束自动机上]设A=（Q，N，-→，Q0）是一个约束自动机，C∈N.约束自动机.ΣC[A]=Q，N\{C}， −→C，Q0，C定义如下。设~p是使得q~p的（转移）关系当且仅当存在有限路q{C}，g1{C}，g2{C}，g3{C}，gn−→q1 −→q2−→... −→qn其中eqn=p且g1， ... . ，g，n是可满足的（即， gi。 （参见E）。（注意，gi仅在C上记录笔。）初始状态集Q0，C为Q0<$p∈Q：q0~<$p，其中q0∈Q0 .转换关系−→C由下式给出：q~np，pN，gr，NJ=N\{C}/=，gJ=nC[g]式中，C[g]=Wd∈数据JJ−→Crg[数据（C）/d]。七问例如，如果Amerger表示图4中的merger自动机，则与异步排出的自动机相同注意，两个确定性约束自动机的乘积总是确定性自动机，而隐藏可以将确定性约束自动机变为非确定性自动机。然而，当用约束自动机对Reo网络进行建模时，可以从REOC[A]导出一个等价的确定性自动机det（C[A]）;参见备注3.2。例4.3[两个FIFO 1通道的合成]图5显示了如何通过乘积和隐藏从两个FIFO 1通道AFIFO 1（A，C）和AFIFO 1（C，B）获得FIFO 2通道AFIFO2（A，B）=CAFIFO1（A，C）daAFIFO1（C，B）7g[data（C）/d]表示通过将g中所有出现的data（C）替换为d而获得的DC。更准确地说，如果d = d j，我们将原子数据（C）=dJ替换为true，如果d/d=J，则替换为FALSE。38F. Arbab et al. / Electronic Notes in Theoretical Computer Science 97（2004）25-{A}{C}Q1P1Q2P2{C}{B}乘积自动机{A}q1q2p1q2{B}{C}{B}{A，B}q1 p2p1 p2{A}隐藏{A}q1q2{B}p1q2{A，B}{A}{B}{B}{A，B}q1 p2p1 p2{A}为了简单起见，我们处理一个单例数据域Data={d}，它允许我们跳过转换的DC。请注意，在FIFO 2（A，B）中，状态q1，p2不可达。原因是当数据元素从第一个通道的缓冲器移动到第二个通道的缓冲器时，通过C进入了q1，p 2。当我们从C的活动中抽象出来时，AFIFO 2（A，B）中可以跳过状态q 1，p 2（或者，它可以用状态p1，q2来标识）。Q图五. 两个FIFO 1通道引理4.4 [连接的正确性]设A1和A2是两个如上所述的约束自动机. 然后又道：(a) LTDS（A1daA2）=LTDS（A1）da LTDS（A2）。(b) 如果N1= N2，则LTDS（A1× A2）= LTDS（A1）<$LTDS（A2）。 Q等式LTDS（λC[A]）=λC[LTDS（A）]一般不成立例如，将B隐藏在图4中的合并自动机中会产生具有单个状态q、一个{A，C}转换和一个{C}转换的约束自动机因此，任何TDS-对（，a，，c），其中=且a=c属于可接受的语言B[Amerger]。另一方面，具有a=c的对（a，a，a，c）都不包含在F. Arbab et al. / Electronic Notes in Theoretical Computer Science 97（2004）25-39因为在每次定时运行的A合并中，数据经常出现在B和C上，而不是在A上。为了补救这种情况，我们需要添加公平性条件，声明哪些自动机转换必须无限进行经常（类似于Büchi自动机，见例如。[8]）。为了保持这个扩展的摘要简短，我们在续集中跳过这个细节。Example 4.5[Exclusive router]图3.a显示了一个Exclusive router连接器的Reo网络。到达输入端口F的数据项只流到输出端口B或E中的一个，这取决于哪一个准备消费它。输入数据永远不会复制到多个输出端口。8图3.a示出了通过组合两个LossySync通道（XM，XN）、一个SyncDrain（XZ）通道、一个合并器（Z的混合节点中固有的）和五个Sync通道（FX，MW，NU，ME，NB）来获得独占路由器ΣAXRouter（F，E，B）=ALossySync（X，M）×ALossySync（X，N）×ASyncDrain（X，Z）×Amerger（U，W，Z）×ASync（F，X）×ΣASync（N，U）×ASync（M，W）×ASync（M，E）×ASync（N，B）图6显示了我们的独占路由器的约束自动机是如何作为其组成通道的约束自动机的乘积获得的，然后隐藏其内部转换。Q例4.6[移位有损FIFO 1通道]图3.b显示了一个Reo网络，该网络用于一个连接器，该连接器的行为类似于具有移位丢失策略的有损FIFO 1通道。此通道称为移位有损FIFO 1（ShiftFIFO 1）。它的行为与普通FIFO 1通道相同，只是如果其缓冲区已满，则新数据项的到达会删除其缓冲区中的现有数据项，为新到达的数据项腾出空间。因此，该信道实现了“移位丢失策略”，丢失其缓冲区中最旧的内容以支持最新到达的内容。这与溢出有损FIFO 1通道的行为相反，FIFO 1通道的图3.b中的连接器由一个专用路由器XRouter（F，E，B）（如图3.a所示，并在示例4.5中解释）、一个合并器（8这个连接器的行为是Reo（汇或混合）节点在其多个输入上执行的合并中固有的原始非确定性选择的对应物，由图4中的合并器建模。40F. Arbab et al. / Electronic Notes in Theoretical Computer Science 97（2004）25-data（X）=data（M）{X，M}{X}data（X）=data（N）{X，N}data（Z）=data（U） data（Z）=data（W）{X}{X，Z}{U，Z}{W，Z}有损同步有损同步同步漏极合并数据（F）=数据（X）数据（N）=数据（U）{F，X}{N，U}data（M）=data（W）{M，data（M）=data（E）{M，data（N）=data（B）{N，B}同步同步同步同步同步乘积自动机{F，X，Z，M，W，E}数据（F）=数据（ X ） 数 据（ Z ） = 数 据（ W ） 数 据隐藏{F，X，Z，N，U，B}数据（F）=数据 （ X ） 数 据（ Z ） = 数 据（ U ） 数 据{F，E}data（F）=data{F，B}data（F）=data互斥路由器见图6。 通过合成基本Reo通道C的混合节点）、SyncDrain（AC）、初始满FIFO 1通道（BD）和初始空FIFO 2通道（AF）：AShiftFIFO1（A，B）=C，D，E，FΣAXRouter（F，E，B）×Amerger（E，D，C）×ΣASyncDrain（A，C）×AFIFO1（B，D）×AFIFO2（A，F）图7显示了ShiftFIFO1通道的约束自动机是如何通过乘积和隐藏从其组成部分的约束自动机中Q我们的乘积运算符依赖于用于构建交集有限自动机的标准构造，并且与用于类似模型的合成运算符具有相似性端口自动机的一对多合成[3]。另一方面，时间端口自动机的隐藏算子与我们的构造完全不同。前者不改变自动机的结构，但有一定的输出F. Arbab et al. / Electronic Notes in Theoretical Computer Science 97（2004）25-41数据（E）=数据（C）数据（D）=数据（C） 数据（F）=数据{E，C}{D，C}{F，E}{F，B}数据（A）=d数据（A）=d数据（F）=d合并前路由器数据（B）{A，{F}数据（F）=d{A}数据（A）=d{F}数据FIFO1{D}数据同步引流乘积自动机数据（A）=ddata（D）=data（C）{A，C，D}data（F）=data（B）{F，B}隐藏{A，C，E，F}数据（A）=d数据（F）=d数据（F）=数据数据（A）=d{A}数据{B}data（B）=d移位有损FIFO 1通道见图7。 通过合成其他Reo通道港口隐形相比之下，我们的构造删除了所有关于隐藏名称的信息（类似于删除普通非确定性有限自动机中的转换5互模拟与仿真对于标准标号变迁系统，约束自动机可以定义分支时间关系，如在Reo的上下文中，我们只对Reo网络（或约束自动机）诱导的语言感兴趣，而不是它们的分支行为。然而，分支时间关系是重要的，因为它们产生了语言等价/包含的另一种表征，以及验证两个自动机是否是语言等价的简单方法，或者一个自动机的语言是否包含在另一个自动机的语言42F. Arbab et al. / Electronic Notes in Theoretical Computer Science 97（2004）25-JQ1Q2Q3{A}{A}{A}数据（A）=d{A}数据（A）>d{A}{A}{B}{C}{B}{B}{C}{B}{C}P1R1P2P2'R2u3定义5.1 [互模拟]设A=（Q，N，−→，Q0）是一个约束自动机，R是Q上的等价关系。R称为A的互模拟，如果对所有对（q1，q2）∈R，所有R-等价类C∈Q/R，且每个N<$N：dc（q1，N，C）≠dc（q2，N，C）。状态q1和q2称为互模拟等价（记为q1<$q2）当且仅当存在一个互模拟R，且（q1，q2）∈R。Q通常，具有相同名称集合的两个约束自动机A1和A2被称为互模拟等价（记为A1<$A2）当且仅当对于A1的每个初始状态q0， 1，存在A2的一个初始状态q0， 2，使得q0， 1和q0， 2是互模拟等价的，反之亦然。在这里，A1和A2必须组合成一个见图8。 相似性和双相似性例5.2在图8的约束自动机中，状态q1和q2是双相似的，而q1，q2/q3。 为了解释为什么q1和q2是双相似的，可以建立一个包含（q1，q2）的互模拟。实际上，由分区Q/R=.Σ{q1，q2}，{q3}，{p1，p2，p2}，{r1，r2}，{u3}可以被证明是互模拟。请注意，例如，dc（q 1，{A}，{p 1，p 2，p J}）=真dc（q 2，{A}，{p 1，p 2，p J}）。2 2另一方面，q1和q2与q3不是双相似的。 原因是不存在从q1或q2可到达的与u3双相似的状态，因为dc（u3，{B}）=dc（u3，{C}）=真，而dc（r1，{B}）=dc（r2，{B}）=假且dc（p1，{C}）=dc（p2，{C}）=假。Q在图8的示例中，状态q1、q2和q3是语言等效的（即，我们有LTDS（A，q1）=LTDS（A，q2）LTDS（A，q3）），但是互模拟将它们区分为不等价的。对于非确定性约束自动机，互模拟比语言等价严格更精细。然而，对于确定性约束自动机，互模拟和语言等价是一致的。F. Arbab et al. / Electronic Notes in Theoretical Computer Science 97（2004）25-43定理5.3 [互模拟与语言等价]设A1和A2是两个同名集N的约束自动机。(a) 如果A1≠A2，则LTDS（A1）= LTDS（A2）。(b) 如果A1和A2是确定的，则A1≠A2当且仅当LTDS（A1）= LTDS（A2）。证据（a）容易核实。（b）的证明可以通过证明给定一个确定性约束自动机A =（Q，N，-→，Q0），关系R =。（q1，q2）∈Q×Q：LTDS（A，q1）=LTDS（A，q2）<$是互模拟Q Q我们现在通过模拟前序来提供语言包含的另一种表征，它可以被视为双向模拟的单向版本：定义5.4 [模拟]设A=（Q，N，−→，Q0）是一个约束自动机，R是Q上的二元关系。 R称为A的模拟，如果对所有对（q1，