使用符号执行的Reo电路自动分析和程序验证技术 2009年的论文研究.

理论计算机科学电子笔记255（2009）137-158www.elsevier.com/locate/entcs使用符号执行的Reo电路自动分析Bahman Pourvatan1计算机工程系，Amirkabir University of Technology，Tehran，Iran LIACS，LeidenUniversity，NetherlandsMarjan Sirjani2冰岛雷克雅未克大学计算机科学学院德黑兰大学，德黑兰，伊朗Hossein Hojjat瑞士洛桑联邦理工学院Farhad Arbab4LIACS，莱顿大学，荷兰，CWI，荷兰摘要Reo是一种协调语言，可用于对不同的系统进行建模。我们提出了一种使用约束自动机符号执行Reo电路的技术，更具体地利用它们的数据约束。 这种技术使我们能够获得数据之间的关系通过不同的电路中的节点，并且还推断协调模式。作为构造符号执行树的替代方案，我们提出了一种类似于用于将确定性有限自动机转换为正则表达式的算法的算法。我们的技术可用于分析数据主导的系统，而模型检测方法最适合于控制主导的应用程序的研究。 还可以检查可能涉及数据值的死锁。我们说明了一组数据占主导地位的电路，以及一个非平凡的临界区问题的技术。一个工具实现自动化所提出的技术。关键词：符号执行，Reo，约束自动机，协调语言，程序验证。1电子邮件地址：pourvatan@aut.ac.ir2电子邮件：marjan@ru.is3电子邮件：hossein. epfl.ch4电子邮件：farhad@cwi.nl1571-0661 © 2009 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.10.029138B. Pourvatan等人/理论计算机科学电子笔记255（2009）1371介绍Reo [1]是一种外生协调语言。在Reo中，复杂的连接器由简单的连接器组成。 Reo中最简单的连接器是一组 具有良好定义行为的通道。REO连接器在视觉上表示为类似于电子电路的电路，并显示组件如何互连。Reo的重点是连接器，以及组件之间的同步和通信，而不是组件的内部行为。约束自动机[3，7]被引入作为Reo的组合语义。利用约束自动机（CA）可以分析Reo电路的行为Reo是作为一种协调语言引入的，它可以用于各种应用程序。Reo和约束自动机在[4]中被用作ADL（架构描述语言），它们可以用于建模硬件和系统级设计[20，21]，以及建模Web服务[24，25]。在这些应用中，Reo通常用于表示通信和同步，而约束自动机用于对组件进行建模。通过这种方式，整个系统的行为可以使用其组成部分的约束自动机组合地构造。为了分析Reo电路，在[13]中提出了模型检查器。我们的符号执行技术和工具构成了一个更简单，但功能强大，更有效的分析器，可以作为替代或扩展，这个模型检查器。在适用的情况下，它可以用来推导电路的符号输出，这也可以以比模型检查更少的计算成本揭示可能的死锁/活锁。而在模型检查中，您可以表达更复杂的属性并为其分析支付更高的计算成本，Reo电路的符号执行可以有效地用于例如当Reo用于建模硬件和系统设计时。类似的技术可以用于Reo和CA的切片缩减和测试用例生成符号执行背后的主要思想[12]是使用符号值而不是实际数据作为输入值，并将程序变量的值表示为符号表达式。因此，由程序计算的输出值被表示为符号输入值的函数[11]。虽然符号执行工具与模型检查器相当，但它们主要用于数据主导的应用程序，而不是控制主导的应用程序。数据主导的应用程序的复杂性不一定来自复杂的数据结构和数据类型。相反，它们的复杂性来自于应用程序中数据项之间的非平凡的相互依赖性。对于Reo电路的符号执行，我们使用约束自动机，这允许我们使用自动机理论领域中的已知算法和技术。对于约束自动机，我们考虑执行路径，这是从程序的入口到出口的路径，作为从初始状态返回到初始状态的路径（或运行）。CA的状态。在Reo的上下文中，这意味着所有启用的节点被触发，电路返回到其初始配置，即，完成事务、交互模式或协调任务。为了简单起见，B. Pourvatan等人/理论计算机科学电子笔记255（2009）137139失去一般性，我们考虑确定性约束自动机，具有一个单一的初始状态。 假设初始状态为”[19]《明史》：“国也。为此，我们定义了一组与CA相关的正则表达式，考虑了同步和同步在CA中的建模方式，并展示了如何在正则表达式中表示数据约束。我们的方法依赖于不同的执行路径中的数据约束的操作。执行符号执行的两个主要困难是（1）处理复杂的数据结构和数据类型;（2）处理可能无限数量的符号执行路径。最初，我们从复杂的数据结构和数据类型中抽象出来，因为它们在Reo和约束自动机中没有定期考虑，我们专注于导出数据之间的非平凡相互依赖关系。代替处理无限数量的执行路径，这里我们遍历每个周期一定次数，这取决于在它们的传递关系中的存储器单元（每个周期中的存储器单元）之间的最长路径的长度 通过出现在相同的数据约束中而处于关系中），产生有限数量的路径。 这就足以给出输入元素之间的关系并且输出数据流通过电路（用符号表示）。工作的贡献。 我们提供了一个自动化的分析技术和支持工具的Reo电路的符号执行方法的基础上。 REO用于不同的应用程序，但只有少数工具提供其分析[15，13]。虽然我们的技术不支持验证时序逻辑属性，erties，它提供了可达性分析，并可以揭示可能的死锁/活锁，这通常是最有趣的设计师的属性。该技术还可以根据其输入数据导出电路的符号输出，从而导出协调模式。这一切都可以高效地完成，并且比模型检查的计算成本更低。此外，由于我们的技术是基于变量的符号表示，而不是实际值，因此它不需要数据域是有限的，而在模型检查中，变量的实际值需要被考虑。据我们所知，这是第一个在CA中使用数据约束进行分析的工作。为此，我们定义了与CA相关的正则表达式集，并考虑了数据约束。我们的工作对符号执行社区也很有趣。 我们从自动机而不是代码开始，因此，我们可以使用生成正则表达式并展开表达式的巧妙方法，而不是构建符号执行树。我们提出了一个解决方案的潜在无限数量的符号执行根据语义的Reo电路。纸的计划本文的其余部分组织如下：第2节是对 Reo和约束自动机在第3节中，我们解释了Reo电路的符号执行方法。第4节载有一些案例研究。 相关工作见第5节。在第6节中，我们讨论了未来的工作，并总结了论文。140B. Pourvatan等人/理论计算机科学电子笔记255（2009）1372Reo和约束自动机Reo是一个以组合方式构建组件连接器的模型[1]。它允许对这些连接器的行为进行建模，对它们进行形式化推理，一旦证明正确，就可以从规范中自动生成所谓的胶水代码。Reo中的每个连接器依次由更简单的连接器组成，这些连接器最终由基本通道组成通道是一种原始的通信媒介，它有两个端点，每个端点都有自己的唯一标识。有两种类型的信道端：数据进入的源端和数据离开信道的宿端。一个通道必须在其两端支持一组特定的基本操作，比如I/O;除此之外，Reo对通道的行为没有任何限制。这允许在Reo中同时使用的一组开放式的不同通道类型，每种通道类型都有自己的同步、缓冲、排序、计算、数据保留/丢失等策略[1]。通道连接成一个回路。连接（或加入）通道是将通道末端放在节点中。因此，节点包含一组通道末端。节点的语义取决于其类型。根据其重合通道端点的类型，节点可以具有以下三种类型之一。 如果所有重合通道结束在一个节点上，只有源（或汇）信道端，该节点被称为源（相应地，汇）节点。否则，它被称为混合节点。组件可以将数据项写入它所连接的源节点。仅当在节点上重合的所有（源）通道末端接受数据项时，写入操作才成功，在这种情况下，数据项被透明地写入到在节点上重合的每个源末端。因此，源节点充当复制器。组件可以通过输入操作从其连接到。只有当至少有一个（汇）通道结束在节点上重合时，take操作才会成功，否则会生成合适的数据项;如果有多个重合通道结束生成合适的数据项，则会不确定地选择一个。因此，汇聚节点充当非确定性合并器。混合节点非确定性地选择并获取由其重合的汇通道端之一所接收的合适的数据项，并将其复制到其所有重合的源通道端中。Reo o表示一组开放式通道，但表示一组原始通道（及其相应的CA）通常用于Reo电路。 Reo中每个连接器的行为都对通过该连接器执行正常I/O操作的实体施加了特定的协调模式，而这些实体不知道这些模式。这使得Reo成为一种强大的粘合语言，用于连接器的组合构造，以将组件实例组合到软件系统中，并外生地编排它们的相互交互。2.1约束自动机：Reo约束自动机在[3]中作为Reo连接器的形式语义提出，基于[5]中给出的共代数语义。使用约束自动机作为Reo连接器的操作模型，自动机状态代表可能B. Pourvatan等人/理论计算机科学电子笔记255（2009）137141− → × × ×A−→∈A∈|配置（例如，Reo连接器的FIFO通道的内容），而自动转换表示可能的数据流及其对这些配置的影响。[1]中提出的Reo操作语义可以用约束自动机加以改造。给定Reo连接器的约束自动机可以以组合的方式导出。为此，提供了与Reo连接器原语相对应的约束自动机在[3]中，约束自动机定义如下：定义2.1[约束自动机]约束自动机（在数据域Data上）是元组A =（Q，Names， −→，Q0），其中• Q是一组状态，• 名字是有限的，•是Q2NamesDCQ的子集，称为的转移关系，其中DC是数据约束的集合• Q0是初始状态的集合。我们写qN，g p代替（q，N，g，p）∈−→。我们称N为名称集，g为转型的守护者对于每一个跃迁qN，g p，我们要求（1）Ni = 0，（2）gDC（N，Data）。 它被称为有限的，数据有限。−→−→和底层数据域数据约束：数据约束由以下语法定义[3]：G：：=假 |真 |ε |d =d|格沃格|格沃格这里，n表示名称，d表示数据。 我们假设一个全局数据域Data用于所有名称。 或者，我们可以将数据域DataA分配给每个名称A并且在数据约束的定义中需要类型一致性。数据约束（DC）可以看作是一组名称-数据-赋值。我们经常使用派生的DC，例如dA/=d或dA=dB。符号=代表明显的满意度关系，这是由于对名称-数据-分配的DC进行解释而产生的。对DCs的满足性、有效性、逻辑等价性、逻辑蕴涵≤等进行了定义。我们现在解释如何约束自动机可以用来模拟可能的 Reo电路中的数据流。为了为Reo电路提供一个组合语义，我们需要每个基本通道连接器和自动机操作的约束自动机来模拟Reo操作的连接和隐藏行为图1显示了合并节点和标准基本通道类型的约束自动机：A同步，（图1.a）通道有一个源（A）和一个汇（B）端。它通过它的源端接受一个数据项，同时它可以通过它的接收端分发它。 通道SyncDrain如图1.b所示。是具有两个源端（A和B）的通道。 它通过一个一个数据项也可供它同时接受，另一端也是。此通道接受的所有数据都将丢失。图1.c是LossySync通道。此通道也类似于同步通道，除了142B. Pourvatan等人/理论计算机科学电子笔记255（2009）137为同步一（一）B{A，B}d_A = d_B一SyncDrain{A，B}（b）第（1）款BLossySyncAB{A，B}d_A = d_B{A}（c）第（1）款{A}d_A一专利滤波器专利（d）其他事项B{A，B}d_APatd_A = d_B一FIFO1{A}、d=d_A{B}，d_B = d（e）BMergerNode一个CB{A，C}d_A = d_C{B，C}（f）d_B = d_C图1.一、 Reo原始通道和合并节点及其确定性约束自动机它总是通过其源端（A）接受所有数据项。 如果可能的话为了同时通过它的接收器（B）分配数据项，信道传送数据项;否则数据项丢失。图1.d中所示的滤波器通道的行为类似于同步，只是它会丢失与滤波器的指定模式不匹配的所有数据（图中的Pat FIFO1通道（图1.e）有一个源端（A）和一个接收端（B），以及一个容量为1个数据项的有界缓冲器（图中的方框）。接受的数据项保存在通道的内部FIFO缓冲器中。通道接收端的适当I/O操作以FIFO顺序获取缓冲器的内容。 一个合并节点，如图所示-步骤1.f，非确定性地选择来自通道端A或B之一的输入，并将其传递到通道端C作为合并器输出。乘积运算符是在约束自动机上定义的，它捕获了Reo的连接运算符的两个约束自动机A1 =（Q1，Names1， −→1，Q0，1）和A2=（Q2，Names2， −→2，Q0，2）的乘积自动机是[3]：A1daA2 =（Q1 ×Q2，Names1 <$Names2， −→，Q0，1 ×Q0，2）其中− →由以下规则定义qN1，g1N2，G21−→1p1，q2 −→2p2，N1 <$Names2 =N2<$Names1q，qN1<$N2，g1<$g2p，p和12⟩ −−−−−−−−−→⟨12N，gq1−→ 1p1，NN ames2N，g<$q1，q2<$−→ <$p1，q2<$以及后者的对称规则。第一条规则适用于自动机中有两个可以一起触发的转换。只有当两个自动机中没有共享名称时才会发生这种情况，该名称存在于其中一个转换中，但不存在于另一个转换中。 在这种情况下，结果自动机中的转换具有联合在两个转换上的名称中，数据约束是两个转换的数据约束的结合。 第二条规则适用于一个自动机中的转换可以独立于另一个自动机被触发时，这发生在转换上的名称不包含在另一个自动机中时。后B. Pourvatan等人/理论计算机科学电子笔记255（2009）137143无无无无无无无−→NpN可以完成隐藏在结果自动机中的连接操作。隐藏抽象了Reo电路中通道之间的内部通信细节，并显示了Reo电路的可观察行为对具有状态记忆的约束自动机（CASM）进行了扩展，将ames显式地划分为三组amessrc， 埃姆斯snk，和 ames混合并扩展数据约束以适应状态存储器单元[2]。在这里，我们使用一种稍微简化的CASM形式，使用状态存储器并省略名称集的分离。正式定义如下：定义2.2（具有状态记忆的约束自动机（CASM））。具有状态记忆的约束自动机是元组A=（Q，Names， −→，Q0， M， V0），其中[2]：• Q、Names、−→和Q0的定义与普通CA相同• M是被划分成存储单元Mq的存储单元的集合，对于所有q ∈ Q。• 对于每个q ∈ Q，当自动机处于状态q时，定义了值函数Vq：M q→ Data。集合V0由初始值函数Vq0组成，每个初始值函数Vq0给出其对应的初始状态q0∈ Q0的初始值。• 数据约束语言被扩展以包括转换的源和目标状态的相对化存储单元名称（s.m和t.m，对于m∈ M），以及N，g对于节点名n∈ Names，通常为dn，使得对于每个转移q p，g的自由变量在集合{s.m|m ∈ M q}<${t.m|m ∈ M p}<${d n|n ∈ N ames}。• 给定数据分配δN：N→Data和值函数Vq：Mq →Data，跃迁qN，g p是可能的，只有当存在一个价值函数V：男→数据such在映射δ，V下g−is→真p p和Vq. 启动过渡，使Vp成为状态p的存储单元Mp的值函数。数据约束根据以下语法编写g：：=假|真|ε |d = d |g ν g|g∧g|t< m>= d< n>|d< n>= s< m> | d< n>= d< n> |d< n>= v其中，m的范围遍及存储器单元，n的范围遍及ames，并且v的范围遍及数据集Data。特殊符号s和t分别表示转换的源状态和目标状态：转换的数据约束g中的名称sx和txN，gq-→p分别指存储单元q.x和p.x。因此，数据约束通过形式s x或t x的相对引用（与明确的存储器单元名称q.x相反），或p.x）。这有两个好处。 首先，它使得转换不可能引用除其自身的源或目标之外的任何状态的存储器单元。 第二、它通过消除做任何特殊事情的需要来简化产品操作（例如，名称替换）时，我们结合同步转换。我们可以看到两个FIFO 1（缓冲器容量为1的FIFO）通道的CASM144B. Pourvatan等人/理论计算机科学电子笔记255（2009）137图二、具有状态记忆的（a）FIFO 1和（b）FIFO 2约束自动机在图2（a）中。在此图中，x和y是两个FIFO 1通道的内部缓冲器。连接两个FIFO 1通道，将一个通道的接收端与另一个通道的源端放在同一个节点上（在此图中为节点B），得到一个FIFO 2（缓冲器容量为2的FIFO）通道，如图2（b）所示。两个通道的约束自动机的乘积给出了FIFO 2通道的约束自动机。在这个例子中，我们看到了存储单元值的数据约束每个状态的状态被称为转换的目标和源;以及数据如何通过Reo电路的缓冲器并相应地通过CASM的状态被传递地描述3Reo电路的符号执行符号执行背后的主要思想是使用符号值而不是实际数据作为输入值，并将程序变量的值表示为符号表达式。因此，由程序计算的输出值被表示为输入符号值的函数符号执行是正常执行的自然扩展，将正常计算视为特殊情况[12]。在传统的命令式编程语言的情况下，语言的基本运算符的定义被扩展为接受符号输入值并产生符号公式作为输出。例如，赋值语句右侧的表达式是求值的，可能用多项式表达式替换变量。结果是一个多项式（整数是平凡的情况），然后将其指定为新值在赋值语句的左边符号执行程序的状态包括程序变量的符号值、程序计数器和路径条件。 的路径条件符号执行树是符号输入值上的无量化器布尔公式;它累积输入值必须满足的约束，以便执行遵循其特定的关联路径。符号执行树表征程序符号执行期间遵循的执行路径。该树中的节点表示程序状态，弧表示状态之间的转换[18]。B. Pourvatan等人/理论计算机科学电子笔记255（2009）137145∈∈--3.1CA、TDS和ReoReo连接器的共代数形式语义，在[5]中给出，为任何Reo连接器分配一个无限时间数据流上的关系，称为其TDS语言。 这种语言可以用于Reo的符号执行和获取电路的输入值和输出值之间的一种符号关系。为了对TDS语言进行推理，我们可以将约束自动机视为定时数据流集合的接受者。如第2节所示，约束自动机的转换被标记为由非空子集N = A1，...，一个n的节点和一个数据约束g。数据约束可以被看作是一组数据分配的符号表示数据分配是从名称集合N到数据域Data的函数。记法dA=d表示d Data对名称AN的赋值。形式上，数据约束是从原子dA=d构建的命题公式，其中数据项d被分配给端口A。在本文中考虑的所有原始Reo通道中，我们从d的具体值中抽象出来。在通过端口的数据元素中，我们只有相等（而不是赋值）。此外，唯一使用的布尔连接器是与连接器。原始的Reo通道（以及它们的产品）满足此属性。为了简单起见，我们只考虑具有单个初始状态的确定性CA我们的方法。在CA中，我们用符号表示输入和输出值，而不是特定的数据值，转换显示它们之间可能的关系。这使得CA成为构建符号执行工具的适当基础。在这里，我们使用数据约束来推导输入值和输出值之间的关系。问题是获得输出值和输入值之间的可能关系，用符号表示。为此，我们需要使用其约束自动机获得给定Reo电路的符号执行树中的执行路径。如果电路的CA中存在循环，则符号执行树中的执行路径的数量是有限的。考虑周期中的记忆单元，出现在同一个数据约束中。设k是存储单元之间的传递关系中的最长路径的长度。通过遍历每个周期k次，我们可以生成表示 数据流的最后k个元素，其中k是有界整数。对于每个数据流，进入/退出每个端口，k可以是不同的，并且取决于数量 在电路中的元件。这也显示了输出是否依赖于输入。如果我们不能在Names中找到某些节点之间的预期关系，这表明可能存在错误，即，规格之间的不匹配和我们的选举事务处的线路在我们的技术中，而不是建立符号执行树，我们生成CA的正则表达式，假设其初始状态为自动机的最终状态。执行路径是正则表达式的衍生物。我们展开数据约束，并显示数据流中的数据元素之间的关系。这个关系上的传递闭包给出了符号输入之间的关系146B. Pourvatan等人/理论计算机科学电子笔记255（2009）137和输出值。传统的符号执行技术从构建符号执行树开始。为了使我们的技术更容易理解并展示直观性，在下文中，我们首先展示如何形成Reo电路的符号执行树。但是，这里我们已经有了约束自动机，而不是程序代码。因此，在显示执行树之后，我们使用CA的正则表达式来解释我们的技术，用于构建所需的执行路径并导出输入和输出值之间的关系。3.2Reo电路通过遍历Reo电路的约束自动机，形成了Reo电路的符号执行树。我们从CA中的初始状态开始，在CA中遍历所有可能的路径当穿越一个变迁qN，g p时，CA，我们将其名称集N和其保护g存储在其各自的transitio−n→中，遍历树当我们构建树时，每次我们看到一个名称（Reo中的端口），这意味着在通过该端口的数据流中观察到新的数据元素。通过端口A的数据流表示为：a=（a0，a1，a2，a3，...， a last-2，a last-1，a last）在遍历树中为每个状态编写数据约束时，我们使用这些数据流的最后一个元素：...，最后-2，最后-1，每个端口的最后：展开数据流，同时保持符号表示和数据元素之间的关系。图3显示了FIFO 2通道的执行树。图中显示了数据元素之间的关系中的所有执行路径返回到初始状态的初始状态。 每片叶子上的字符串树显示了在其相应路径中触发的端口的名称。一对方括号包含了一组同步触发的端口名称（参见第3.3节中的步骤1）。 连接到树的每个节点的框显示触发以到达该节点（CA状态）以及所有保持的数据约束在那一点上（直到那一点上都是满足的），以及它们之间的传递关系。我们认为数据约束（数据值的布尔表达式）的集合作为通过节点的数据元素和存储在存储单元（其中我们有FIFO通道）中的数据元素的关系。我们只考虑原始的Reo通道，它只产生数据约束中的相等。因此，对应于通过节点的数据的关系是对称的。必须正确解决存储单元和数据元素之间的关系。这个关系的传递闭包给出了输入和输出值（端口）之间的所有符号关系。图3中的符号执行树是通过只遍历CA中的每个循环一次而生成的。 在这个例子中，这足以产生一般表达式输入值和输出值之间的关系。通过多次遍历循环不会生成新的关系。 在某些情况下，我们可能只感兴趣在查找通过某个输出节点的数据与B. Pourvatan等人/理论计算机科学电子笔记255（2009）137147图三. FIFO 2的符号执行树：每个节点表示一个状态，边表示转换在CA中（每个叶子上的字符串：在相应路径中触发的端口的名称;一对方括号：包含一组同步触发的端口名称输入数据。在本例中，我们只关注包含该特定输出节点名称的路径。符号执行已经被用于程序的验证，并且技术自然地基于构建符号执行树。但在我们的例子中，我们领先一步，拥有约束自动机而不是程序的源代码。因此，我们使用CA的正则表达式来获得我们感兴趣的导数集，而不是构建符号执行树。这里提出的符号执行树的目的是显示我们的技术与传统的符号执行方法的相似之处。3.3Reo电路我们分三步计算Reo电路的符号输出值• (1)获取约束自动机的正则表达式。在这里，我们使用Brzozowski我们认为初始状态是CA的最终状态。• (2)构造正则表达式的导数（单词），替换为148B. Pourvatan等人/理论计算机科学电子笔记255（2009）137∗关于我们具有k或零重复的Kleene闭包JJ，其中k是循环中的存储器单元之间的传递关系中的最长路径。这些导数表示约束自动机中所有执行路径的集合（符号执行树中的叶子），如果我们经历CA的每个循环k次（用k替换JJ），或者在可能的情况下绕过循环（用零替换JJ• (3)通过形成每个流中的数据元素之间的关系的传递闭包，基于每个导数的数据的符号输入流来在这一步中，我们从右到左遍历每个导数，并在数据约束公式中替换数据流的数据元素（为每个元素添加适当的索引）。然后，我们计算输入和输出数据流中的数据元素在下文中，我们将解释每个步骤，并使用图2（b）中所示的FIFO 2通道作为运行示例。第一步：生成正则表达式。 我们使用Brzozowski代数方法[9]和Arden我们创建了一个正则表达式系统，其中一个正则表达式作为约束自动机中每个状态的未知数，然后我们求解该系统其中R1是与初始状态q1相关联的正则表达式。出于我们的目的，我们将约束自动机的初始状态视为最终状态，因为当我们回到这些状态时，我们就回到了Reo电路的初始配置中，我们可以假设这是在Reo电路中完成了一次运行。我们还考虑了约束自动机的每个转换的数据约束。 我们将数据约束和转换标签（名称）保持成对。 注意，在应用Brzozowski代数方法时，我们保留每个转换的名称和数据约束对，并在求解系统时携带它们在约束自动机中，我们可能在转换上有多个名称，这意味着与这些名称对应的所有Reo端口都同步触发在这个过渡。我们将这些名称放在方括号[]中，以显示它们的同步/原子发射。例如，[ABC]意味着A、B和C在一次跃迁中以任何顺序（甚至同时在一起）原子地燃烧。相反，（ABC）意味着A、B和C在连续的转换中一个接一个地触发。[001 pdf1st-31files] 这是一个明显不同的概念，而这两个概念又是不同的。 所以，阿尔法-我们的语言是由复合字母组成的。 字母的第一部分可以是CA的名称集中的名称，也可以是包含（非空）一组名字。第二个组件是相应转换的数据约束。图2（a）中FIFO 1通道的正则表达式为：R1=（AB），用数据约束扩充它，我们得到R1=（A tx=dA B dB=sx）。 对于我们的运行示例，图2（b）的FIFO 2，我们有R1=（（A）（B [AC]+BAC）BC）并且包括数据约束的完整表达式为：B. Pourvatan等人/理论计算机科学电子笔记255（2009）137149∗--∗R1=（（A{tx=dA}）（B{dB=sx，ty=dB}[AC]{tx=dA，dC=sy}+B{dB=sx，ty=dB}A{tx=dA}C{dC=sy}）B{dB=sx，ty=dB}C{dC=sy}）对于LossySync，我们添加数据约束 d A=d A在过渡时期， 名称A表示数据丢失步骤2：通过将每个j j替换为零或k个重复来生成正则表达式的所有导数。在这个步骤中，我们通过将表达式中的重复视为零或k（其中k是循环中存储单元之间的传递关系中的最长路径的长度）来生成正则表达式的所有可能的导数。这意味着在CA中的循环的情况下，我们只遍历循环k次。下面，我们通过替换每个JJ来显示正则表达式的导数对于FIFO 2示例，具有零或k=• 将外部jJ替换为零重复：R11=空• 将内部jJ替换为零重复，将外部JJ替换为一：R12=（A{tx=dA}B{dB=sx，ty=dB}C{dC=sy}）• 用一次重复替换内部JJ，用一次重复替换外部JJR13=（（A{tx=dA}）（B{dB=sx，ty=dB}[AC]{tx=dA，dC=sy} +B{dB=sx，ty=dB}A{tx=dA}C{dC=sy}）B{dB=sx，ty=dB}C{dC=sy}）第三步：根据以下内容构建每个输出节点的符号数据流：每个导数的符号输入数据流。 在这一步中，我们遍历每个正则表达式，通过其元素显示数据流（索引数据流的元素）。然后，获得流的这些元素之间的所有传递关系（传递闭包），给出输出值和输入值之间的关系。在这一步中，我们首先为正则表达式中显示的数据约束中的每个数据元素指定索引。为此，我们从右向左遍历正则表达式。然后，我们得到传递闭包。步骤3.1：索引。直观地说，索引的目的是显示沿着正则表达式的遍历所看到的节点的顺序。 例如，如果我们观察在正则表达式中，我们第一次用索引名称a替换它的数据dA。如果我们看到另一个A，我们把新的A记为last，把前一个A记为last-1，把前一个记为last-2，以此类推。对于FIFO 2的例子，我们得到下面的二阶导数方程在步骤2中：R12=（A{tx=alast}B{blast=sx，ty=blast}C{clast=sy}）注意，在从右到左索引数据元素时，J+J的所有子表达式的起始索引是相同的最后一个正则表达式的等式150B. Pourvatan等人/理论计算机科学电子笔记255（2009）137步骤2是：R13= （ （ A{tx=alast−1} ） （ B{blast−1=sx ， ty=blast−1}[AC]{tx=alast ，clast−1=sy}+B{blast−1=sx，ty=blast−1}A{tx=alast}C{clast−1=sy}）B{blast=sx，ty=blast}C{clast=sy}）双索引。当我们遍历一个带括号的表达式进行索引时，我们可能会得到一个Reo节点名的两个不同的索引版本。如果表达式包含至少一个J+J运算符，则可能发生这种情况在本例中，我们继续为每个版本建立索引，然后使用逻辑RISK操作符组合数据元素名称的两个索引版本。例如，在R =（A {t x= d A}（AB{d B= d A} + B {d B= s x}））中，我们计算A（和B）的索引如下：R =（A {tx= a lastlast−1}（AB {b last= a last}+ B {b last= s x}））。步骤3.2：传递闭包。在正确地索引了数据元素之后，我们得到了它们之间的所有传递关系对于我们的FIFO 2示例，我们有R12=（A{tx=alast}B{blast=sx，ty=blast}C{clast=sy}）由于我们知道每个tx和sx之间的关系，我们可以写：R12=（AB{tx=alast，blast=sx，ty=blast，alast=blast，ty=alast}C{clast=sy}）然后：R12=（ABC{tx=alast，blast=sx，ty=blast，alast=blast，ty=alast，clast=sy，clast=alast}）现在，只关注输出节点C和输入节点A之间的关系（这是我们感兴趣的关系），我们有：R12=（ABC{clast=alast}）现在我们可以得出结论，ci的数据和ai的数据是一样的。 上述方程中的模式ABC表明，ci的数据正好是ai的数据，可能存在延迟。如果模式是[ABC]，情况就会不同，因为这意味着点火是原子的。我们继续R13：R13= （ （ A{tx=alast−1} ） （ B{blast−1=sx ， ty=blast−1}[AC]{tx=alast ，clast−1=sy}+B{blast−1=sx，ty=blast−1}A{tx=alast}C{clast−1=sy}）B{blast=sx，ty=blast}C{clast=sy}）则：R13=（A（B[AC]+BAC）BC{alast−1=clast−1，clast=alast}）这就给出了关系式：clast=alast，clast−1=alast−1，这意味着在Reo回路的一次运行中，我们有两个a输出节点中的c的每个元素与Reo电路的输入节点中的a的元素相同。B. Pourvatan等人/理论计算机科学电子笔记255（2009）137151见图4。 电路（a）替代者和（b）非确定性选择及其约束自动机最后，如果我们可以通过一组输入数据流S来描述输出Reo节点上的数据流，比如Z，那么我们就实现了我们的目标。否则，Reo节点Z无法从集合S中的Reo节点到达，并且如果S是所有输入值的集合，则我们发现了死锁或活锁陷阱。4案例研究在本节中，我们将介绍几个示例。示例1：交流发电机电路。交流发电机电路如图4（a）所示。 生成该电路的正则表达式、生成其导数、索引以及导出其输入和输出值之间的关系的步骤包括在附录中。最终结果是：zlast−1=blast，zlast=alast这表明：（1）来自端口Z的输出数据是通过在来自端口A和B的输入数据之间交替而形成的，以及（2）来自A的数据是在Z上同步产生的，而来自B的数据是在Z上以一个周期延迟产生的。示例2：非确定性选择。 图4（b）显示了一个Reo电路，其输入端口之间具有非确定性选择。生成电路的正则表达式，生成其导数，索引以及导出其输入和输出值之间的关系的步骤包括在附录中。最终结果是：zlast−1=blast，zlast=alastzlast=blastzlast=alast这表明输入值和输出值之间的所有三种关系都是可能的。由于合并，我们这里有一个不确定的行为，152B. Pourvatan等人/理论计算机科学电子笔记255（2009）137图五. Fibonacci Reo回路及其约束自动机。导出表示该电路的输入值例子3：斐波那契数列。 斐波那契数列的Reo回路[7]有从其输出到其输入的反馈，以生成该递归公式的值。图5显示了一个Fibonacci Reo回路及其约束自动机。在该电路中，FIFO 1的初始值为1，FIFO 2的初始值为0。 在这里，我们感兴趣的是作为输入反馈的输出与同样的电路。 当在正则表达式中，在循环数据约束中将同一节点视为源和目标。为了提取循环关系，我们需要遍历每个循环有限次。 在此示例中，x是FIFO 1的存储单元，y和z是存储单元对于FIFO 2，m和n是加法器组件的存储单元。加法器组件只是一个简单的组件，它获取两个输入值，将它们相加，并将它们放在输出端口上。 生成正则表达式的步骤电路，产生其衍生物，索引，并推导出之间的关系其输入和输出值包含在附录中。 在这个例子中，因为我们感兴趣的是推导出序列之间的关系，Reo电路的节点E上的数据与其自身。因此，我们重复循环和索引，直到我们有一个封闭的数据值表达式，即，我们有关于E本身的数据（这里它是总数的三倍 的缓冲器）。最后的结果给出了斐波那契回路的以下符号输出：elast=elast−1+elast−2示例4：关键部分。在[19]中，CPU的行为通过定义一组用于算术，逻辑和比较操作的基本组件来建模，Reo电路用于分支，移动和基本I/O指令。结果表明B. Pourvatan等人/理论计算机科学电子笔记255（2009）137153如何使用Reo来构造这些基本操作。该方法可用于分析多线程系统、数据库应用和资源共享系统。我们选择[19]的案例研究作为控制主导系统的一个例子。它是一个由两个并发过程组成的系统，其中一个关键部分使用Reo和CA建模。在该系统的模型中，CA中有84个状态、284个转换和127个名称。对于每个过程，在其通过临界区之后生成输出。我们在符号执行结果中检查是否生成了该输出。我们在这个系统中发现了一个执行路径，其中没有生成这个输出。 这说明，已经出现了僵局。 因此，在本发明中，我们可以在不生成整个状态空间的情况下检测系统中的死锁，因此这比传统的模型检测更便宜5相关工作符号执行是验证中的一种既定技术，特别是在硬件验证社区中。符号执行起源于七十年代[12]，迅速发展成为硬件设计的主要验证技术之一，并有许多成功的应用，例如[16]。 随着Seger和Bryant在90年代[8]发明了符号轨迹评估，这种方法现在已经成为大多数工业硬件验证系统的一个组成部分（例如Intel的FORTE [22]）。由于Reo以前曾用于硬件系统建模[20，21]，因此本文中的方法可以与之前关于硬件系统符号执行的论文进行比较，因为我们也能够符号化硬件设计中输入和输出值之间的关系。虽然不像硬件那样流行，但符号执行也被用作软件系统的验证技术。非确定性的程度和决定软件系统结果的大量不同因素通常阻止符号执行在实践中被用作唯一的验证技术，而没有任何其他伴随技术。示例包括[14]它将并发Ada程序转换为一种类型的Petri网，然后使用符号执行来查找程序的输入和输出值之间的关系。这项工作与我们的工作有相似之处，因为它试图象征性地分析用于表示并发行为的模型符号执行在软