没有合适的资源？快使用搜索试试~ 我知道了~
a1a2ab3理论计算机科学电子笔记159（2006）99-115www.elsevier.com/locate/entcsReo电路到约束自动机的自动映射Fatemeh Ghassemi，SamiraTasharo fi，Marjan Sirjani，，一德黑兰大学电子与计算机工程系，伊朗德黑兰B计算机科学学院，IPM，德黑兰，伊朗摘要为了输入Reo回路并生成相应的约束自动机，开发了一个工具。输入和输出的XML模式，建立一个通用的接口，生成一个集成的工具集。 提出了两种连接约束自动机的算法，并给出了实验结果。关键词：协调语言，基于组件的系统，Reo，约束自动机，工具设计1介绍Reo是在[5，2]中引入的，作为一种用于对基于组件的系统进行建模的协调语言模型中的组件使用Reo连接器进行外部协调。Reo中最简单的连接器是通道。REO通道通过节点连接，并组成更复杂的连接器。因此，Reo电路由组件、通道和节点组成。Reo的共代数语义模型在[6]中给出，其中连接器是无限时间数据流上的关系。约束自动机在[4]中基于时间数据流提出，其捕获操作1电子邮件：f. ece.ut.ac.ir2电子邮件：s. ece.ut.ac.ir3电子邮件：msirjani@ut.ac.ir1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.064100F. Ghassemi等人/理论计算机科学电子笔记159（2006）99Reo的语义约束自动机为Reo提供组合语义，其中每个Reo元素被映射到约束自动机，并且使用约束自动机的连接算法来构造整个电路的在Reo中对真实世界系统进行有效建模并使用约束自动机分析Reo为了进入Reo电路，将其映射到约束自动机，然后使用约束自动机分析模型的行为，需要一套集成的工具在本文中，我们提出了一个工具，RtC，用于输入XML格式的Reo电路，并将电路映射到约束自动机。该工具的输入也可以是要连接的多个约束自动机该工具的体系结构和接口设计的方式，以提供可扩展性，并在主要算法中使用的算法，以提供效率。为了开发该工具，为约束自动机定义了一个标准XML模式，并建立了该XML模式与Reo [ 7 ]现有标准XML模式的映射。Reo电路和约束自动机的标准XML模式在支持Reo的不同工具之间提供了一个公共接口在连接算法的实现中，使用了算法从多个自动机中选择两个自动机进行连接，并获得两个自动机的乘积。相关工作。除了Reo和约束自动化的理论工作外，还有一些工具提供的自动化支持在[10，9]中，提出了一种用于连接约束自动机的工具，该约束自动机用于建模和验证软件体系结构组件。此工具的输入和输出是文本格式，具有类似CSP的样式。连接算法只考虑转换，状态在获得乘积时不起作用RtC遵循[8]中的工作，增加了Reo到约束自动机的转换功能，并优化了连接算法。[8]中的连接实现的不精确性只适用于小的例子，这表明需要更好的算法和有用的算法。在[11]中，使用了另一种方法来自动推理Reo模型。在SOS [12]规则中提出了一种操作语义，并将其转化为Maude [1]重写逻辑。约束自动机不用于这种方法。本文是第一篇解释自动化Reo到约束自动机的映射的工具，用于集成支持Reo的工具集的标准接口F. Ghassemi等人/理论计算机科学电子笔记159（2006）99101论文的结构。第二节介绍了Reo和约束自动机。第3节使用一个简单的例子解释了该工具，第4节描述了该工具中使用的算法和我们的实验结果。第五节是我们的结论和未来的工作。2Reo和约束自动机Reo是一种基于通道演算的外生协调语言[2]。Reo由通过连接器连接的组件组成，这些连接器协调它们的活动。每个组件都是一个软件实现，其实例可以在物理和逻辑设备上执行原始连接器是具有两端的通道有两种类型的通道末端：源和汇。源信道端将数据接收到其信道中，而宿信道端将数据分发到其信道之外在任何给定时间，每个通道末端最多可以复杂的连接器是通过应用连接操作组合简单的连接器来构造的通道在节点中连接在一起，因此，节点是由一组通道末端组成的渠道类型。 Reo有不同类型的频道。通道可以具有源端和汇端、两个源端或两个汇端。本文中使用的一些基本通道类型如下：• 同步：这个通道有一个源和一个汇端，没有缓冲器。它通过它的源端接受一个数据项，同时它可以通过它的接收端分发它。• LossySync：此通道类似于Sync通道，不同之处在于它始终通过其源端接受所有数据项。如果它有可能通过其接收器同时分发数据项（例如，在其接收器上存在未决的Take操作），则信道传输数据项;否则数据项丢失。• SyncDrain：此通道有两个源端。它通过其一端接受数据项，同时也可以通过其另一端同时接受数据项。此通道接受的所有数据都将丢失。• FIFO-n：该通道具有源端和接收端，以及具有n个数据项的容量的有界缓冲器。接受的数据项保存在通道的内部FIFO缓冲器中。通道接收端的适当I/O操作以FIFO顺序获取缓冲器的内容102F. Ghassemi等人/理论计算机科学电子笔记159（2006）99节点类型。Reo中的节点分类为：• Sink节点：节点中的所有通道末端都是sink。仅当至少有一个重合通道结束或中断数据项时，来自此节点的take操作才成功如果有多个通道结束于较短的数据，则非确定性地选择一个一个汇聚节点，因此，作为一个（公平的）不确定性合并。• 源节点：节点中的所有通道末端都是源。只有当节点中的所有源端都接受数据时，对它的写操作才成功，在这种情况下，数据被透明地写入到与节点重合的每个源端。因此，源节点充当复制器。• 混合节点：它同时包含sink和source通道端。它在无限循环的原子迭代中结合了sink节点和源节点的行为：在每次迭代中，它非确定性地选择并获取由其一致的sink通道端之一访问的合适的数据项，并将其复制到其所有一致的源通道端。只有当数据项可以被在混合节点上重合的所有源通道末端接受时，该数据项才适合于在迭代中选择Reo提供了一些操作，使组件能够在sink和source节点上连接和执行I/O请注意，组件不能连接到混合节点、从混合节点获取数据或向混合节点写入数据。一次最多只能将一个组件连接到一个（源或宿）节点I/O操作通过不同组件之间的接口节点执行，我们称之为端口节点。约束自动机[4]被提出作为Reo的组合语义基于定时数据流[6]。定时数据流的每个元素是一对时间和一个数据项，其中时间指示数据项何时被输入或输出。如果一个转换在组件的端口中观察到数据项，则它会触发，并且根据观察到的数据，自动机可以改变其状态。约束自动机（在数据域Data上）是元组A=（Q，Names，-→，Q0），其中Q是状态的有限集合，N ames是状态的有限集合。名字的有限集合，−→是Q×2名字×DC×Q的有限子集，称为A的跃迁关系，Q0<$Q是初始状态的集合从简单的连接器构造复杂的连接器，是通过Reo中的join操作完成的连接两个节点会破坏这两个节点，并生成一个新节点，在该节点上，它们的所有重合通道端点都重合。Reo中的每个通道和合并节点都映射到一个约束自动机。图1中描述了这种映射的一些示例（摘自[4]）。Reo中最重要的一个组合操作符join相当于自动机的一个乘积。两个约束自动机A1=（Q1，Names1，F. Ghassemi等人/理论计算机科学电子笔记159（2006）99103−→Fig. 1.约束自动机的一些基本的Reo通道，并合并节点−→1，Q0，1）和A2=（Q2，Names2，−→2，Q0，2），是[4]：A1daA2=（Q1×Q2，Names1<$Names2，−→，Q0，1×Q0，2）其中−→由以下规则定义N1，g1N2，g2q1−→ 1p1，q2−→ 2p2，N1<$Names2= N2 <$N ames1q，q<$N1<$N2，g1<$g2普岛12−−−−−−−−→12和年q1N，g1 p1，NNames2=N，g<$q1，q2<$−→ <$p1，q2<$以及后者的对称规则。Q第一条规则适用于自动机中有两个可以一起触发只有当两个自动机中没有共享名称时才会发生这种情况，该名称存在于其中一个转换中，但不存在于另一个转换中。在这种情况下，结果自动机中的转换具有两个转换上的名称的并集，数据约束是两个转换的数据约束的合取第二条规则适用于104F. Ghassemi等人/理论计算机科学电子笔记159（2006）99当一个自动机中的转换可以独立于另一个自动机被触发时，这发生在转换上的名称不包含在另一个自动机中时。在连接操作之后，可以在结果自动机中隐藏。隐藏抽象了Reo电路中通道之间的内部通信细节有限状态自动机和标记转移系统可用的模型检查和分析方法可以适用于约束自动机[4]。3RtC工具RtC是将Reo自动转换为约束自动机的工具Reo电路可以包括不同的通道类型以及黑盒组件。RtC中提供了一组原始通道的相应约束自动机Reo通道和约束自动机的输入和输出格式基于其相应的标准XML模式[7]。 RtC在Java中实现，并使用约束自动机连接操作将Reo电路映射到约束自动机。 代替输入Reo电路，用户可以输入多个约束自动机并直接执行连接和隐藏操作。图2显示了RtC工具的用例图图二. RtC工具RtC工具的UML组件图如图3所示。命令解释器包用于解释用户的命令及其参数，并在遇到错误时提供适当的这个解释器使用Automaton包来解析自动机F. Ghassemi等人/理论计算机科学电子笔记159（2006）99105并执行自动机相关的操作，如连接和隐藏。命令解释器还使用ReoCircuit包来解析Reo电路XML并将其转换为相应的自动机。Digester包用于根据模式解析XML文件。图三. RtC工具3.1XML格式的Reo和约束自动机在下文中，我们简要地解释了Reo和约束自动机的XML格式，然后展示了一个例子。Reo电路的XML规范Reo电路以XML格式定义，并根据标准Reo模式进行验证[7]。每个Reo电路由XML文件中的电路元素定义 电路元素由两个子元素组成，分别称为头元素和体元素。头部元件包含连接器元件，该连接器元件用于定义将连接到外部通道端的电路中的通道端。体单元是一个复合单元，其组成元素是通道、节点和组件。 每个通道和节点都由Reo的标准XML模式中的一些预定义类型指定。每个节点通过定义其重合的通道末端来描述。每个通道通过定义其两个通道端来描述通过为其分配唯一标识符（编号）来定义通道末端在组件的元素中，我们可能有多个连接器实例。这些是存在于文件中的预定义连接器的实例106F. Ghassemi等人/理论计算机科学电子笔记159（2006）99约束自动机的XML规范约束自动机也以XML格式定义，可用作工具的输入或输出此XML文件由[8]中提供的相应模式验证 每个约束自动机都由一个gxl元素定义，该元素的类型为graphType。 每个graphType由两个元素定义;节点和边缘元素分别用于定义自动机的状态和转换。节点元素是一个简单的元素，由一个属性名组成。边缘元素是由两个元素组成的复合元素，信号和约束，分别用于定义转换的名称和数据3.2例如在本节中，我们将展示一个简单的Reo电路及其XML规范，以及其对应的约束自动机的XML。我们还简要地解释了两个XML规范之间的映射。Reo电路称为双定序器，如图4所示。见图4。 双定序器Reo电路该电路同时接收来自通道端A和B的数据，并以AB格式对它们进行排序。因此，相应自动机的接受语言是（AB）。该电路具有三个端口节点n1、n2和n6，每个端口节点分别包括通道端1、3和12如上所述，这些通道末端在XML定义的头元素中定义，如图5所示。内部节点和通道在电路的主体元件中定义，如图6所示。通道末端1、3和12同时触发，而在通道末端1和3上有写操作，在通道末端12上有取操作信道端1上的数据令牌A由信道端12取得，并且数据令牌A由信道端12取得。通道端3的令牌B保留在FIFO 1中（如图4中的c4所示）。当信道端12执行另一个take操作时，数据令牌B被F. Ghassemi等人/理论计算机科学电子笔记159（2006）99107<？XML version=“1.0”encoding=“UTF-8”？>
