语法驱动的ESTEREL程序模型检验与可达状态空间划分

理论计算机科学电子笔记153（2006）19-35www.elsevier.com/locate/entcs语法驱动的行为划分模型检验E星程序EricVecc c hi'eand RobertdeSimone1INRIA，Sophia Antipolis，法国摘要我们考虑的问题，利用的结构形式，ESTEREL程序来划分算法RSS（可达状态空间）定点构造用于模型检查技术。基本思想听起来非常简单，就像顺序合成的情况一样：在P;Q中，首先完全计算P中到达的状态，然后只进行Q，每次只使用相关的转移关系部分。在这里，如果P具有不同长度的不同行为，那么蛮力符号广度优先搜索将混合P和Q的探索，这将导致临时状态空间的不规则BBD表示，这是符号模型检查复杂性的主要原因。在我们的分解方法中，当调度存在并行性和局部信号交换的不同过渡部分时，出现了困难。 由于动态行为，并行放置的程序块（或“宏状态”）可以以各种方式同步，并且考虑所有可能性可能导致过度的划分复杂性。我们的目标是在组合方法和全局方法之间具体地说，我们使用的一些功能，TI GE RBDD库和内部信号之间的启发式排序，以使过渡关系通过程序行为进行，以获得与全局RSS计算相同的效果我们提供了具体的基准，显示该方法的实用性。关键词：Esterel，模型检测，BDD，可达性，划分，程序块，边界，高级，语法，余因子分解1引言在过去的十年中，基于BDD的隐式状态空间表示[5]的出现但是不能仅仅依靠BDD来处理可达状态空间构造的所有复杂性。具体而言，虽然1 Eric. sophia.inria.fr，simone@sophia.inria.fr1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.02.02320E. 韦奇埃河de Simone/Electronic Notes in Theoretical Computer Science 153（2006）19最终可达状态空间的BDD编码通常可能非常紧凑，下一状态计算的过渡关系和中间步骤已经提出了几种用于划分过渡函数应用程序的巧妙技术，这些技术部分地解决了问题[1，2，10]。背景下E星[3]建议使用应用转换关系分段地，仅当它可以提供进一步的状态时。直观地说，在顺序组合P;Q中，人们显然希望首先计算P中的所有可达状态，然后继续计算Q中的状态。 虽然这看起来可能是一个微不足道的想法（毕竟，可达状态空间构造可以被视为所有行为的详尽符号模拟），但必须小心，特别是在存在并行组件和内部信号通信的情况下，以便该方法保留了符号方法的一些优点，即，不枚举（或甚至不几乎枚举）所有个体行为。这是一个典型的时间/空间交易。尽管如此，使用ESTEREL程序的算法结构来指导（符号，穷举，广度优先搜索）状态空间构造是一个清晰，简单的想法，据我们所知，以前从未尝试过。其他有类似关注的作品通常试图在符号广度优先搜索之前，进行部分显式深度优先搜索模拟，以识别潜在行为中“前方”的新初始配置出于暂时的原因，我们将在当前的文章中关注该语言的一个微小的内核版本，仍然足以展示我们的技术（可以处理完整的语言）。特别是，我们将只考虑由一般的并行“网络”组成的规范尽管如此，组件可以交换信号来启动，冻结或中止彼此，并改变宏观状态配置。从本质上讲，我们的改进算法如下进行：最初应用非常受限的转换关系，许多位置（内部或外部）信号接收“阻塞”。然后，这些信号接收事件以渐进的顺序方式逐渐“重新允许”，使得过渡关系总是增长。但是由于新的扩展总是应用于通过T i G e R BDD的一些简化属性得到包[7]，它它们所适用的国家的域这种操作大大简化用于对“接收容限”进行排序的启发式方法本文的组织如下：首先，我们非正式地激励我们的框架上一个简单的例子。然后，我们给出一个简短的总结（一个限制性的E. 韦奇埃河de Simone/Electronic Notes in Theoretical Computer Science 153（2006）1921微子集）ESTEREL，以及符号模型检查的技术元素 我们关注的是T I G E RBDD包[6]如何执行转换划分和“转换余因子分解”，以减少数据的大小结构（并优化变量支持）。这些技术在以后理解我们的技术时会很方便然后，我们提供了我们的方法的抽象描述，首先是顺序组件，然后是具有本地信号交换的并行系统，然后是实际算法及其BDD实现，依赖于已经提到的TI GE R的特点。我们证明了我们的分区的正确性，构建完整的RSS。最后，我们来描述一下我们的原型--类型实现和性能基准测试，然后是进一步改进循环构造处理的建议。一个例子：老式的数字手表。如图1所示的设计包括几个模块，以及4个输入按钮和一个输出LCD屏幕的接口（也有音频嗡嗡声）：报警（计数器）模块通过将输入的石英滴答声相加来计算时间和日期;当发生变化时（增量），它将信息发送到显示器时间设置模块允许使用适当的输入按钮来改变和更新时间和日期值;报警设置模块允许设置报警时间，并切换开/关报警模式;秒表模块允许设置/重置或停止计时器;如果需要，即使没有显示，它也应该继续运行;显示模块根据当前设置的模式，在手表液晶显示屏上显示适当的信息或音频蜂鸣按钮解码器模块应该根据当前模式将实际的手表按钮链接到进入子模块的适当信号。 特别是右上角按钮的作用“ 到 替代 活性 模式的一个LARM设置和S TOPWATCH模式。时间已定，报警/报警按钮解码器时间设置Fig. 1. 手表的设计。为了空间起见，这里不能包括组件的反应行为但读者可以很容易地说服他/她自己，是模式选择报警设置模式显示模式报警设置按钮ALM双 TMR晶体管时间设定方秒表模式秒表显示22E. 韦奇埃河de Simone/Electronic Notes in Theoretical Computer Science 153（2006）19子模块之间时间已定，一套闹钟，表必须放在但在对大多数问题的按钮事件（实际上，只有当前选择的模式响应这些脉冲，对于切换模式的按钮是安全的）。这种程序的基本广度优先搜索分析没有利用子模块是互斥的这一事实，并计算整个程序的可达状态空间。该程序的分析可以分为三个部分：第一部分在时间集模式下计算可达状态，然后在ALARM集模式下计算可达状态，最后在STOPWATCH模式下计算可达状态。因此，每个模式的状态搜索可以在很大程度上独立于其他两个模式来完成这种方法在空间上的增益是明显的，因为对原始程序的分析可以被同化为对三个程序的分析，这三个程序都小于原始程序，因为局部转换被用来代替全局转换。2μ-ESTERELESTEREL是一种命令式同步反应语言。我们在这里只考虑一个简单的版本，其中数据变量和数据处理被丢弃，就像在模型检查中经常发生的那样我们只会用一种信号（identi），fier）类型。一个完整的程序由一个头（定义了输入和输出信号的接口）和一个主体组成程序语句的语法由以下简单语法提供：P：：=暂停| P CUP| present S then P else P end| P; P| 发射S| 当S时中止P| 环P端| 信号S在P端其中S在信号范围内变化。的朴素语义E星程序的行为如下：在瞬间之间离散地划分控制线程被执行，直到达到-执行一个语句，这是一个主语句，它将行为切割成原子实例。我们称之为在一个反应周期中，输入信号被读取/采样，内部计算发生，直到输出信号被发射的答案，并pro-gram状态进行。instant基于一个公共的逻辑时钟，它对所有并行线程进行同步。这（所有组件都以相同的原子步骤进行的事实）就是为什么我们称该模型为当然，在一个反应中，各种并行线程并不是独立运行的，因为它们可能会同步，并相互影响（硬件人员会说“组合地”）。当控制到达S测试语句时，它可能不得不推迟执行，直到为当前反应中的信号获得一致的定义值（存在或不存在）（因为它是在某个地方并行发出的，或者因为其他执行线程可证明地进展到可证明所有潜在发射都被丢弃的点建设性因果关系的主题（用于确定信号的存在价值观）是一个庞大的身体ESTEREL语义理论，但我们不会广告-这里我们将它打扮一下;相反，我们将假设没有循环组合信号之间的依赖关系E. 韦奇埃河de Simone/Electronic Notes in Theoretical Computer Science 153（2006）1923虽然是高级命令式语言，E星享受着一种语义上的-保留到硬件RTL级（网表）的转换，其中因果关系问题可以更容易地处理，并解释成Mealy FSM的第二个层次（再次语义上的声音）。第二个层次实际上丢失了关于精细因果关系问题的信息，但明确了实际可达的状态空间，因此可以作为模型检查分析技术的定义背景当然，隐式（或符号）基于BDD的模型检查的目的是在电路级应用这些分析在我们的例子中，我们试图通过利用源语法中的高级结构信息来提升它们。我们将坚持从ESTEREL到[4]中描述的电路的经典翻译，它为每个语句生成一个布尔寄存器。在接下来的文章中，我们将考虑一个抽象的语法树，锡恩福E星其中构造被显式标记的程序通过相应的寄存器名称，提供必要的关联。事实上，我们希望识别每个指令实例，我们在这里用一个称为指数的唯一标签来识别。 树中的每个节点都是根据它所代表的指令来确定类型的。因此 ， 由 L 标 记 的 指 令 类 型 的 指 令 的 树 节 点 被 写 入 ：（instructionLsubtrere111. . sub trenln）。3符号下一状态操作和优化3.1符号状态空间计算基本的广度优先搜索可达状态空间算法可以写成：1reachable←初始化2new ←初始化3while（new/=new）do4new←ImageΔ（new，INPUTS）\reachable5reachable←reachable新的6end while在第n次迭代中达到的状态集是由在第（n-1）次迭代中达到的状态集和程序的有效输入集通过在转移关系Δ下计算图像而构建的。算法停止程序的每个状态是电路的布尔寄存器的集合R的赋值，并且程序的每个输入是输入信号的集合I的赋值唯一的全局转移关系Δ让我们计算程序关于R和I的值的新状态：Δ：Bm×Bn→Bm（R，I）→RJ= Δ（R，I）当B={0，1}时，m为寄存器的数量，n为电路的输入事实上，Δ可以被24E. 韦奇埃河de Simone/Electronic Notes in Theoretical Computer Science 153（2006）19我δi： Bmi×Bni→B（Ri，Ii）→rJ=δi（Ri，Ii）向量Ri和Ii称为这些转移函数的支集。mi和ni分别是寄存器的数量和该支持的输入信号的数量这种划分方案用于加速表示各个δi的BDD的应用。3.2集编码给定一组BDD变量R={r1，. rn}，我们引入算子[R ∞=λX→ <$r1<$. ∧ ¬rn.如果r1，. rn是表示布尔寄存器R1，. Rn则表示所有寄存器Ri对于所有i∈ [1.n]。我们注意到[R <$= λX → r1<$. 表示状态的集合，其中至少一个寄存器Ri对于i ∈ [1.. n]。对于所有集合S，我们有S<$[R <$=S\[R <$]。3.3扩展的余因子分解方法我们将广泛使用一些著名的BDD变换，通常称为扩展的余因子分解技术[8]。从本质上讲，这个原则是，如果BDD的值只与其变量的可能赋值的子集相关，那么这个有限的定义域可以用来简化BDD的表达式（可能在它之外改变它的值）。通常，域本身作为BDD提供。我们记f↑S为f的余因子分解，集合S：f↑S（X）=λX→.f（X）如果X∈S？如果X/∈SS中的f↑S的值不被使用，可以是任何值。它的背景是为了最小化表示f↑S的BDD的大小。在我们的算法中，此运算符用于Image函数中。它让我们在图像计算过程中处理更小的BDD，因为转换关系相对于它所应用的域更精确地说，给定一个寄存器r，如果r的激活条件（r= 1的状态集）和转移关系的域不相交，那么r的转移函数可以简化为一个非常简单的表达式λX→<$r。换句话说，对下一瞬间不会被激活的寄存器的转换函数进行编码的BDD非常小。4方法概述该方法的核心是将程序体划分为适当粒度的块（或宏状态）。在顺序子组件中，宏状态将按顺序组合或作为替代选择if-then-else。在移动之前，将在每个块内执行状态搜索，直到稳定E. 韦奇埃河de Simone/Electronic Notes in Theoretical Computer Science 153（2006）1925到下一个下一个迭代步骤将采取新的初始状态那些为了禁止在给定的块中进行搜索，只需要移除其中这些块的所有寄存器都不活动的转换关系的部分。图二.程序的四块划分方法。 块之间的边界（以虚线绘制）逐个打开该方案提出了一个并行性问题，以及在并行组件中可以同时遍历两个局部边界的情况。考虑所有可能的区块组合将导致案例的笛卡尔积爆炸。因此，我们选择遵循以下策略：首先，找到一个然后，我们从最小数量的活动块开始，并且我们只在通过边界时添加新块，而不关闭任何回。因此，过渡关系将从初始过渡关系发展到全局完全过渡关系。但是，与此同时，我们只将增长的转换关系应用于可以证明在前一个范围之外创建新的状态的状态，因此仅使用受限版本安全地计算仅在前一个步骤到达和贡献的状态因此，我们的新的状态集（在其上应用了转换关系）将始终位于先前的块组合之外，并且余因子分解的各种操作将（希望）省略大部分转换关系描述。图2显示了PQ图三.我们在两个块P和Q之间的边界上的划分方法的细节。在前三个步骤中，执行P的饱和。在图像计算中不使用在P区域之外的超低频的状态。在最后两个步骤中，P和Q的饱和从先前的未决状态开始执行。由于已分析了整个P，因此可达状态的探索仅涉及Q。块之间的划分和相关边界的定义当然在很大程度上依赖于结构句法，主要依赖于信号接收（如在PS中），在较小程度上依赖于信号发射。我们使用26E. 韦奇埃河de Simone/Electronic Notes in Theoretical Computer Science 153（2006）19一个控制流程图数据结构来帮助我们完成这项任务。该图是建立在我们的语法树之上，使用相同的节点。它描述了所有可能的路径遵循的控制之间的每个指令的ESTEREL程序，克，特别是寄存器之间。然后，将通过选择边缘的专用子集来描述块之间的边界随着保留的边界边缘越来越少，选择会动态变化，从而导致之前描述的过渡关系然后，从包含锁定和解锁边缘的当前图，算法的每个迭代宏步骤包括计算非活动寄存器的集合，构建所考虑区域的适当BDD描述，从未决状态中选择适当的下一步初始配置集合。 在下一节中，我们将描述我们从结构语法中选择的边界，以及控制流程图的创建。5根据语法划分为这里将考虑两个方面。第一个明显的问题是如何根据语法划分转换关系应用程序第二个问题是如何计算分解何时确实是有益的（因为实际上没有一个子部分会退化到孤立地考虑它是浪费精力的地步）;我们暂时还不清楚第二个方面。序列语句。考虑一个由两个按顺序排列的组件组成的程序：P;Q。如果在全局转移关系上以广度优先搜索方式计算可达状态空间，则将考虑Q中的状态，而可能P中的其他状态仍未到达，在这种情况下，如果我们承认部分可达状态空间的中间形式比最终形式更不规则，那么中间符号描述可能比最终符号描述更大。此外，这里的顺序划分的状态空间搜索允许在处理每个分量（P，然后Q）时仅使用转移关系的相关部分在两种情况下，分区是一种能量浪费。第一个是P或Q不包含暂停语句的明显情况。第二种情况发生在P是定长规划时。例如，如果P的形式为P的每一次执行都分布在两个瞬间。换句话说，P;Q的划分自然由广度优先搜索算法执行。选择运算符。如果我们现在考虑SP Q替代选择，情况非常相似。P和Q中的可达状态空间可以独立构建，如果假设两个分支都不会立即终止，因此包含暂停语句。E. 韦奇埃河de Simone/Electronic Notes in Theoretical Computer Science 153（2006）1927S1S2S1S2S1S2先占权PS语句允许在P的自然终止上添加失败的转换。我们的划分技术的目标是在探索由P的终止所激活的下一个程序块之前完全探索P(of当然，这也将具有阻止导致中止的潜在排放的效果，这将在相同的全局转变中出现因此，我们想把从P出发的每个跃迁都看作是前沿。循环。在顺序（“无并行”）的上下文中，对P程序的探索分解为对P的探索，因为循环只会回到P的初始配置，已经达到了。然而，在（更常见的）并行设置中，问题来自于这样一个事实，即哪些块可以并行活动，通常是通过连续的同步动态获得的（这在很大程度上是为什么RSS构建如此困难的原因）。我们目前的解决方案是只增加对连续定点中使用的转换关系的寄存器支持，并希望依赖于这样一个事实，即实际的同步只允许创建这样一种形状的状态，即TI GE R的正则余因子分解将清除多余的转换关系(when配置是一致无效的，导致假值寄存器，丢弃相应的过渡部分在未来，对控制流图结构的进一步研究应该有助于我们确定哪些边界可以被视为全局同步整个系统的循环模式，以便每次循环“展开”时，并行网络和信号同步。如前所述，这里的问题是确定哪些并行放置的块可以并行激活，以便全局搜索可以用匹配的级数来划分。如图4所示。唯一的语法见图4。一种并行组件的划分方法。有两个信号同步三个并行组件。我们的技术旨在根据黑色块进行分区。影线框应该通过余因子分解方法移除。在这里，我们可以用来指示同步的元素当然是信号接收。当信号是本地信号时，这些接收必须与相应的发射相匹配（否则输入信号的接收可以随时发生，但每个并行组件必须一致地感知它）。然而，应该注意的是，在同步反应框架中如果没有人在当时“积极观看”，则本地信号发射可能不会导致接收。因此，虽然我们将使用信号接收来生成边界转换，但这些将在发射时自动生成同步边界。28E. 韦奇埃河de Simone/Electronic Notes in Theoretical Computer Science 153（2006）19中止循环暂停结束|| pause;pausewhen S;现在T然后暂停;[暂停||暂停]其他暂停;暂停结束;暂停F1F2.1？F2.2||F2.1||F2.2侧，否则发射可以通过并不同步。为了进一步说明，考虑下面的简单示例：P1;S;P2||Q1;S;Q2.如果这个程序的设计是这样的，S的任何发射都被await S语句接收，那么如果Q 2不活动，则P2不可能是活动的。因此，根据Q1和Q2进行划分将划分也是根据P1和P2的第一个分支如果S的一些发射没有被接收到，那么根据Q1和Q2的划分将在第一个分支上没有精确在所有情况下，这种划分方式都有真正的好处在最好的情况下，可达状态空间计算将首先涉及P1和Q1，然后是P2和Q2。在最坏的情况下，它将涉及P1，P2和Q1，然后是P2和Q2。边境命令目前，边界解锁的顺序是动态定义的，“在运行时”，在我们连续的定点迭代过程中，在不断增长的支持域中搜索新的我们每次都选择一个可能产生新状态的边界，而不是严格地在另一个边界之前。这在很大程度上依赖于一组未完全处理的未决状态的形状，并且可以生成超出当前边界的配置详情见第7.1节。在未来，我们打算研究这种选择（更静态的性质）的可能的改进，特别是寻找具有全局效应的边界，这些全局效应可以在循环中保留。6控制流程图我们的控制流程图是建立在ESTEREL程序。给定语法树T的控制流图定义如下：G（T）=（I，O，N，E，F），其中N是G的结点的集合。这些节点与语法树的节点相同I和O是N的子集，分别代表图的起始节点和最终我们的图的边（记为i→j）分为两类：E包含通过构造，集合E ∈F是空的。因此，对应于当前和中止语句的边在F中被解决。这样的边缘被称为“边界”边缘。其他边在E中解决。图五.一个带有控制图的ESTEREL程序的例子。虚线中的边界F1、F2.1和F2.2是由中止和本陈述产生的。我们在这里描述我们为每个ESTEREL构建控制流程图的方式E. 韦奇埃河de Simone/Electronic Notes in Theoretical Computer Science 153（2006）1929LL端）=（J指导。 该描述使用语法树的标签，这是识别节点的更轻松的方式。通常的运算符“×”允许我们连接集合I = { I 1，. Im}映射到集合J ={J1，. Jn}。原子指令生成包含单个节点且没有边的图：G（emitLs）=（{L}，{L}，{L}，n，n）G（暂停Lr）=（{L}，{L}，{L}，，）在下面的陈述中，我们假设指令I产生一个图G（I）=（I，O，N，E，F）。对于i∈[1，2]，有G（Ii）=（Ii，Oi，Ni，Ei，Fi）. 在我们看来，我们可以把范围的起点和终点分开因此，信号声明的图形与I的相同：G（信号LsIendLJ）=（I，O，N，E，F）在二进制序列中，第一个图的最后节点链接到第二个图的开始节点：G（序列LI IJend）=（I，O，N尼日利亚，EJ，FF）12 1 2 1 2 1 2EJ=E1<$E2<$（O1×I2）一个循环永远不会终止，因此它的最终节点集是空的。G（I）的最终节点与它的元素相连。G（loopLIendLJ）=（I，N，E<$EJ，F）EJ=O×I并行的两个分支在同一时刻启动。因此，并行的起始点是链接到其两个分支的条目的唯一节点G（标准LI1JI2end）=（{L}，O1臭氧2，N1N22）EJ=E1<$E2<$（{L}×（I1<$I2））在一个present语句中，我们要设置边界，以便探索I1，然后是I2，然后是程序中此语句之后执行的任何操作因此，边界被放置在“then”分支和“else”分支之前和之后。G（当前Ls I1I2结束L）=（{L}，{LJ}，N1<$N2<${L，LJ}，E1<$E2，FJ）FJ=F1<$F2<$（{L}×（I1<$I2））<$（（O1<$O2）×{LJ}）每一个暂停指令都可能导致包含它的中止指令的结束，这样的转换是边界，它将帮助我们分割RSS计算，因此被放在集合F中。G（abortLsILJI，{LJ}，N<${LJ}，E，F<$FJ）FJ=（O <${l/（pauselr）∈N}）×{LJ}7精确算法及其BDD实现我们都在努力实现我们的目标。Clos ure （N ，E）（I）表示从I通过E中的边可达的状态的集合.我们写<$（X）={j∈ N/ i ∈30E. 韦奇埃河de Simone/Electronic Notes in Theoretical Computer Science 153（2006）19X，<$i →j∈E}是E的边的目标节点的集合，其源属于× ×：Clos ure（N ，E）（I）=（μX. （X））下面的函数计算程序块的给定一组节点R N（对应于一组活动寄存器），表面是在R中的一个或多个寄存器激活后立即可以交叉的边的集合。如果R是类型为“pause”的节点的集合表面（N，E）（R）= Trans（μX . R（（X）\R））其中Trans（X）是E中源属于X的边的集合。 给定一个图的节点集合S，我 们 引 入 运 算 符 RegisterS ， 它 返 回 S 中 的 寄 存 器 BDD 变 量 集 合 ：RegisterS={ri/（pause ri）∈ S}。这个操作符将帮助我们在控制流图和基于符号BDD的 计算之间建立联系。7.1分块算法我们的分区算法是由控制流程图的边缘逐步解锁。BDDrestrictedArea表示位于边界内的所有状态（可达或不可达）在算法的每个步骤中，仅对位于restrictedArea（第7行）内的未决可达状态执行图像计算。根据当前域的余因子分解在图像计算中隐式地完成（第8行）。在每个步骤结束时，新发现的状态存储在挂起集合中（第9行）。只要在restrictedArea中找到新的状态，就不需要解锁（第4、5、6行）。第一个算法没有描述restrictedArea的初始化和放大方式（稍后将解释）。1reachable← INIT，pending← INIT2−−1。初始化由“restrictedArea”编码的集合3while（pending/=等待）4if（（pendingrestrictedArea）=0） then5--2。删除某些边缘并放大6end if7currentDomain←pending域名 restrictedArea8new←ImageΔ（currentDomain，INPUTS）\reachable9pending←（pending\ currentDomain）新的10reachable←reachable新的11end while控制流图和限制区域初始化（1）。我们假设所分析程序的语法树在T.初始化过程包括构建图以获得锁定边缘的初始集合，然后相对于这些初始条件构建集合restrictedAreaE. 韦奇埃河de Simone/Electronic Notes in Theoretical Computer Science 153（2006）19311.初始化由“restrictedArea”编码的集合1（I，O，N，E，F）← G（T）2allRegs←注册登录3reachableRegs←寄存器关闭（N，E）（I）关闭4restrictedArea←[所有Regs\reachableRegs]第一步是建立图表（第1行）。然后，我们需要知道允许激活的寄存器的reachableRegs集合（第3行）。最后，restrictedArea被定义为一组状态，除了reachableRegs中的寄存器之外，没有寄存器是活动的（第4行）。限制区域扩大（2）。当restrictedArea需要放大时，我们希望解锁“好”边。我们只想解锁允许我们在不断增长的restrictedArea集合中包含一些挂起状态的边这样的边只能在reachableRegs的曲面中找到。此外，可能需要解锁多于一个边缘这是两个并行分支等待相同信号的典型情况因此，当没有未决状态位于restrictedArea内时，分析新的边缘以便决定是否应该将其解锁。在事实上，当初始条件满足Closure（N ，E）（I）时，我们首先分析了在我们的算法中没有出现的d2. 隐藏一些边缘并放大1surface=F <$Surface（N，E <$F）（reachableRegs），i←12while（（pending_restrictedArea）= 0）3边界←曲面[i]，i←i+14-2.1 检查是否应打开“frontier”5if（unlock？）然后6-2.2 "边境"7end if8end while边缘交叉（2.1）。为了确定是否应该解锁边缘，必须关注未决集合中的新活动寄存器。2.1. 检查是否1newRegs←寄存器闭包（N，E）（I）闭包\reachableRegs2如果（newRegs=0），则3解锁？←真4else if（（pending\[newRegs]）5解锁？←真6其他7解锁？←错误8end if）然后首先，我们计算图中的节点集，如果边缘边界被解锁，则会到达该节点集。我们只需要知道新找到的寄存器，它们存储在第1行的newReg如果边界导致没有寄存器，则可以解锁，但这不会对设置的restrictedArea（第2行，第3行）产生影响。如果newRegs不是32E. 韦奇埃河de Simone/Electronic Notes in Theoretical Computer Science 153（2006）19空，我们检查是否有一些pending状态激活了newRegs中包含的一个或多个新寄存器（第4行，参见第3.2节）。在这种情况下，可以解锁边缘。解锁兼容边界（举个例子：R1、 R2和R3是由三个不同的边沿锁定的三个非活动寄存器。setpending包含两种状态：第一种状态只有R1和R3是活动的，第二种状态只有R2和R3是活动的。我们解锁第一个边缘，使我们能够激活寄存器R1。然后，在算法的这一点上，没有什么禁止我们在R3之前激活R2，而我们宁愿只激活R3。该解决方案包括制作一个副本的设置挂起所谓的挂起在开始解锁边缘之前。每次边缘被解锁时，我们减少设置的“挂起1pending二......3else if（（pending4pending5解锁？←真六......在我们前面的例子中，一旦R1被允许激活，R2就不能再在R3解锁边（2.2）。一旦决定解锁一条边，我们只需执行以下更新：首先，将解锁的边从F移动到E。然后，扩大所设置的restrictedArea。2.2. Unlock1E ← E {frontier}，F ← F\{frontier}2reachableRegs← reachableRegs创建新的Regs3restrictedArea← [allRegs\reachableRegs]7.2正确性参数（提示）我们将给出非正式的论证来证明我们的主张，即所有的状态都将被我们的分割技术所达到。最终，不断增长的过渡关系将达到经典单次迭代广度优先搜索中使用的全局关系的形式。但它只适用于新的初始状态的选择（那些从临时挂起的集合），因此将达到所有只能从那里到达的状态。但是，重要的是，在转换选择的给定阶段，在定点搜索中到达的新状态没有被放入未决集合中，这些新状态不能产生任何进一步的后继者（因为我们已经到达了E. 韦奇埃河de Simone/Electronic Notes in Theoretical Computer Science 153（2006）1933该限制关系转换的固定点）。因此，当边界解锁将打开一条通往它的路径时，最终将达到一个可达状态。8原型实施和基准我们实现了我们的方法的帮助下，TI GE RBDD包，我们测试了它的一些ESTEREL设计。这里所介绍的结果是通过在具有1GByte内存的Bi-PentiumIII-550 MHz上执行我们的程序并在Linux操作系统下运行而由于我们目前的原型模型检查器只能处理μ-ESTEREL约束语法（没有数据处理），我们还不能解析和分析大型程序，E星基准套件。结果在小型手写程序上仍然很有前途例如，在通过我们的语法标准的最大基准测试示例（名为sequencer在基准测试套件中），我们将由于BDD消耗而导致的峰值内存使用量降低了大约60%（17 MB对40 MB）。图6和图7显示了该示例中算法的演变在另一个大型设计（在基准测试套件中命名为cabin）中，使用全局转换关系的我们的方法能够产生135 441 875个状态（35小时40分钟后），成功实现123次迭代。虽然第1节中展示的腕表设计令人鼓舞，但它太小，无法呈现出显著的效果。200001800016000140001200010000800060000 20000400006000080000100000120000140000国数目1400001200001000008000060000400002000000 100 200 300 400 500 600时间（秒）见图6。在这两个图中，框表示默认算法。实线表示分区算法。第一个图显示了相对于找到的状态数使用的内存（分区更好）。第二个显示了相对于计算时间找到的状态数（默认方法更快，正如预期的那样）。9结论和今后的工作据我们所知，我们的方法是唯一的分区方法的基础上，从（同步）程序中提取的结构信息的syntactic{squential/alternative/parallel/synchronized}我们的方法倾向于模仿内存（Kb）国数目34E. 韦奇埃河de Simone/Electronic Notes in Theoretical Computer Science 153（2006）1918000 25000160001400020000120001000015000800060004000200010000500000 20000400006000080000100000120000 140000国数目00 20000400006000080000100000120000 140000国数目见图7。第一个图显示了BDD中编码新发现的状态的节点数与发现的状态数的关系;第二个图显示了BDD中编码可达状态的节点数与发现的状态数随着时间的推移，控制的行为进展，但在所有路径都必须遵循的情况下（穷举搜索，而不是单一路径模拟）。我们提出了一种解决方案，划分RSS计算，主要是根据信号接收，然后根据控制进度排序块的评估后一种信息是从控制流图中提取的，控制流图本身直接来自抽象语法树。该图还用于实际构建在任何给定的宏步骤中选择的精确的转移关系，通过包括在适当的边界中找到的寄存器的部分不断增加的方面的过渡允许避免潜在的爆破在各种情况下的配对块并行活动。但是，作为一个必然的结果，该方法在处理循环时仍然存在相对不科学的地方，这些循环实际上不能分为一系列步骤。我们打算在未来的研究是否更密切的检查的图形可以导致的情况下，一个前沿（说，信号接收）可以被视为具有全球同步功能，使一些循环组件放在并行不能进展各自的不规则的例如，在我们的草图手表示例中就是这种情况，其中按钮解码器主循环具有串行激活明显并行的时间集、ALARMSET和STOPWATCH模块的效果，而它们的大多数行为只能以循环方式执行，由按钮解码器主循环命令。引用[1] J. R. Burch，E. M. Clarke和D. E.久了基于分区转移关系的符号模型检验。以. Halaas和P.B.Denyer，editors，International Conference on Very Large Scale Integration，pages 49-58，Edinburgh，Scotland，1991. 北荷兰[2] J. R. Burch，E. M. Clarke，D. E.朗，K. L. MacMillan和D. L. 迪尔 时序电路验证的符号模型检验 。 IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems ， 13（4）：401[3] G'erard很好。我的天啊synchro nousprogramminglanguage：Design， 自我实现。Science of Computer Programming，19（2）：87可达集新集合E. 韦奇埃河de Simone/Electronic Notes in Theoretical Computer Science 153（2006）1935[4] G.贝瑞纯Esterel的构造性语义。草案第3版。http：//www-sop.inria.fr/meije/，1999年。[5] R. E.布莱恩特基于图的布尔函数操作算法。IEEE Transactions on Computers，C-35（8）：677[6] O.库德特角Berthet和J.C.妈妈 使用符号执行验证同步时序机。有限状态机自动验证方法研讨会，卷LNCS 407，1989年。[7] O. Coudert，J. C. Madre和H. Touati。Tiger 1.0版用户指南，1993年。数字巴黎研究实验室备忘录。[8] OlivevierCou d ert.S IAM ： Une Bo itea`utilsPorlaPeuveFormelledeSyst`em es S'equentiel s.PhDthe sis，EcoleNatio n a leS u peerieurd esTeleecommu nications，Octobre1991.[9] D.盖斯特和我啤酒转换关系自动排序的高效模型检验。在大卫湖Dill，编辑，Proceedings of thesixth In