散列压缩扩展的分布式内存LTL模型检测算法及实验评估

可在www.sciencedirect.com在线获取理论计算机科学电子笔记296（2013）79-93www.elsevier.com/locate/entcs使用Hash Compaction1的J. Barnat，J.Havl'soughtcecekanddP.Rockai2捷克布尔诺马萨里克大学信息学院摘要利用散列压缩扩展了一个分布式内存显式状态LTL模型检测算法（OWCTY）。我们提供了一个详细的描述，改进的算法和正确性的论点在理论部分的文件。此外，我们提供了一个实现的算法的一部分，在E的外部和分布式内存模型检查器D i V，并使用这种实现的方法，我们报告的实验部分的实际评估。关键词：模型检测，LTL，分布式，哈希压缩，OWCTY1介绍模型检查[8]是一种已建立的方法，用于验证硬件和软件系统以及协议规范的正确性，以满足通常使用某些已建立的时态逻辑表示的正式指定的时态要求。最广泛的逻辑是CTL（计算树逻辑，通常应用于同步系统是规范的硬件设计）和LTL（线性时序逻辑，异步系统验证的主要工具即软件和通信协议）。模型检测的研究主要关注模型检测过程的内存需求（俗称在同步系统的CTL模型检测中，最受欢迎和公认的技术是基于符号表示的。不是存储单个状态，而是使用合适的紧凑结构编码的状态集，最常见的是BDD（二元决策图）。成功1这项工作得到了捷克科学基金会第2000号拨款的部分支持GAP 202/11/03122电子邮件：{barnat，xhavlic 4，xrockai}@ fi.muni.cz1571-0661 © 2013 Elsevier B. V.在CC BY-NC-ND许可下开放访问。http://dx.doi.org/10.1016/j.entcs.2013.07.00680J. Barnat等人理论计算机科学电子笔记296（2013）79这种方法已经相当压倒性，现在它是该领域的默认方法-显式状态工具几乎从未在硬件应用程序中使用过然而，没有明显的优越的方法已经出现了显式状态LTL模型检查器的异步软件系统，其中所需的体系结构的大小可以指数增长的系统进程的数量请注意，在LTL模型检验的情况下，在LTL指定的处理过程中也存在指数爆破，然而，这通常不是实际的限制因素，因为单个LTL公式通常很小。 真正的瓶颈在于被验证系统的状态空间的大小。随着最近模型检测直接应用于（并行）程序的出现，内存限制变得更加紧迫[22，2，25，18，11]，而不是更传统地使用手动构造，简化和抽象的模型。虽然单个计算机中可用的内存量一直在稳步攀升，但显式状态模型检查器仍然非常受限。分布式内存工具是克服这种情况的更直接的方法之一，并且与偏序约简[21，10，23]一起是目前需要100%忠实结果的唯一选择。然而，存在一系列折衷方法，在模型检查过程中引入误差幅度，从而显著减少内存使用。这些方法包括散列压缩[27，28]或位状态散列[12，14]等技术。在本文中，我们专注于结合哈希压缩与一个特定的并行LTL模型检测算法。哈希压缩是一种广泛且成功地应用于共享[19]和分布式内存环境[5]中安全（可达性）属性的模型检查的配备了哈希压缩的算法将状态的哈希值存储在哈希表中，而不是完整的状态表示。这种算法的存储器消耗减少并且独立于个体状态表示的大小（散列压缩状态总是相同的大小）。然而，如果多个不同的状态具有相同的散列压缩表示，则状态空间的散列压缩图不等于原始状态空间图，因为这些状态冲突成一个状态。幸运的是，大多数哈希压缩的经验表明，只有原始图的边缘部分被省略。使用散列压缩和位状态散列，误差容限非常小（可能小到百分之一）虽然节省了很大的（70%或更多），但在相当多的情况下做出这样的妥协是值得的。此外，还有一些技术可以限制哈希冲突的数量[28]或完全解决哈希冲突[26]。例如，ComBack方法[26]扩展了散列压缩技术，为每个状态存储额外的整数，并将backedge存储到其前任状态。这允许使用回溯机制来即时解决散列冲突，然而，代价是不平凡的额外存储器。其它散列压缩相关技术建议，例如，增量哈希，以便有效地处理非常大的状态描述符[17]。哈希压缩和位状态哈希方法在可达性分析中的应用是直接的，即使与分布式内存结合使用也是如此。J. Barnat等人理论计算机科学电子笔记296（2013）7981处理.这是因为对于可达性分析，哈希压缩图中的状态冲突可能只会导致错过一些错误。然而，在活性属性的情况下，情况要复杂得多，其中将散列等价状态合并为单个状态可能会引入新的，因此是虚假的系统行为。因此，在散列压缩的状态空间图上执行模型检查可能会导致虚假的反例和遗漏的错误。对于串行LTL模型检测算法，该问题通过深度优先搜索（DFS）堆栈的帮助得以避免。基于DFS的散列压缩算法利用DFS堆栈存储当前探索路径上的完整状态，因此它们只考虑真实的系统行为。然而，这不适用于任何非基于DFS的算法。在本文中，我们介绍了一个有效的组合散列压缩技术与一个特定的非DFS为基础的算法的分布式内存LTL模型检测。2预赛2.1LTL模型检验显式状态LTL模型检查的自动机理论方法[24]利用了这样一个事实，即可以由LTL公式表示的每一组执行都可以由Bu？chi自动机描述。特别地，本文建议用一个系统自动机来表示所有不满足公式的执行，用一个性质自动机或否定断言自动机来表示所有不满足公式的执行。这些自动机被合并到它们的同步产品中，以检查是否存在违反公式所表示的属性的系统执行。产品自动机识别的语言是空的，当且仅当没有系统执行是无效的。Buéchi自动机的语言空性问题可以表示为一个概念中的接受循环判定问题。 EachBuchi自动机可以自然地用一个自动机图来标识，该自动机图是一个有向图G =（V，E，s，F），其中V是状态集（n = 1）。|V|），E是一组边（m = |E|），s是初始状态，FV是一组接受态。我们说G中的一个循环是可接受的，如果它一个接受的状态。设A是一个布希自动机，GA是一个对应的自动机图.然后A识别非空语言，如果GA包含一个接受从s可到达的周期。因此，LTL模型检验问题被简化为自动机图中的接受循环检测问题接受循环检测的最优顺序算法使用深度优先搜索策略来检测接受循环。各个算法在它们的空间要求、产生的反例的长度和其他方面有所不同。嵌套DFS算法被广泛应用于模型检测中，被认为是最适合于显式状态序列LTL模型检测的算法。该算法由Courcoubetis等人提出[9]其主要思想是使用两个交错搜索来检测可达接受循环。第一个搜索发现接受状态，而第二个，嵌套的，检查自我可达性。算法的时间复杂度与图的大小成线性关系，即：时间复杂度O（m+n），82J. Barnat等人理论计算机科学电子笔记296（2013）79其中m是边的数量，n是状态的数量。嵌套DFS算法的有效性是由于图被探索的特定顺序而实现的，这保证了状态不被访问超过两次。事实上，所有最著名的算法都依赖于相同的探索原则，即DFS计算的后序。众所周知，后序问题是P-完全的，直接基于DFS后序的可扩展并行算法是不可能存在的。 几种解决方案 以克服并行环境中的后序问题。并行算法的开发采用额外的数据结构和/或不同的搜索和分布策略。还有一些方法基于运行几个嵌套DFS实例，并具有有限的信息共享，如[15]所示。对于接受循环检测的并行算法的调查，我们参考[3]。 本文主要研究了单向捕获算法（One-Way-Catch-Them-Young algorithm，简称OWCTY），它是C.能够在并行或分布式环境中进行LTL模型检查的公开可用工具包括SPIN[13]，DI VIN E[4]和LTSMIN[16]。2.2OWCTY算法给定一个自动机图GA=（V，E，s，F），OWCTY算法的目标是检测从s可到达的GA中的接受循环的存在。该算法的思想是迭代地计算一组状态X，这些状态位于s可达的某个接受循环上或可达。计算本身由四个阶段组成，它们细化了近似集SX。初始化阶段是从s可到达的所有状态的集合。任何随后的可达性阶段从S中移除顶点，只要它们从已经在S中的某个接受状态不可达;这是通过从SF运行可达性来实现的。对于SF中的每个顶点，该阶段还计算由S导出的子图上的前驱计数（入度）。 然后，消除阶段移除不位于循环上的顶点。这也是通过从SF运行可达性来实现的，但是只跟随导致入度变为零的状态的边。这样的状态从S中移除，并且它们的后继者的阶数减少。最后，在每个可达性阶段之前执行复位阶段，以将所有状态的前驱计数初始化为零。除了初始化阶段，所有阶段都重复执行，直到找到一个定点。参见描述OWCTY算法的伪代码，如算法1所示。如果到达定点且S不为空，则通过从SF中选择一个状态并从其开始可达性，在此过程中从S中删除所有如果再次到达选定的状态，我们回溯并打印遍历的路径作为反例。否则，我们从SF中选择另一个状态并重复搜索（忽略任何已经访问过的状态，即不在S中的状态）。由于OWCTY是正确的，这一步保证会产生一个反例。所有通行证访问每个州最多一次，并遵循每个边缘最多一次，所以J. Barnat等人理论计算机科学电子笔记296（2013）7983S1sS2...Fig. 1.假反例，假设s1≠s2它们在图的大小上是线性的。迭代次数在图的高度上最多可以是线性的，但实际上非常低。 OWCTY不依赖于后序，因此可以很好地并行化。我们参考[7]的细节和正确性的证明。2.3OWCTY的在线扩展OWCTY算法的初始化阶段可以扩展到允许在线验证。最简单的选择是在枚举接受状态的后继者时查找自循环。更复杂的技术是基于MAP算法来检测接受周期[6]。它要求在常数时间比较过程中所有状态都有一个全序。然后我们可以在遍历图时传播最大接受如果一个状态被证明是它自己的接受前驱，那么这个图就保证有一个接受循环。然而，原始MAP算法的迭代不能在线性时间内执行，因为用于传播接受后继者的任何边缘稍后可能再次用于传播另一个（给定顺序中更高的）。此外，MAP算法可以使用线性数量的迭代来完成。在[1]中表明，在OWCTY算法的初始化阶段可以执行MAP算法的一次迭代，而无需重新传播，这允许在具有非平凡反例的各种模型上提前终止。3基于OWCTY算法的哈希压缩方案，如[28]中所述，改变了在图遍历期间使用哈希表的方式通常，所有访问状态的完整显式表示存储在哈希表中。使用哈希压缩，只有状态表示的哈希存储在那里，完整的表示只保存在BFS使用的队列中，我们需要它来生成后继者。在并行和分布式环境中，线程之间的通信可以通过一组队列来实现，这些队列充当将状态从一个线程发送到另一个线程的通道为了节省更多的内存，哈希压缩方案可以伴随着一种机制，一旦这些队列达到一定长度，就会将其内容保存到磁盘[5]。哈希压缩以前只用于可达性分析，我们只需要跟踪访问状态以及是否存在某些哈希 哈希表中的数据为我们提供了这些信息。OWCTY算法需要存储84J. Barnat等人理论计算机科学电子笔记296（2013）79∈←¬←←/∈¬/∈¬←←∅←−∈算法1：OWCTY1I初始化2个重复3oldSize← |S|4for alls∈Vdos.pre←0/* Reset */5将所有状态从SF排队到q6REACHABILITY7将所有状态从SF排队到q8E消除月9日至|S|= oldSize10 返回|S|> 0个11个程序I初始化12将init排入q13whileq.emptydo14t q.pop（）15如果t S，则16将t加到S17对于所有的（t，u）∈E，u确实排队到q18个程序R可达性19S20whileq.emptydo21t q.pop（）22如果t S，则23将t加到S24对于所有的（t，u）E做25u.pre u.pre+126将u排入q27 过程E消除28.空的时候，29吨q.pop（）如果t.pre= 0，则31从S中删除t32对于所有的（t，u）E做33u.pre u.pre134将u排入q每个状态的更多信息，即近似集中的前驱计数和成员资格。我们确定了在使用OWCTY算法进行哈希压缩时出现的两个主要问题。(i) 可达性阶段可能会遇到在初始化阶段未发现的状态此外，可达性可以发现不同的状态集时，从同一组状态运行多次。这可能导致前趋计数器变为负值或大小S变得比其在前趋中更高J. Barnat等人理论计算机科学电子笔记296（2013）7985我们的迭代。这也意味着比较当前和上一次迭代中近似集的大小是否相等不再可靠地检测到到达定点。(ii) 该算法可以报告假阳性（假接受循环）。当某个状态s2可以从接受状态s1到达并且这两个状态具有相等的散列时（我们将用s1≠s2表示），就会发生这种情况。当可达性从s1开始时，s2在某个点被访问，其前驱计数增加到1。但是由于s1和s2共享前导计数，并且s1不会在消除阶段被消除，因为它具有非零前导计数。图1中描述了这种情况-虚线边实际上不是图的一部分，但由于哈希冲突，来自s的边似乎同时指向s2和s1。为了解决上述问题并最大化状态空间覆盖，我们以以下方式改变了OWCTY算法• 我们添加了一个队列来存储接受状态-Qacc。使用哈希压缩，不再可能从哈希表中获得所有接受状态，因此我们必须单独存储它们，以便能够从它们开始可达性。我们选择了队列，因为它可以很容易地存储在磁盘上，以减少内存需求。• 在初始化阶段，遇到的每个接受状态都被排入Qacc。• 可达性阶段从Qacc中的所有状态开始，并且当遍历通向接受状态的任何边缘时，目的地状态被入队到Qacc中。Qacc的新内容将在以下阶段使用• 消除阶段忽略S之外的状态。• 当S中的状态数不减少时，退出算法的主循环。• 在算法的最后，我们增加了一个新的阶段来检查发现的接受循环的有效性它的工作方式与上一节中描述的OWCTY的反例生成阶段相同。唯一的区别是它可能失败，因为没有实际的反例。包含所有这些变化的OWCTY版本的伪代码被列为算法2和3。我们的方法完全解决了第二个问题，这意味着它永远不会报告没有反例的模型，但它显然会错过现有的反例。我们使用队列Qacc的方式确保了在切换迭代时消除错误的接受循环。这可以在图1中呈现：状态s1将在s2之前被推入Qacc，并且从s1开始的可达性阶段将增加所有三个状态的前驱计数，这将防止它们被消除。然而，由于可达性阶段不遍历通向s1的任何边缘，因此s1不被推回到Qacc。这确保了下一次迭代将86J. Barnat等人理论计算机科学电子笔记296（2013）79← ||∈←| |S1S2S3图二、没有固定点的终止，假设s1≤s2≤s3不访问s1，并且所描绘的假接受循环将不再包含在近似集合S中。关于这些化学品如何工作的更正式的描述可以在第3.2节中找到。然而，由于只有在切换迭代时才执行错误接受循环消除，并且我们不再能够可靠地检测到达固定点，因此我们需要最终验证阶段来检测由于算法在到达固定点之前终止而所描述的算法可以通过添加接受自循环检测来扩展以允许提前终止，但是由于可达性阶段可以访问先前未被初始化阶段发现的状态，因此将该算法添加到两个阶段是有意义的。另一方面，我们决定不使用基于MAP算法的算法。原因是，它可以像OWCTY一样产生错误的接受周期，我们没有办法绕过它。在每个阶段中，任何状态（包括新添加的状态）最多只能访问一次，这意味着OWCTY算法的时间复杂度不受这些变化的影响。算法2：OWCTY HC1I初始化2个重复3旧尺寸S4for alls Vdos.pre0/* Reset */5.将Qacc中属于S的所有状态复制到q中并清除Qacc6REACHABILITY7将属于S的所有状态从Qacc复制到q8E消除9直到S >=oldSize10 返回验证3.1正确性正如我们在下一节中证明的那样，如果我们的算法到达一个定点，则结果集S要么是空的，要么包含一个接受循环。在这种情况下，不需要最后两点所述的措施。然而，由于我们无法可靠地检测到达定点，迭代过程可能会过早停止，我们需要验证阶段来防止报告错误的反例。这在图2中举例说明。当在所描绘的图上运行时，我们的算法将在两次迭代后退出，而不会到达固定点，因为即使S的内容在迭代之间发生变化，其大小也不会改变。然而，验证阶段将始终得出结论，没有接受周期，算法将提供J. Barnat等人理论计算机科学电子笔记296（2013）7987←∈←/∈¬¬←←/∈←∅¬←∧ ∈¬←−∈←∅←/∈¬算法3：OWCTY HC（续）1个程序I初始化2将init排入q3whileq.emptydo4t q.pop（）5如果t S，则6将t加到S7对于所有的（t，u）∈E，u确实进入q8如果t∈F，则将t排入Qacc9 过程可检索性10S11whileq.emptydo12t q.pop（）13如果t S，则14将t加到S15对于所有的（t，u）E做16u.pre u.pre+117将u排入q18如果u∈F，则将u排队到Qacc中19程序E消除20whileq.emptydo21t q.pop（）22如果t.pre= 0t S，则23从S中删除t24对于所有的（t，u）E做25u.pre u.pre126将u排入q27 程序验证28S29，而Qacc.空30磅一次31将a排入q32whileq.emptydo33t q.pop（）34如果t S，则35将t加到S36如果t=a，则返回 true37对于所有的（t，u）∈E，u确实排队到q38返回false正确答案注意，在OWCTY的反例生成阶段和我们算法的验证阶段中使用的循环检测过程88J. Barnat等人理论计算机科学电子笔记296（2013）79因此，只有在以下情况下，它才是完整的（如果有反例，则总是找到反例）：J. Barnat等人理论计算机科学电子笔记296（2013）7989S中的所有状态都位于一个循环上，或者可以从S中的一个循环到达。OWCTY的正确性（见[7]的证明）确保了如果达到一个定点，这个条件总是满足的。在算法在到达它之前终止的情况下，这可能导致反例遗漏。验证阶段只有在状态a到自身存在路径且状态a在Qacc中时才能返回true。比较是用状态a的完整表示来完成的，所以它不受哈希压缩的影响。这一点，以及Qacc只能包含可到达的接受状态的事实，保证了如果返回true，则存在可到达的接受循环。因此，验证阶段是正确的。在并行环境中需要额外的措施，即在验证阶段的外循环中需要全局同步，以确保所有并行工作者具有相同的状态a。3.2消除错误的接受周期虽然不需要正确性证明，我们证明了我们的假接受循环消除算法是正确的。换句话说，我们证明，如果到达一个定点，近似集S不包含假接受循环。在本节中，我们将介绍哈希压缩状态空间的概念。给定一个状态空间图G=（V，E），我们定义一个哈希压缩图G=（V，E，），其中等价关系对应于哈希相等（即，v1= hash（v1），v2=hash（v2））。在下文中，集合W=V\n是V根据n的等价类的集合。此外，我们定义了一个从W到V的内射映射p，使得p（w）=v<$v∈w.在给定的散列压缩图G上有许多这样的关系。我们定义一个由投影p导出的图为：Gp=（W，Ep），其中w1，w2∈ W. （w1，w2）∈ Epv2∈ w2. （p（w1），v2）∈E.我们可以看到，即使在基础图G中没有圈，（接受）圈也可以在诱导图Gi中形成。因此，一个使用固定投影p的算法，即使在不包含任何循环的状态空间中，也必然会发现接受循环，因此既不是过近似也不是欠近似。然而，用于特定图探索（pn）的投影取决于发现顺序：从每个集合w，发现的顶点v第一个选择为pn（w）。我们还观察到在一个特定的G pn中的每一个假诱导圈C都包含一个w满足条件，使得<$v2∈w.pn（w）=/v2<$（pn（w），v2）∈E<$。此外，我们知道（v2，pn（w））/∈E<$（否则，有一个接受图G中的循环）。假设n是一次淘汰，m是下面的可达性通过。 我们知道pm（w）pn（w）：在可达性pass，pn（w）不会立即被访问（即使它是初始队列上的第一个接受状态，我们在第一次将它们出列时也不会将这些状态标记为已访问）。我们还知道，（ pn（w），v）∈E+<$（v，pn（w））/∈E<$（同样，G中会有一个接受圈）。由于至少有这样的WJ∈C，WJ=p-n1（v）在wis之前被访问，并且由于Cw是一个伪接收圈，w必须从WJ到达，因此pm（w）/=pn（w）。最后，这意味着，90J. Barnat等人理论计算机科学电子笔记296（2013）79对于随后的消元过程，w不是wJ的前趋并且假周期C不再存在（由于从w到WJ的路径丢失）。这与原始OWCTY算法的正确性一起，确保了当到达定点时没有错误的接受周期4执行情况和结果为了评估我们的方法，我们已经在验证工具DI VIN E.我们使用了一个32位哈希的开放哈希方案Jenkinslookup 3 hash function的函数我们的实现还包含接受自循环检测并在磁盘上存储长队列。第一个实验侧重于内存使用，并将我们的算法与目前在E[4]中D i V中实现的OWCTY版本进行比较。此版本包含第2.3小节中描述的两个扩展。我们对BEEM数据库中的模型进行了大量实验[20]。事实证明，许多验证运行使用的内存太少，无法进行有意义的算法比较。 当DI VIN E在空模型上运行时，它使用259 MB内存，因此我们决定仅考虑验证运行使用超过280 MB内存的模型此外，我们发现许多实例包含接受状态上的自循环，因此检测其中的反例是一个简单的图遍历问题，不适合我们的实验。我们包括一个这样的模型进行比较。从表1中可以看出，我们的方法为更大的模型节省了25- 70%的内存，但它总是会导致一些速度下降。这是由I/O操作和在某些情况下更高的迭代次数引起的该表还显示，某些型号的内存需求有所上升我们发现，在所有这些情况下，由于MAP算法的一次迭代，原始OWCTY算法提前终止，因此仅访问了状态空间的一小部分。标记为coverage的列显示了使用和不使用哈希压缩访问的状态的比率，尽管只计算在初始化阶段访问的状态。在MAP扩展导致提前终止的情况下，覆盖率超过100%。我们决定包括这些情况，以显示相对于最新版本的OWCTY算法的实际内存节省在我们的实验中，哈希压缩从未导致某些属性被错误地识别为有效。然而，这可能是由BEEM模型的结构造成的，在某种意义上，任何具有反例的模型通常包含多个类似的反例。然而，这个属性在一般的异步系统模型中是普遍存在的，我们并不期望这个效应会被BEEM中的选择此外，我们注意到，我们的算法发现的反例在许多情况下明显短于原始OWCTY在DI VIN E中报告的反例。我们发现这是由于接受状态的顺序在反例生成阶段，每个算法都有所不同。当主循环终止并且近似集S不J. Barnat等人理论计算机科学电子笔记296（2013）7991最短CE原稿OWCTY散列压缩。国家（·103）相对覆盖率（%）时间（s）RAM（MB）时间（s）RAM（MB）时间（%）RAM（%）186+18269.2864201132.13470642742+320-27178.842没有一28.1483076.89514746+173-3899.993没有一25.4154892.573781573+264-3199.974没有一41.3747346.79257999+13-4699.985二十一加四十29.1835881.562822000+180-21104.366十九加四十33.6339379.512892239+136-2699.977没有一36.5651786.852862239+138-4599.9785+411.85628316.8810452165+2574+15638155.599没有一18.9745821.372901978+13-3799.9710没有一18.8645821.922941978+16-3699.9711没有一6.132796.572561189+7-899.8112没有一16.3074717.082813098+5-6299.5813123+121112.172468110.63101411245-1-5998.841439+9128.081147112.978005945+302-30101.4715没有一68.081406524.878376012+671-4099.5016二十四加九十四25.42964130.888054371+415-16136.9017没有一34.43115739.523616047+15-6999.2518没有一26.06115527.793634955+7-6999.2919没有一104.992553441.9212529533+321-5199.082025+8031.001133287.8412754993+828+13189.6921十二加十20.2359353.943501758+167-41128.35228+1021.1858265.193702256+208-36201.91234+1791.35934119.695604555+31-4099.94243+18105.581034128.855204628+22-5099.9525没有一94.751053153.345194627+62-5199.9526没有一508.3664003595.7724181825+607-6299.52表1与原始OWCTY的比较空，则OWCTY算法检查S中的所有接受状态并查找一条从这些状态之一通向自身的路径。首先返回这样的路径，一个反例在DI VIN E中实现的OWCTY通过遍历哈希表来获得属于S的一组接受状态，这意味着它们的检查顺序是随机的。另一方面，我们的算法保持这样的状态在一个队列中，这导致从初始状态的路径较短的状态被检查较早和反例一般较短的线性部分。第二组实验的重点是可扩展性。我们选择了两个模型（一个有反例，一个没有反例），并通过使用不同数量的线程运行两种算法来测量散列压缩如何影响OWCTY算法的可扩展性。如图3至图6所示，修改后的算法与原始算法相比具有很好的扩展性。相对速度降低似乎与线程数量无关，但相对内存节省似乎随着线程数量的增加而减少一种可能的解释是，增加更多的线程（二次）会增加用于将状态从一个线程传递到另一个线程的队列数量，这意味着单个队列的平均长度会减少，并且我们不能将它们有效地保存在磁盘上，因为92J. Barnat等人理论计算机科学电子笔记296（2013）7940353025201510502 4 6 8 101214 16线程两千一千八百一千六百一千四百一千二百一千80060040020002 4 6 8 101214 16线程图3.第三章。rether.6.prop2上的可扩展性（平方-哈希压缩）1101009080706050403020102 4 6 8 101214 16线程三千五百三千两千五百两千一千五百一千50002 4 6 8 101214 16线程图四、rether.5.prop3上的可扩展性（squares-hash compaction）120100806040202 4 6 8 101214 16线程两千一千八百一千六百一千四百一千二百一千80060040020002 4 6 8 101214 16线程图五. szymanski.4.prop3上的可扩展性（平方-哈希压缩）出于性能原因，I/O操作的总频率必须保持较低时间（秒）时间（秒）时间（秒）内存（MB）内存（MB）内存（MB）J. Barnat等人理论计算机科学电子笔记296（2013）7993三千五百三千两千五百两千一千五百一千50002 4 6 8 101214 16线程八千七千六千五千四千三千两千一千02 4 6 8 101214 16线程见图6。anderson.6.prop2上的可扩展性（squares - hash compaction）5结论在本文中，我们提出了一种方法，使用哈希压缩与OWCTY算法。这构成了一种新的方法来对抗状态爆炸问题时，验证LTL属性，利用以前只考虑可达性分析的技术。我们的实验表明，内存需求可以减少25至70%，即使是相对较小的模型，所提出的方法是可行的，即使在并行和分布式环境中，因为它没有一个完美的可扩展性的OWCTY算法。我们的方法是基于使用一个队列来存储接受状态，消除错误的接受周期和最终检查。作为一个侧面的例子，使用队列也使我们能够找到比当前OWCTY实现更短的反例。虽然使用哈希压缩永远不会产生完整的算法，当由于内存限制而无法通过标准方法进行验证时，它可以提供极大的帮助。对于相对较小的状态，无损状态压缩可能是更可行的方法，但特别是当状态可能占用数千字节的模型检查实际代码时，哈希压缩可能是正确的技术。引用[1] Barnat，J.，L. Brim和P. Rockai，对弱LTL属性的验证最优的On-the-paral lel M o del Che cking A ltaxm，出现在计算机编程科学（2012）中。URLhttp://dx.doi.org/10.1016/j.scico.2011.03.001[2] Barnat，J.，L. Brim和P. R oc kai，Towa rdsLTLM odelChe ckingofUnm odifiedThreead-Based C&C++Programs，in：NASA Formal Methods Symposium，LNCS7226（2012），pp. 252-267。[3] Barnat，J.，L.布里姆和我。Cern'a，LarrgeSystems的基本LTL模型检查，in：部件和对象F标准方法，LNCS中的第4111号，2005年，第100页。259-279.[4] Barnat ， J. ， L. Brim， M.Ces ka 和 P.R oRucc kai ， Divine ： Paral lelDistribut edM odelCh ecker（ Toolpa per ） ， in ： Parallel and Distributed Methods in Veri fication and High PerformanceComputational Systems Biology（HiBi/PDMC 2010）（2010），pp. 4-7.[5] Bingham ， B. ， J. Bingham ， F.de Paula ， J.Erickson 和 M.Singh ， G. 和 Reitblatt ， IndustrialStrength Distributed Explicit State Model Checking ， in ： Parallel and Distributed Methods inVerification and High Performance Computational Systems Biology（HiBi/PDMC）（2010），pp.28比36时间（秒）内存（MB）94J. Barnat等人理论计算机科学电子笔记296（2013）79[6] 布里姆湖I. 切埃纳山口 Mor avec和J. Si msa，Acceptingpre eecessorsa rebetterthanackedgeindistributed ltlmodel-checking ， in ： 5th International Conference on Formal Methods in Computer-Aided Design（FMCAD'04），LNCS 3312（2004），pp. 352-366.[7] 查埃纳岛 和R. Pe l'anek，Distribut edexplicitfaircachedete，in：P roc. SPIN车间，LNCS第2648（2003）号来文，第264页。49比74[8] 克拉克，E.，O. Grumberg和D. Peled，[9] Courcoubetics，C.，M. Vardi，P. Wolper和M. Yannakakis，用于验证时间属性的内存有效算法，在：CAV233-242。[10] Godefroid，P.，使用偏序来改进自动验证方法，在：第二届计算机辅助验证国际研讨会论文集，CAV'90（1991），pp。176-185网址http://dl.acm.org/citation.cfm?电话：+86-647759.735044传真：+86-647759.735044[11] Holzmann，G.和M. H. Smith，Software Model Checking - Extracting Verification Models from SourceCode，Formal Methods for Protocol Engineering and Distributed Systems（1999），pp.481六十五比七十九[12] Holzmann，G. J.，关于自动化协议分析的限制和可能性，见：IFIP WG6.1第七届协议规范、测试和验证国际会议论文集VII（1987年），pp. 339-344.网址http://dl.acm.org/citation.cfm?电话：+86-510 - 88888888[13] Holzmann，G. J.，该模型检查自旋，IEEE trans.softw。Eng.23（1997），pp. 279-295.网址http://dx.doi.org/10.1109/32.588521[14] Holzmann，G. J.，位状态散列分析，Form。方法系统设计。13（1998），pp. 289-307.URLhttp://dx.doi.org/10.1023/A:1008696026254[15] Laarman，A.，R. Langerak，J. Van De Pol，M. Weber和A. Wijs，多核嵌套深度优先搜索，在：第九届自动化技术验证和分析国际会议论文集，ATVA'11（2011），pp. 321-335网址http://dl.acm.org/citation.cfm?电话：+86-20 - 55091788传真：+86-20 - 55091788[16] Laarman，A.，J. van de Pol和M.韦伯，多核ltsmin：结合模块化和可扩展性，在：美国宇航局正式方法第三次国际会议的会议记录，NFM'11（2011），pp。506-511.网址http://dl.acm.org/citation.cfm?联系电话：0531 - 8888888[17] Mehler ， T. 和 S. Edelkamp ， Dynamic Incremental Hashing in Program Model Checking ， ElectronicNotes in Theoretical Computer Science149（2006），pp. 51[18] Musuvathi，M.美国，D. 帕克A.Chou，D.R. Engler和D.L. Dill，CMC：A Pragmatic Approach toModel Checking Real Code ， in ： The Fifth Symposium on Operating Systems Design andImplementation，2002.[19] Nguyen，V.和T.Ruys，Incremental Hashing for SPIN，in：K.哈夫隆河Majumdar和J.Palsberg，editors ， Model Checking Software ， Proceedings of the 15th International SPIN Workshop ，LNCS5156（2008），pp. 232-249。[20] 佩拉内克河， 例如：用于显式模型的基准，例如：P roc。SPIN车间，LNCS4595（2