分布式动态等价性检查

理论计算机科学电子笔记128（2005）47-62www.elsevier.com/locate/entcs分布式动态等价性检查Christophe Joubert和Radu Mateescu1INRIARhon ene-Alpes/VASY655，av.de摘要基于需求的等价性检查是通过以需求驱动的方式探索两个标注转换系统（LTSs）的等价关系来比较它们。由于它避免了LTSs的显式构造，因此该方法即使在太大而无法装入计算机内存的系统中也能够检测到错误。在本文中，我们的目标是进一步提高性能的在线等价性检查使用多台机器连接的网络。 我们提议奥尔夫警长， 提出了一种求解布尔方程组（BESs）的分布式在线求解的新算法，使等价性检查模的各种关系，其特征在于在BESs。DSOLVE作为分布式版本BIMSIMULATOR的验证引擎，B imsimulator是一个在CAD p验证工具箱中使用OpEN/Cimsimulator环境开发的在线我们的实验措施表明，准线性加速比和良好的可扩展性的分布式版本的BISIMULATORw.r.t.它的顺序版本。关键词：互模拟，布尔方程系统，标记转移系统，分布式等价性检查。1介绍等价性检查是一种验证技术，包括比较系统行为的描述（例如，协议）及其期望 行 为 的 描 述 （ 例 如 ， 服 务 ） 对 适 当 的 等 价 关 系 取 模 。[24][25 ][26][27][28]][29][29][29]][[11]、安全性[8]等） 被定义为标记转换系统（LTS），其是用于诸如进程代数的基于动作的描述语言的自然模型。基本上有两种方法来检查有限个LTSs的等价性：全局，这需要构造两个LTSs1{Christophe.Joubert，Radu.Mateescu}@ inrialpes.fr1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.10.01848C. 茹贝尔河Mateescu/Electronic Notes in Theoretical Computer Science 128（2005）47在验证之前和本地（或在验证过程中），这允许在验证期间增量地构建LTSs。该方法具有检测错误的能力，即使当LTSs太大而无法显式构造时，因此更适合于分析大型系统。在过去的二十年中，设计了许多用于全局等价性检查的顺序算法，并在验证工具中实现（调查见[10]）。这些算法中的大多数依赖于划分细化：从包含单个等价类的状态划分开始，它们迭代地细化它（通过分裂包含非等价状态的类），直到根据给定的等价关系不可能进一步区分类。最近，提出了分布式全局等价性检查算法[5，6]，在中型和大型LTS（数千万个状态和转换）上显示出有效的行为。然而，相对较少的研究文献致力于在的-的等价性检查算法。第一个提出的算法用于即时等价性检查[11]和前序检查[10]是基于以下原则：从两个L TS的初始状态开始，对它们进行向前的、同时的探索，直到遇到一些显示不等价的执行模式（反例），或者两个L TS已经被完全探索。另一种用于在线等价性检查的方法是基于布尔方程系统（BES）[9，3]中等价关系的特征化，其允许使用有效算法进行在线BES解析[20]。通过这种方式，等价关系的编码和BES解析算法被清楚地分离，允许它们被独立地实现和优化。我们遵循后一种方法开发了在线等价检查器B ISIMULATOR，它使用通用的CASSAR S OLVE[20] B ES解析库，使用Op EN/Cassar环境构建，用于C AD p verification toolbox [13]的在线L ts探索[ 12 ]。在本文中，我们提出了分布式版本的BISIMULATOR，这已获得通过设计DSOLVE，分布式上的非线性BES分辨率的算法。据我们所知，这是第一次尝试开发一个分布式的在线等价性检查器。DSOLVE在精神上与在[7]中提出的分布式模型检查算法（在游戏图的设置中）：它执行B的依赖图的分布式前向遍历，结合稳定变量的后向传播（即，其最终值已计算）。它被实现为运行在常用的松耦合架构，如工作站网络（NOWs）和PC集群。实验结果表明，DSOLVE具有准线性加速比和良好的可扩展性。问题的大小。DSOLVE已集成到通用的CENSISARSOLVE库中，因此允许C. 茹贝尔河Mateescu/Electronic Notes in Theoretical Computer Science 128（2005）4749一τ立即获得使用CENSORSARSOLVE构建的任何其他应用程序的分布式版本，例如无交替的μ-演算模型检查[20]和τ-一致性约简[23]。本文的其余部分组织如下。第2节回顾了BESs的定义和五种广泛使用的等价关系在BESs方面的编码。第3节详细介绍了DSOLVE算法和Section- tion4显示的实验数据比较的分布式和顺序版本的BIMSIMULATOR的性能。最后，第5节给出了一些结论和未来工作的方向2等价关系与布尔方程组一个LTS是一个四元组M=（Q，A，T，q0），其中：Q是状态集，A是作用集（Aτ=A<${τ}也包含不可见作用τ），T<$Q×Aτ×Q是转移关系，q0∈Q是初始状态。一个跃迁q1→q2∈T意味着系统可以从状态q1移动到状态q2通过执行一个cti o na. GivenallanguagelA，q1→lq2表示从q1到q2有一个转换序列，其级联动作形成a我的话其次，我们考虑两个LTsMi=（Qi，A，Ti，q0i），i∈{1，2}.ABES是一组方程B={Xi=Xi1opi···opiXiki}1≤i≤n，其中Xi是布尔变量，opi∈ {x，x}。 为了提高分辨率，我们考虑简单的BESs [4]，其方程的右侧是纯离散的。连接或合取公式（布尔常量F和T分别编码为空的析取和合取）。B es的语义 由 相 关 向 量 泛 函 Φ 的 最 大 不 动 点 给 出 ： n→n ， Φ （ b1 ， ... ， bn ） =（[Xi1opi···opiXiki]][b1/X1，.，bn/Xn]）1 ≤i≤n，其中[n]] δ是布尔公式n在上下文δ中的解释，将布尔值赋给变量。作为BESs基础的理论在[18]中得到了广泛的发展。LTSs之间的各种等价关系用BESs [9，3]刻画。下表显示了五个广泛使用的等价物的编码：强[24]，分支[25]，观察[22]，τ.a[11]和安全[8]。每个关系都表示为Bes，其变量Xp，q表示状态p∈Q1和q∈Q2是否等价（a∈A和b∈Aτ）. 为每个等价，相应的前序（灰色）通过删除第二个合取项（对于强、τα、安全性和分支），或者第三个和第四个合取项（对于观测）在方程的右侧。50C. 茹贝尔河Mateescu/Electronic Notes in Theoretical Computer Science 128（2005）47n上表中显示的所有BES都可以变得简单（价格通过引入额外的变量，使得方程的右手边变成析取的，或连续的，连接公式（例如，的BES对于强等价，{Xp，q=p→bpJYpJ，b，qq→bqJZp，b，qJ，YpJ，b，q=q→bqJXpJ，qJ，Zp，b，qJ=p→bpJXpJ，qJ}）。由此产生的BESs的非线性解决方案包括求解变量Xq01，q02（表示两个LTS的初始状态的等价性）通过递增地构造BES;这相当于对两个LTS的需求驱动的探索，因为方程右侧的公式是通过以向前的方式遍历LTS3分布式分辨算法分布式B ES解析采用的体系结构由索引i ∈ [1.. P]和一个索引为0的协调器节点，所有节点通过网络连接。除了分布式终止检测之外，（DTD）任务（见图2，第二节）3.3），协调员还负责其他活动，例如监控BES解决方案的进展，收集有关BES结构的统计数据，处理用户请求的提前终止或由远程硬件或软件故障引起的紧急终止。这些功能是通过适当的扩展DSOLVE（图中省略）实现的。①的人。DS OLVE 算法 是根 据布尔 图（ V ， E， L ）[2] 设计的，定义如下 ： V={X1，.，Xn}是顶点的集合（布尔变量），E={（Xi，Xj）|Xj∈{Xi1，.，xiki}}1≤i≤n是边s的第一个条件（布尔变量之间的依赖关系），L：V→ {x，y}，L（xi）=opi是顶点标记（方程右侧的布尔运算符DSOLVE的实例在每个工作者上运行（任务分区），数据（布尔变量）通过消息传递根据R编码强Xp，q8=“b'b'Xp'，q'p→p“b'b'Xp'，q'q→q p →p分支 P，则134：trm status：=TERM第135章：不一样136：endcase;137：如果trm status=DET ECT，则164：如果总消息=−（发送-接收）165：nnbidle=P，则166：trm status：=CONF;167：bcast节点：= 1;nb确认：= 0;168：stamp：=stamp+1第169章：不一样170：elsiftrm status=CONFthen一百三十八：RECEIVE（msg，sender）;171：nb ack：=nb ack+ 1;第139章：你 是谁？140： elsifIRECEIVE（msg，sender）then第141章：你 是谁？第142章：一夜情第143章：一夜情144：结束172：如果总消息=−（发送-接收）173：如果ack=P，则174：trm状态：=ST OP;175：bcast节点：= 1第176章：一夜情第177章：不一样第178章：不一样第179章：一夜情180：结束图二、终止检测算法（协调器节点）将相同的Ack（戳）消息返回给协调器（行106-110）。如果一个worker在接收到一个Ack（stamp）消息时是活动的，它会简单地忽略它。在这种情况下，来自该worker的Act消息最终必须到达协调器。最后，如果协调器接收到P Ack（戳）消息（即，nb ack=P，第162-178行）。然后它可以广播该终止检测（即，trm status=STOP）（第129-135行）。3.4正确性和复杂性我们的分布式BES分辨率算法是基于布尔图的理论，其基础是顺序算法[2，C. 茹贝尔河Mateescu/Electronic Notes in Theoretical Computer Science 128（2005）475726]。它由两个交织的图遍历（向前和向后）组成，其最坏情况时间58C. 茹贝尔河Mateescu/Electronic Notes in Theoretical Computer Science 128（2005）47复杂度为O（|V| + |E|）.同样的界限也适用于内存复杂度，因为在图探索期间存 储 了 依 赖 关 系d （ y 假 设 配 分 函 数 是 完 全 的 ， 则计 算 复 杂 度 xi ty 为 O（2·|E| ·（P-1）/P），最坏情况是用两个消息（扩展和稳定）获得的。Tion）每边交换。从理论上讲，我们的D TD算法的复杂度为O（|E|），但实际上它显示出非常有效的，只有0。01%的总交换消息用于终止检测。 实际上，协调员具有足够准确和最新的分布式计算状态映像，只需少量尝试即可执行DTD4实施和实验我 们 实 现 的 DSOLVE 和 CCOORDINATOR （ 8500 行 C 代 码 ） 已 集 成 到 使 用OpEN/CENSORSAR环境[12]开发的通用BES分辨率库CENSORSARSOLVE[20因此，我们立 即 获 得 了 CAD pverification toolbox [13] 的 BIMSIMULATOR[20] on-the-the-the-y等价性检查器的分布式版本，它使用CASSARSOLVE作为验证引擎。这个工具体系结构是高度模块化的，允许将前端（将等价关系编码为Bes）与后端（BESresolution）。为了计算布尔变量Xp，q的后继，表示状态p和q模给定关系的等价性，前端，在每个worker上顺序且独立地调用，根据该关系的定义，从p和q开始向前探索两个LTS（参见第2节中的表格）。注意对于弱等价关系（分支，观察，τ.a，安全），前端必须在两个LTSs中的τ-转换上执行我们已经进行了广泛的一组实验上的集群20XEON 2.4 GHzL的LINUX PC的，与1.5 GB的主内存，通过千兆网络互连。所考虑的LTS主要是从VLTS基准套件[1]中提取的，该基准套件被设计为对在大型图上操作的算法和工具（例如分布式等价检查器）进行科学评估的参考标准本节只展示了十几个至少需要几秒钟计算的实验。 请注意，为了获得性能的准确图像，在下面描述的实验结果中，我们排除了系统相关活动的固定成本（在远程节点上加载代码，连接初始化和复制L文件），我们只保留了分布式解析和终止检测的成本每个实验我们做了十次。每条曲线上的每个点代表与所获得的测量值相对应的八个值的平均值，不包括最大值和最小C. 茹贝尔河Mateescu/Electronic Notes in Theoretical Computer Science 128（2005）47594.1加速比量化并行算法效率的一种方法是计算绝对加速比S=T1/Tp，方法是将最著名的单处理器（顺序）算法的单处理器时间T1和P个工作机的时间Tp图3显示了比较分布式版本的BI模拟器（基于DSOLVE）和其顺序版本（基于CENSORSARSOLVE的广度优先搜索算法）的性能的实验数据。对于每个等价关系R和LTSM，实验涉及M与MR的比较模R，其最小化版本w.r.t. R. 选择这种比较有两个原因：（a）它再现了一种情况在实践中经常遇到，当设计师指定系统行为（协议）及其外部行为（服务）时，它们在这里对应于M和MR;（b）它代表了最坏情况下的行为，因为算法必须探索B（以及两个LTSs）完全在决定M和MR的等价性之前。我们还-形成了各种实验比较非等价LTSs：在所有情况下，分布式和顺序版本的BI模拟器在发现反例方面都非常快。强等价性。 图3（a）显示了在一组示例上使用分布式B I模拟器进行强等价性检查时获得的加速比，按大小递增排序，从9. 757·10 3个州和24个。352·103转换（dle 10）到8. 082·10 6个州和42. 933·106转换（vasy8082 42933）。强等价非常适合于分布：在前端花费的时间很少（不需要τ转换的传递闭包），曲线显示从低（仍然比顺序时间好）到几乎最佳 此外，当LTS大小增加时，加速比变得更好。为例如，实验BRPm 3 n 30（具有3次重传和分组长度30的有界重传协议，即5.957·10 6 states，9. 225· 106次转换）花费了332.53秒，而具有13个工作者的并行检查花费了29.06秒（加速11.5）。τ.a和安全当量。图3（b）显示了τa在一组与强等价（安全等价显示了类似的行为）相似的示例上这些等价的计算涉及到τ-转移上的广泛的传递闭包（执行顺序地由每个工作者上存在的前端）和非常小的BESs，在LTSs包含许多τ-跃迁的情况下。60C. 茹贝尔河Mateescu/Electronic Notes in Theoretical Computer Science 128（2005）47dle10vasy_65_2621vasy_66_1302dle03vasy_157_297b57vasy_574_13561vasy_720_390fw6BRPm3n25BRPm3n30vasy_8082_42933理想加速因此，观察到的加速比是20比强等效低1816岁，开始对大LTs感到14次 作为 vasy8082 42933，其中加速比为8.22，8工人64200 2 4 6 8 10 12 14 16 1820工人数量(a) 强等效2018分 支 等 价 和 观 测 等 价 。 图 3（c）显示了观测等价性（分支等价性表现出类似的行为）。相反 到A.A和 安全当量Lences ， theBES s encoding 编 码observa观察-16141210864200 246 8 10 12 14 16 1820工人数量函数和分支等价性大得多，因此分布式分辨率对性能具有更强的影响。 因此，曲线通常显示出更好的加速，特别是对于具有少数τ跃迁或确定性跃迁(b) τ.a等价201816141210864200 2 4 6 8 10 12 14 16 18 20工人数量(c) 观察等效性图3。三个等效的行为，等 作为 vasy65 2621，在13个工人的情况下，加速比增长到7.86 。全 球观 测结 果可 以通 过w.r.t. L的性质被检查。影响分布式系统性能的三个因素B模拟器：大小 在LTSs中，τ-跃迁的百分比，以及去-非决定论的程度。因此，当LTSs中既不存在τ-转换也不存在非确定性时，则对于所有等价关系都实现了良 好 的 加 速 比实 验瓦 西11125290，vasy574 13561， vasy65 2621，或vasy8082 42933. 恰恰相反，τ-跃迁百分比的增加导致τπ.a的低加速比，安全等效性（因为昂贵的前端计算），但对于强和观测等效性仍然有很好的加速（因为重要性），vasy_18_73scsiAvasy_65_2621vasy_157_297vasy_164_1619cwi_214_684vasy_1112_5290B200vasy_4338_15666BRPm3n30vasy_8082_42933理想的加速比vasy_18_73scsiSpBRPm3n4vasy_65_2621dle18vasy_157_297vasy_386_1171vasy_574_13561vasy_720_390vasy_1112_5290B200vasy_8082_42933理想加速加速比加速比12加速比10C. 茹贝尔河Mateescu/Electronic Notes in Theoretical Computer Science 128（2005）4761如图3上的实验BRPm3n30所示。类似地，增加非决定性和τ-跃迁的百分比都会产生大的BESs。在这种情况下，只有强等价性才能在合理的时间内终止（顺序少于45分钟），并在图3（a）的实验b57中显示出高加速弱等价或者不能终止（例如，对于B57的观察等效性），或者它们没有显示加速（例如，τα和安全性B200的等效值4.2扩展性通过上述实验测量以及图1所示的可扩展性结果，提供了对DSOLVE四、180160140120100806040200P=3p=5p=7p=11p=200 2e+06 4e+06 6e+06 8e+06 1e+07 1.2e+071.4e+07问题大小（转换）图4上的每条曲线表示实验BRPm3nK（具有3次重传和分组长度K从4到10变化的有35）在X的固定数量P上使用强等价的线性级数曲线表明，DSOLVE是良好的-见图4。可扩展性（相对于 问题规模适应问题规模的增加，有效地利用记忆和记忆。至于另一个大型示例，DSOLVE处理实验b200（具有200个不同消息的AlternatingBit Protocol）的强等价性检查，其生成的BES大小为二、4· 108个变量，在大约24分钟内与15名工人，而顺序由于当前的实现限制，B ES大小（最大为1。6· 107个变量）。4.3记忆我们已经证明了性能在运行时间方面是合理的。时间（秒）62C. 茹贝尔河Mateescu/Electronic Notes in Theoretical Computer Science 128（2005）47201510500 2 4 6 8 10 12 14 16 18 20工人数量图五.记忆w.r.t. 问题规模然而，现有的顺序算法的内存限制是主要的动机分布。图5通过实际实验证明，DSOLVE有效地利用了理论。它提供了在十几个按大小递增排序的VLTS从 9· 103 状 态 ， 25· 103 转 换 到8·106states，4·3·106转换LTs并且随着节点数量的增加（从2到20）。我们只考虑DSolve算法所使用的数据结构，包括用于存储布尔变量的哈希表，以及包括通信缓冲器的Cubisar网络库。增加更多工作者的影响相当低，这由总分布式内存消耗与相应的顺序内存消耗之间的比率显示，该比率几乎没有增加。待检查的LTS越大，比率越低。5结论和今后的工作我们提出了DSOLVE，一个新的算法上的分布式分辨率的BESs使用多台机器连接 DS OLVE在分布式版本的B ISIMULATOR中用作验证引擎，B isimulator是一种在C AD p工具箱[13]内开发的在线等价性检查器，使用Op EN/Censisar环境进行L TS探索[12]。在一个PC集群上使用基准测试实例和五种广泛使用的等价关系进行的实验表明，该分布式版本具有准线性的加速比和良好的可扩展性w.r.t. BI模拟器的顺序版本。DSOLVE的实现是独立于应用程序的，并集成在通用的Censar-SOLVE库[20]中，该库已经为在线BES分辨率提供了四种不同的顺序算法。我们目前正在使用DSOLVE来获得使用CensarSOLVE构建的其他应用程序的分布式版本，例如无交替的μ-演算模型检查[20]和τ-一致性约简[23]。我们还计划用其他等价关系扩展BISIMULATOR，例如马尔可夫互模拟[15]。引用[1] http://www.inrialpes.fr/vasy/cadp/resources/benchmark_bcg.html网站。dle10vasy_65_2621vasy_66_1302dle03vasy_157_297b57vasy_574_13561vasy_720_390fw6BRPm3n25BRPm3n30vasy_8082_42933理想内存比总标准杆。内存/序列存储器C. 茹贝尔河Mateescu/Electronic Notes in Theoretical Computer Science 128（2005）4763[2] H. R.安徒生模型检查和布尔图。Theoretical Computer Science，126（1）：3[3] H.