SMV垃圾收集机制：C2edl软件的应用与bug分析

理论计算机科学电子笔记55第3期（2001）URL：http://www.elsevie r. n l/l oc ate/en tcs/vol um e55. ht ml 页SMV垃圾收集机制Cindy Cristina1IBM海法研究实验室Matam先进技术中心，海法，31905以色列摘要本文介绍了一个经验的应用程序的规则库模型检查器的C语言编写的软件，使用工具C2edl。 C2 edl将ANSI-C代码翻译为规则库的输入语言EDL。虽然c2edl使用了一个激进的抽象，以解决软件模型检查的问题，由c2edl建立的抽象模型被证明是足够的，让SMV的垃圾收集机制的分析。使用c2edl和RuleBase，在RuleBase本身中发现了8个bug，它使用相同的垃圾收集机制。1引言近年来，模型检查作为硬件设计的强大工具得到了广泛的认可近年来，模型检测在软件中的应用引起了人们越来越多的兴趣。一种方法[22，23，36，20，2，37]是开发专门用于软件的新技术第二种方法[15，26，28，27，14]是使用允许应用现有工具的建模技术。前者的优点是它允许直接解决软件模型检查中固有的困难，而后者的优点是投入现有工具的多年开发和优化不会浪费。在本文中，我们描述了第二种方法的经验，使用的工具c2edl。C2 edl将ANSI-C代码翻译为EDL，这是RuleBase模型检查器的输入语言[6]。C2edl使用了一种激进的抽象来解决软件模型检查的问题。然而，抽象1 电子邮件地址：eisner@il.ibm.comc 2001年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。艾斯纳2由c2edl建立的模型被证明是足够的，可以分析SMV的垃圾收集机制。使用c2edl和RuleBase，在RuleBase本身中发现了8个bug，它使用相同的垃圾收集机制。本文的其余部分组织如下。第2节将本工作与相关工作进行了比较。第3节介绍了规则库的一些背景知识。第4节描述了一个程序如何以一种适合于符号模型检验的形式来表示。第5节介绍了工具c2edl。第六节讨论了模型检测在SMV垃圾收集机制中的应用，并给出了实验结果。第7节总结并指出了未来的研究方向。2与相关工作的许多以前的工作已经描述了验证软件的高级模型的过程在本文中，我们应用模型检查的源代码本身，通过自动生成的抽象，而不是一个手编码的高层次模型。有大量的模型检查应用于铁路联锁软件的源代码的工作[25，33，10，11，18，17]。虽然从技术上讲，铁路联锁是一个软件，但铁路联锁语言的语义非常简单，以至于Shepherd和St almarck将联锁称为类似硬件的系统[35]。本文将模型检测应用于通用C语言编写的软件中。Godefroid [22，23]描述了VeriSoft，一个用C或C++编写的并发软件的模型检查工具，并成功地验证了一个2500行并发C程序。[22，23]的重点是搜索算法，它执行各种显式状态空间探索。Stoller [36]对Java程序采用了类似于[22，23]的方法在本文中，我们不修改模型检测算法。相反，我们使用c2edl将C代码转换为模型检查器的输入语言，并使用现有的算法来验证程序的某些有用属性。Demartini、Iosif和Sisto [15]描述了SPIN模型检查器在Java多线程应用程序中的应用。它们描述了将Java 源代码翻译成SPIN 的输入语言PROMELA的过程。他们的目标和本文一样，是验证源代码，使用自动抽象技术来得到一个简化的模型。他们在玩具上展示他们的技术。Havelund和Pressburger [26]在他们的第一代工具Java Path中采用了类似于[15]的方法，但支持更多的语言，并注意到多达2000行代码的Java程序的结果。在[15]和[26]中，由于需要对Java的并发原语进行建模，翻译变得复杂，而c2edl使用的方法则没有这些问题。另一方面，[15，26]的翻译在某些方面比c2edl的翻译更简单，因为PROMELA语言允许它们保留比c2edl更多的原始程序结构。艾斯纳3EDL。Visser、Havelund、Brat和Park在[37]中提出了第二代Java Pathlogic。第一代将Java源代码翻译成PROMELA，而第二代则是一个成熟的Java定制模型相比之下，我们没有开发一个新的模型检查算法，但使用建模技术，允许现有的应用程序。Holzmann和Smith [28]提出了一种从源代码中提取验证模型的方法然而，它们的抽象过程只是半自动的，并且由用户手动编码的查找表和模型模板辅助。相比之下，c2edl的使用不需要人工干预。他们描述了将他们的方法应用于用C编写的商业呼叫处理软件的结果，尽管他们没有提到这个软件的大小。在[27]中，Holzmann描述了该方法在检查点管理系统中的另一种应用。同样，没有讨论软件的大小。Corbett等人[14]描述了Bandera，一种用于自动提取Nite状态模型的Java源代码。它们基于减少数据集的基数来执行用户引导的抽象，并提供用于指定附加抽象的语言。他们将Java翻译成一种中间语言，然后再翻译成一种模型检查语言。他们在一个玩具示例上演示了他们的方法，一个由60行Java代码组成的线程管道。相比之下，c2edl是完全自动的，我们提出了一个非平凡的应用程序的结果Esparza，Hansel，Rossmanith和Schwoon [20]描述了下推自动机的模型检查算法。他们和我们一样，采取了抽象所有变量值的激进方法。然而，它们并不局限于nite堆栈。相反，c2edl为RuleBase生成一个nite状态模型。他们给出了令人印象深刻的结果，随机生成的ow图（骨架程序）多达20，000行。最后，Ball和Rajamani [2]描述了Bebop，一个布尔程序的符号模型检查器。他们已经开发了一种专门的算法模型检查软件，这似乎是有限的检查属性直接表示为用户的可达性查询。相反，我们检查时态逻辑中表达的属性。他们解决软件语义困难的方法是将所有变量限制为布尔值，并将过程调用限制为按值调用参数。像[20]一样，它们并不局限于nitestate系统。他们显示了一个简单的家庭的程序越来越深层次的嵌套过程调用，但有限的非确定性的结果。相反，我们对嵌套的级别设置了人为的限制，但很容易处理高级别的非确定性行为。艾斯纳43预赛本文中描述的工作是使用RuleBase [6]进行的。RuleBase最初基于SMV的一个版本[32]。经过八年的发展[4，8，3，9，7，5，6，21]，原始SMV代码只是整个代码的一小部分。然而，SMV的垃圾收集机制仍然存在。RuleBase的输入语言是EDL，它是SMV语言的一种方言。RuleBase使用时态逻辑Sugar [4]作为其规范语言。Sugar结合了正则表达式和CTL的语法加糖功能。本文所描述的工作只使用了一种Sugar公式，一个Sugar蕴涵。非正式地，这样的公式由两部分组成：序列和必需条件。一个序列是一个计算路径的前缀，被描述为一个正则表达式。一个必要的条件是一个糖公式，它需要在序列的每个最终状态中保持。 例如，下面的糖公式：（1）ftrue[];a;b[];c[+]g（d）声明d需要保持在正则表达式ab c+描述的每个序列的nal状态。等效的CTL公式为：(2)：EF（a^EXE[bUE[cU（c^：d）]]）4将程序表示为一组下一状态函数将程序转换为一组适合模型检查的下一状态函数的过程类似于[31，13]。 我们以一个简单的例子来非正式地描述它，然后添加细节。考虑图1中的C函数getmax（）。我们用程序计数器（pc）的值来注释代码如果我们将整数a和max限制在0到3的范围内，那么我们可以int max（）;0int max = 0;1多夫2if（a> max）3return a;4int maximum（）;5g while（a）;6return（max）;7 GFig. 1.函数getmax（）按照变量的下一状态函数重写getmax（），如下所示在图2中我们已经将对a=input（）的调用表示为对变量a的非确定性赋值。其他变量的下一个状态函数是确定性的。为了简单起见，我们忽略了翻译return语句的细节（下面有一个包含函数调用的例子）。通过轻微的语法更改和添加状态变量声明，图2是一个完整的SMV或EDL程序，可以使用SMV或RuleBase进行模型检查艾斯纳5next（ a）=如果pc=0则0else if pc=4 then f0，1，2，3g else anext（ max）=如果pc=0则0else if pc=3 then aelse maxnext（ pc）=如果pc=0则1否则，如果pc=1，则2else如果pc=2那么如果a> max那么3 else 4否则，如果pc=3，则4否则，如果pc=4，则5else if pc=5然后if a然后1 else 6否则，如果pc=6，则7否则，如果pc=7，则7图二. 函数getmax（）表示下一状态函数intmax;8int maximum（）;9 G图三. 程序doit（）当然，一个有趣的C程序通常会比函数getmax（）更复杂。将转换扩展到其他类型的分支和循环语句是很简单的。但是，转换过程还应该能够处理复杂的数据类型、指针和函数调用，包括递归函数调用。所有这些都可以通过模仿编译器来处理，或者通过从汇编或机器代码开始翻译2。然而，这样的解决方案将是纯理论的，因为状态爆炸问题将使得除了最琐碎的程序之外，不可能对所有程序进行模型检查。在下一节中，我们将描述c2edl使用的解决方案5C2edlc2edl所使用的建模软件的语义问题的解决方案是一个很容易自动化的根本抽象C2edl消除了除了程序计数器和nite堆栈之外的所有变量，并将对变量的引用if（a > max）变为iff0; 1g）。其结果是一个骨架程序，它代表了原始程序所有可能的控制流的过度近似。例如，考虑图3所示的程序doit（），它调用图1的函数getmax（）。它的抽象如图4所示。由于消除了所有变量，复杂的数据类型和指针不需要特殊处理。不需要在堆栈上保存局部变量的值（因为没有）。因此，为了支持函数调用，包括递归调用，保存程序计数器就足够了。堆栈被限制在一个nite（和小）的深度，通过使用2递归在理论上仍然是有问题的，因为它是潜在的。如果我们假设我们的软件运行在某台真正的机器上，并且有一个nite堆栈，我们可以忽略这个问题。艾斯纳6next（ pc）=如果pc=0则1否则，如果pc=1，则2else如果pc=2那么如果f0，1g那么3 else 4否则，如果pc=3，则4否则，如果pc=4，则5else如果pc=5那么如果f0，1g那么1 else 6else if pc=6 then stack（stackp-1）else if pc=7 then 7否则，如果pc=8，则0如果pc=9，则9next（stackp）=如果pc=8则stackp incelse if pc=6 then stackp decnext（ stack（ stackp））=如果pc=8则9else stack（stackp）stackp inc= if stackp = max stackp then stackp else stackp+1stackpdec= if stackp = 0 then stackp else stackp-1不胀钢栈p=最大栈p见图4。 程序doit（）抽象next（stackp）= if somecall then stackp incelse if somereturn then stackp decelstackpnext（ stack（ stackp））= if somecall then nextpcnocallelse stack（stackp）图五.堆栈的标准化行为一个不变量实现本身非常简单。 在解析源代码之后，通过遍历解析树来分配程序计数器。然后，生成程序计数器的行为就是第二次遍历编号的解析树 在这个遍历过程中，需要收集生成命题somecall（表示函数调用）、somestreturn（表示函数或返回语句的结束）和nextpcnocall（表示函数调用要推送到堆栈上的返回点）所需的信息。这些用于标准化堆栈的行为，如图5所示除了命题 somecall、 somestreturn和nextpcnocall之外，c2edl还自动为程序中的每个变量v和函数f生成形式为assign v（表示对变量v的赋值）、use v（表示对变量v的使用）和callf（表示对函数f的调用）的命题。这可以在不添加额外变量的情况下完成，因为这些命题中的每一个都可以纯粹地表示为程序计数器的函数。c2edl对程序doit（）的完整输出见附录A。乍一看，似乎所描述的抽象使模型失去了所有意义。实际上，getmax（）的有趣属性无法使用图4所示的抽象模型进行验证。然而，有些程序的抽象保留了足够有用的信息。SMV的垃圾收集机制就是这样一个例子。模型检查的过程将在下一节中讨论艾斯纳76模型检查SMV使用c2edl构建的模型，检查了SMV版本r2.4.4和RuleBase的垃圾收集机制的使用情况，RuleBase使用相同的机制。C2edl是在使用位向量而不是整数的模式下调用的（参见附录A），堆栈深度限制为5。6.1SMV的垃圾收集机制模型检测器SMV使用二元决策图（BDD）作为其基本数据结构。由于内存使用是一个问题，因此有必要定期丢弃不再需要的BDD。这就是垃圾收集机制的工作。它的工作原理如下。通过显式调用函数mygarbage（），在代码的各个位置执行垃圾收集。在垃圾收集期间，每个未标记为保存的BDD都将被收集并丢弃。一个BDD是通过调用函数save bdd（）保存的，它将保存的BDD放在一个名为save bdd list的链表中，并返回它的参数。例如，BDDv在调用save bdd（v）之后以及调用v=save bdd（u）之后是安全的，其中u是其他BDD。通过调用release bdd（）将BDD从列表中删除。例如，通过调用release bdd（v）释放BDDv。在保存bdd列表中可能多次出现同一个BDD。函数save bdd（）总是添加一个实例，而release bdd（）总是删除一个实例。如果将来计算所需的BDD被收集为垃圾，则结果是悬空引用，即，一个可能包含垃圾的BDD。 如果将来的计算不需要的BDD永远不会被释放，那么结果就是内存泄漏，内存需求不必要的膨胀对于BDDv来说，悬空引用的问题可以这样表述：如果一个值在没有调 用 save bdd （ ） 的 情 况 下 被 赋 值 给 v ， 并 且 如 果 在 下 一 次 调 用mygarbage（）之前调用save bdd（）没有保存它，并且如果它被另一个计算使用，这是一个错误。由于我们有以下原子命题（如第5节所述自动生成）：assign v：对v的赋值call save bdd v：调用save bdd（）并将v作为参数，或者调用save bdd（）并将结果赋给v调用mygarbage：调用mygarbage（）使用V：使用V我们可以将Sugar中没有悬挂引用的要求表达为：[];assignv^：callsavebddv;：（assignv_callsavebddv）[];(3)call mygarbage;：assignv[ ]; usevg（false）BDDv的内存泄漏问题可以表述如下：如果调用save bdd（）保存BDDv艾斯纳8v而不调用release bdd（），这是一个错误。 借助于上述原子命题和下面的附加命题：call release bdd v：一个以v为参数的release bdd（）调用，我们可以用Sugar表示如下：(4)ftrue[];callsavebddv;：callreleasebddv[];assignvg（false）6.2实验结果使用C2edl和公式3和公式4对SMV的垃圾收集机制进行模型检查。针对SMV 版本r2.4.4 检查le symbols. c的函数构建symbols （）对也出现在symbols.c中的函数的任何函数调用都被翻译，其他函数调用被忽略。生成的模型由3953行代码组成（也就是说，程序计数器的值在symbols. c中有178个BDD类型的变量。对于每一个，生成公式3和公式4，总共356个公式。在RuleBase中，公式可以分组为规则。每项规则在16组（每组22-24个公式）中检查公式。表1显示了规则构建符号0到构建符号15的结果。所有显示的失败都是假阴性，如下一节所述。也检查了规则库本身。特别是，检查了当时正在调试的一个名为reduc- tion（）的函数。生成的模型由2630行代码组成（也就是说，程序计数器的值 在检查的352个公式中，有47个不合格。其中，39如下一节所述，有8个是假阴性，8个是真正的问题使用垃圾收集机制。c2edl的使用允许在新版本的常规回归测试开始之前，使用RuleBase静态地发现这些问题。虽然使用垃圾收集机制的问题通常很难调试，但使用c2edl和RuleBase可以很容易地找到并解决这些问题。生成的反例不是意外的结果或神秘的分段违规（这是测试出错的指示），而是精确地指向显示问题的源代码行（由程序计数器指示）。6.3假阳性和假阴性公式3和公式4的效用高度依赖于程序员使用的编码风格。例如，图6的代码片段是安全的，...b = save bdd（a）; c = b;mygarbage（）;d = c;...图六、c的值不会因为调用mygarbage（）而损坏。 然而应当艾斯纳9表1SMV版本2.4.4的结果规则名称构建符号0vars91运行时19250年代存储器141 MB#规则中的公式22#失败公式0构建 符号19168580S303MB222构建 符号29128482S193MB221构建 符号39182946S321MB222构建 符号4919048S123MB220构建 符号59113692S154MB221构建 符号69115432S149MB222构建 符号79127076S203MB223构建 符号914 S249MB223艾斯纳1082793构建 符号99133952S216MB223构建 符号109111186S130MB222构建 符号119118019S168MB223构建 符号129143809S247MB223构建 符号1391123990S424MB225构建 符号149199560S366MB247构建 符号159142704S276MB244因为公式3不“知道”变量c被赋了一个先前保存为b的值。另一个问题由公式4说明。它将错误地aga-违规的局部变量的使用实际上是安全的。例如，考虑图7中的函数f（）和调用它的代码片段。的呼声bdd ptr f（bdd ptr p，q）f艾斯纳110bdd（g，q）;1return（p）;2 G...10a = f（b，c）11mysql（）;12释放bdd（a）;13 d = g（a）;...图7.第一次会议。艾斯纳12第12行上的release bdd（）释放第0行上保存在函数f（）内部的值。然而，公式4将第二次调用函数f（）作为违规，因为它没有“看到”在两次单独调用函数对变量p的赋值之间为信号p释放bdd（）的调用（第12行上的调用释放信号a）这些和其他假阴性可以通过遵守某些编码约定来避免。我们现在转向误报的问题。 首先，公式3和公式4可能不能完全表达SMV垃圾收集机制的正确使用。第二个问题更为严重。由于我们已经限制了堆栈的深度，我们将不会发现仅在更深层次的嵌套调用中发生的错误这是我们所描述的软件模型的一个基本问题。误报问题意味着我们的方法不能用于软件的验证。然而，假阳性并不是在软件伪造中使用该技术的障碍。 因此，应该从证伪的实际角度来看待这项工作7结论和今后的工作我们已经描述了一个经验，在应用符号模型检查通用软件，垃圾收集机制的模型检查器本身。在这个过程中，在一个正在开发的模型检查器版本中发现了八个真正的bug。 虽然该方法不适用于验证，因为假阳性的可能性，但实验结果表明，它在伪造过程中非常有用未来的工作包括将该方法或其变体应用于其他应用程序。此外，用诸如[20]中描述的那些技术的夜间状态技术进行实验将是有趣的，其不需要限制堆叠的深度。确认我最初的SMV垃圾收集机制模型比本文描述的要复杂得多。感谢IlanBeer，他指出该机制及其正确使用可以单独表示为程序计数器的函数。感谢Shoham Ben- David，Avigail Orni和Yaron Wolfsthal的时间审查和有用的意见。引用[1] Y. Abarbanel-Vinov，N.艾曾布德-雷谢夫岛比尔角Escherner，D.盖斯特，T. 海曼岛Zagaveni，E.里佩尔岛Shitsevalov，Y.Wolfsthal，和T.亚茨卡-哈哈姆。论功能形式验证的有效部署。系统设计中的形式化方法，19（1），2001年。出现。艾斯纳13[2] T. Ball和S. K.拉贾马尼Bebop：一个布尔程序的符号模型检查器。第七届国际自旋通讯研讨会论文集，LNCS 1885. Springer-Verlag，2000.[3] J. Baumgartner，T. Heyman，V. Singhal，and A.阿齐兹IBM Gigahertz处理器的模型检查：高性能网表的抽象算法。 在Proc.11thInternational Conferenceon Computer Aided Veri cation（CAV），LNCS 1633，第72页中。Springer-Verlag，1999.[4] I.啤酒，S。本-戴维角Escherner，D. Fisman，A. Gringauze和Y.罗德时间逻辑糖。第13届计算机辅助验证国际会议论文集. Springer-Verlag，2001.出现。[5] I. 啤酒，S。本-戴维角Escherner，D.盖斯特湖Gluhovsky，T.海曼，A. Landver，P. Paanah，Y.罗德湾Ronin和Y.沃尔夫斯塔尔规则库：IBM的 模 型 检 查 。第 九 届 计 算 机 辅 助 验 证 国 际 会 议 论 文 集 ，LNCS1254.Springer-Verlag，1997.[6] I.啤酒，S。本-戴维角Reynner和A.兰德弗RuleBase：一个面向工业的形式化验证工具.在Proc.33rdDesign Automation Conference（DAC），第655页{660.计算机协会，1996年 6月[7] I.啤酒，S。本-戴维角Reynner和Y.罗德有效检测ACTL公式中的空值。在Proc.9thInternational Conference on Computer Aided Veri cation（CAV），LNCS 1254，pages 279{290.Springer-Verlag，1997.[8] I.啤酒，S。本-戴维角Reynner和Y.罗德 真空的有效检测时态模型检查 系统设计中的形式化方法，18（2），2001年。[9] I.啤酒，S。Ben-David和A. 兰德弗RCTL公式的在y模型检验。在Proc.10thInternational Conference on Computer Aided Veri cation（CAV），LNCS 1427，pages 184{194.Springer-Verlag，1998.[10] C.贝尔纳代斯基，A.凡特奇，S.格内西，S.拉罗萨，G.Mongardi，以及D.罗马诺铁路信号系统设计的形式化验证环境。 系统设计中的形式化方法，12（2），1998年3月[11] A. 博尔alv和G. Stalmar ck.轨道交通的规范化。 InM. Hinchey和J. Bowen，编辑，工业强度形式方法在实践中，第329页{350。Springer-Verlag，1999.[12] W. 昌河J. Anderson，P.Beame，S.Burns，F.莫杜尼奥湾诺特金，J. D.里斯大型软件规范的模型检验。IEEE软件工程学报，24（7）：498{520，1998年7月[13] E. Clarke，O. Grumberg和D.佩尔德。 模型检查。MIT Press，1999.艾斯纳14[14] J. C. Corbett ， M. B. Dwyer ， J. Hatterney ， S. 劳 巴 赫 角 S. Pasareanu ，Robby，and H.郑Bandera：从Java源代码中提取nite-state模型。第22届国际软件工程会议论文集，2000年6月.艾斯纳15[15] C.德马丁尼河Iosif和R.西斯托使用SPIN对Java多线程应用程序进行建模和验证。1998年第四届国际SPIN研讨会论文集.[16] A.他的儿子。1M门ASIC的正式设计。在第二届计算机辅助设计形式方法国际会议（FMCAD），LNCS 1522，第49页。Springer-Verlag，1998.[17] C.我是特纳采用符号CTL模型检验对Hoorn-Kersenboogerd和Heerhugowaard两 个 火 车 站 进 行 了 验 证 。 International Journal on Software Tools forTechnology Transfer（STTT）出现。[18] C.我是特纳利用符号模型检验对Hoorn-Kersenboogerd和Heerhugowaard两个火车站进行了验证。第10届IFIP工作组会议记录10.5正确硬件设计和验证方法高级研究工作会议（CHARME），LNCS1703，Bad Herrenalb，德国，1999年9月。史普林格出版社[19] C.阿利纳河Hoover，W.民族，K。纳尔逊岛Shitsevalov和K.瓦尔克应用于高速缓存一致性协议的硬件控制形式化设计方法。在Proc.37thDesignAutomation Conference（DAC），第724页{729.计算机协会，2000年6月。[20] J. Esparza，D. Hansel，P. Rossmanith，and S.施温 有效算法用于模型检查 下 推 系 统 。 在 Proc.12thInternational Conference on Computer Aided Verication（CAV），LNCS 1855，pages 232{247. Springer-Verlag，2000.[21] D.盖斯特和我 啤酒自动化的高效模型检查订购转换关系分区。在Proc.6thInternational Conference on Computer Aided Veri cation （ CAV ） ，LNCS 818，第299页中。Springer-Verlag，1994.[22] P. Godefroid 。 使 用 VeriSoft 对 编 程 语 言 进 行 模 型 检 查 。第 24 届 ACMSIGPLAN-SIGACT Symposium on Principles of Programming Languages.计算机协会，1997年1月[23] P. Godefroid。VeriSoft：一个自动分析并发反应式软件的工具在proc第九届计算机辅助验证国际会议，LNCS1254.Springer-Verlag，1997.[24] A. Goel和W.李你IBM CoreConnect处理器局部总线仲裁器核的形式化验证。在Proc.37thDesign Automation Conference（DAC），第196{200}页中。 计算机协会，2000年6月。[25] J. Groote、J. Koorn和S. 范·弗利曼。 Hoorn-Kersenboogerd站的安全保障系统。Logic Group预印本系列121，乌得勒支大学，1994年。[26] K. Havelund 和 T. 汉 堡 包 使 用 Java Path 对 Java 程 序 进 行 模 型 检 查 。International Journal on Software Tools for Technology Transfer（STTT），2（4），2000.艾斯纳16[27] G. J. Holzmann。用SPIN对ANSI-C代码进行逻辑验证。第七届国际自旋研讨会论文集，LNCS1885，第224页.Springer-Verlag，2000.[28] G. J. Holzmann和M. H. 史密斯 软件模型检查：从源代码中提取验证模型。在PSTV/FORTE 99号文件第481页中，497. Kluwer，1999年。[29] Y. Kesten，A. Klein，A. Pnueli，G.拉南通过正式验证弥合电子商务差距。In M. Hinchey和J. Bowen，编辑，工业强度形式方法在实践中，第117页{137。Springer-Verlag，1999.[30] G.勒杜克岛博纳旺蒂尔湖Leonard，E. Koerner和C. Pecheur。基于模型的服务条件访问安全协议验证。系统设计中的形式化方法，14（2），1999年3月[31] Z. Manna和A.普努埃利反应系统的时间验证：安全性。Springer-Verlag，New York，1995.[32] K.麦克米兰 符号模型检查。 Kluwer Academic Publishers，1993.[33] J. Mertens海尔胡戈瓦德火车站安全保障系统的研究 博士论文，乌得勒支大学，1996年。[34] A.帕拉斯MPEG解码器芯片的形式验证：形式方法工业应用在验证进展研讨会（WAVE）会议记录中，（CAV-2000后研讨会），芝加哥，2000年7[35] M. Shepherd和G.圣阿尔马克。圣阿尔马克命题逻辑证明程序教程。在第二届计算机辅助设计形式方法国际会议（FMCAD），LNCS 1522，第82页。Springer-Verlag，1998.[36] S. D.斯托勒模型检查多线程分布式Java程序。在proc 第七届国际SPIN研讨会，LNCS 1885，第224页Springer-Verlag，2000年。[37] W. Visser，K. Havelund，G. Brat和S.公园模型检查程序。第15届自动化软件工程国际会议论文集，法国格勒诺布尔，2000年 9月[38] K. Yorav，S. Katz和R. Kiper用模型检查重现同步错误。在第11届IFIP WG10.5高级研究工作会议上正确的硬件设计和验证方法（CHARME），LNCS。Springer-Verlag，2001.出现。一图3的程序doit（）的c2edl输出下面是c2edl对图3的程序doit（）的完整输出。C2edl输出两个le，*.cout和 *. edl。*.cout le是用c2edl分配的程序计数器注释的原始C代码。*.edlle是C代码的RuleBase模型，在语言EDL中，RuleBase的输入语言艾斯纳17图A.1显示了le doit.cout。注意，由c2edl分配的程序计数器使图1、3和4中使用的编号不同。图A.2显示了le doit.edl，这是c2edl从程序doit（）构建的模型。图A.2所示的模型使用整数作为程序计数器和堆栈; c2 edl有一个开关，允许使用位向量来建模。堆栈的深度由参数控制。在这里显示的示例中，深度设置为5。getmax（）f/*0*/a= /*0*/ max =0;/*1*/dof/* 2 */if（a> max）/*4*/max =a;/* 5 *//* push call */;/* 6 */int maximum（）;/*7*/g while（a）;/* 8 */return max;/*/ return; g杜伊特/* 10 */ /* push call */;/* 11 */ max = getmax（）;/* 12 */ return ;g图A.1. 文件doit.cout艾斯纳18var pc：0..十三个;assign init（pc）：= 10;assign next（pc）：=casesome return：返回到哪里;pc=2 ： 如 果 pcaux=0 ， 则 4 else 5endif; pc=7 ： 如 果 pcaux=0 ， 则 2else 8 endif; pc=10：0;pc=13：13;else：if pcplusone> maxpc then maxpc else pcplusone endif;esac;de ne maxpc：= 13;de ne pcplusone：= pc+1;var pcaux：0..二、de ne nextpcnocall：= casepc=2：如果pcaux=0，则4，否则5endif; pc=7：如果pcaux=0，则2，否则8 endif; pc=13：13;else：if pcplusone> maxpc then maxpc else pcplusone endif;esac;var stackp：0..6;%，用于0.. 5%的人这样做变量stack%fiig：0..intfindDuplicate（）：= 0;next（stackp）：= casesome realpushcall：if stackp=6 then 6 else stackp + 1 endif; somereturn：if stackp=0 then 0 else stackp-1 endif;stackp;esac;不胀钢叠层6;var auxnondet：0..十三个;assign next（stack 0）：= casesome（stackp = 1）：auxnondet;（0！= stackp）j！someRealpushcall：stack 0; else：nextpcnocall;esac;assign next（stack 1）：= casesome（stackp = 2）：auxnondet;（1！stackp）j！someRealpushcall：stack1; else：nextpcnocall;esac;assign next（stack 2）：= casesometreturn（stackp = 3）：auxnondet;（2！stackp）j！someRealpushcall：stack2; else：nextpcnocall;esac;assign next（stack 3）：= casesometreturn（stackp = 4）：auxnondet;（3！stackp）j！someRealpushcall：stack3; else：nextpcnocall;esac;assign next（stack 4）：= casesometreturn（stackp = 5）：auxnondet;（4！stackp）j！someRealpushcall：stack4; else：nextpcnocall;esac;assign next（stack 5）：= casesometreturn（stackp = 6）：auxnondet;（5！stackp）j！someRealpushcall：stack5; else：nextpcnocall;esac;de ne stackpminus1：= if stackp = 0 then 0 else stackp - 1 endif;de ne stackpplus1：= if stackp = 6 then 6 el