C程序错误定位方法的模型检查器应用

理论计算机科学电子笔记174（2007）95-111www.elsevier.com/locate/entcsC程序的自动故障定位1Andreas Griesmayer、Stefan Staber和Roderick Bloem格拉茨技术{agriesma，sstaber，rbloem}@ ist.tugraz.at摘要如果一个程序没有满足给定的规范，模型检查器会提供一个反例，一个证明错误行为的运行。 即使有一个反例，在源代码中定位实际的错误对于验证工程师来说也是一项艰巨的任务。我们提出了一个自动的方法，在C程序中的错误定位。该方法基于模型检查，只报告可以更改的组件，以便消除示例的实际行为和预期行为之间的差异。为了识别这些组件，我们使用有界模型检查器CBMC的仪表化版本的程序。 我们提出的实验数据支持 我们的方法的适用性。保留字：故障定位，调试，模型检验，反例1引言调试是软件开发周期中最耗时的部分之一。由于软件系统的复杂性在不断增加，因此对帮助程序员进行调试的工具的需求也在不断增加。故障检测包括三个步骤：检测程序包含故障、定位故障和纠正故障。断层探测一直是一个活跃的研究领域。目前，在故障定位和校正方面的工作较少。在这项工作中，我们专注于本地化，并提出了一种新的方法来确定C程序中的故障原因。我们假设我们有一个用C写的程序和一个规范。假设程序包含一个错误，我们有一个反例表明该规范不成立。我们使用反例来创建程序的扩展版本。 我们根据反例的值固定程序的输入，并为每个组件引入异常谓词，1 这项工作得到了欧洲联盟根据第507219号合同（PROSYD）提供的部分支助。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.12.03296A. Griesmayer等人理论计算机科学电子笔记174（2007）95节目如果一个组件的异常谓词为真，我们假设该组件工作异常。因此，我们挂起组件的原始行为，并将其替换为新的输入。因此，定位问题就是找出哪些异常谓词需要断言，以及如何替换相应的组件以满足原始规范。为了发现异常谓词，我们否定了原始规范，说明通过挂起组件不可能满足它，并再次使用模型检查器来验证新系统。 如果我们发现一个失败的运行，我们可以从中推导出工作异常的组件和一个替代品，这样程序就可以固定为原来的反例。1.1相关工作所提出的工作与基于模型的诊断（MBD）理论密切相关[21，16]，该理论起源于诊断物理系统。Console等人[4]展示了MBD在逻辑程序中故障定位的适用性。在将MBD应用于源代码级的硬件设计方面已经做了很多工作[9，25，20]。该理论也已成功地应用于调试程序编写的Java的一个子集[19，18]。在MBD中，模型是从源代码中派生出来的。该模型与给定的故障跟踪一起描述了程序的实际故障行为跟踪的正确输出必须由oracle提供（通常由验证工程师提供）。基于模型的诊断产生一组组件，解释模型和期望行为之间的差异，但不提供这些组件的替代品。在我们的方法中，我们不需要特定的故障跟踪和为该跟踪提供正确输出值的oracle。相反，我们假设给定了一个规范，并使用一个验证工具来获得一个任意的有限故障迹线，以证明该规范被违反。此外，我们还使用该规范来自动导出该跟踪的正确行为。Veneris、Smith等人开发了基于模型的诊断的相关理论。例如，参见[7]。他们使用SAT求解器来诊断时序电路，但不考虑规范：用户必须为给定的反例提供电路的正确行为。诊断的一个应用是设计校正。Huang和Cheng [13]开发了一种理论，以确定电路可以修改以满足新规范的位置。在他们的情况下，规格是作为另一个电路。在[15，23]中，提出了一种用于调试的基于游戏的方法。使用LTL规范，该方法能够定位故障并提供对所有可能的输入值有效的校正。最近，这项工作被扩展到下推系统来处理递归布尔程序。[10]中给出了该方法及其在C程序抽象中的应用的详细信息。找到对所有输入都有效的校正的问题在计算上是困难的，因此该方法不如本文中提出的方法有效，在本文中，我们仅为所考虑的反例提供校正。其他现有的工作使用故障定位的轨迹之间的差异A. Griesmayer等人理论计算机科学电子笔记174（2007）9597Renieris和Reiss [22]假设存在一个错误的跟踪和一些成功的跟踪。两条线索的不同指向了程序中可疑的部分实验数据表明，故障定位的质量强烈依赖于给定的一组轨迹。 在Groce [11]的工作中，一个规范被用来生成一个成功的迹，它尽可能接近一个反例。失败痕迹与成功痕迹的差异是解释故障的依据。实验数据表明，他们的方法相当不错的结果，虽然对于一些例子，手动假设必须添加，以获得有见地的解释。与我们工作的比较可以在第4节中找到。在[26]中，Zeller的delta调试方法用于获得故障的原因-后果链。在失败的和成功的程序运行中，在经验选择的兴趣点中的状态之间的差异提供了对故障的解释。Ball等人[1]使用多次调用模型检查器，并将获得的反例与成功的跟踪进行比较。未出现在正确轨迹中的转换被报告为故障的可能原因所有使用跟踪之间的差异的方法都需要由用户生成或给出的成功运行。报告的语句是失败运行中出现的代码片段，而不是成功运行中出现的代码片段。不能保证报告的是真正的故障位置，也不能保证代码的碎片是最小的。不同的失败运行可能导致不同的故障候选，共同的候选人。与这些方法相反，我们不比较不同输入的运行，而是从一个反例开始，寻找最小的变化在程序中，以生成具有相同输入的成功运行。因此，每个报告的位置都是潜在的故障候选者，并且可以用于修复所使用的反例的故障。 可以肯定的是，真正的错误在于 找到的候选者的集合（假设故障在所考虑的故障模型中C.F. 2.1）。因此，我们在多个反例上对该过程进行验证，并使用结果的交集来缩小故障候选者的数量其他现有的工作没有报告可能的故障位置，而是给出了对失败的本质有更深的理解。在[14]中，确定了导致错误发生的实例部分。Zeller和Hildebrandt [27]指出了导致程序输入失败和成功输入之间的显著差异。Groce和Visser [12]生成并分析程序运行的类似版本（成功运行和错误运行），以获得有关失败原因的更多信息在下一节中，我们将详细介绍我们在一般情况下的方法。第3节给出了C程序中故障定位的实例以及所使用的工具和方法的细节。 我们在第4节中通过检查两个示例并解释收集的结果来展示该方法的适用性。第五节对未来的工作进行了总结和展望。98A. Griesmayer等人理论计算机科学电子笔记174（2007）95NDS2基于模型检测的故障定位在这一节中，我们将概括地描述如何使用模型检查器进行故障定位。在这一节中，效率不是我们主要关心的问题。在第3节中，我们给出了C程序中定位错误的方法的具体实例2.1预赛我们有一个系统S，它由一组分量C ={c0，. ，cn−1}以及一组信号V=VS<$VND。 信号vi∈VS由分量定义ci作为函数fi（V），V_ND中的信号被非确定性地选择，并且描述系统的输入或非确定性行为。(In下面，我们把系统中的输入和非确定性都称为“输入”。元件和信号的确切定义取决于应用领域。例如，对于硬件，可以将组件定义为门，将信号定义为线。（参见[15、23]。我们假设系统是连续的，并且在离散时间内运行。也就是说，系统的运行是信号估值的可数序列，包括输入和不确定性选择。除了系统之外，我们还给出了一个规格，这是一个安全属性。如果系统没有满足规范，模型检测器会给我们一个反例π：一个对VCVND中的信号赋值的有限序列，使得系统违反规范。我们认为，违反规范是由规范所规范的行为与S所规定的行为之间的矛盾。系统的组件可以根据故障模型进行更改，故障模型描述了允许的行为更改。例如，电路的一种可能的故障模型：用NAND或NOR门代替门。我们称一个可以改变的组件，以避免错误（而系统的其余部分保持不变），一个单一的故障诊断。所有这些组件的集合我们很自然地将这种符号扩展到二元或多重故障的组件元组。2.2方法我们的方法包括以下步骤。(i) 我们选择一个参数m，它定义了为了生成一个遵守规范的系统，可以改变多少个组件例如，在一个示例中，如果m= 1，我们寻找单一故障。(ii) 我们构造了一个新的系统SJ.系统SJ由S通过两个修改得到。首先，我们通过添加组件来构建VJ =VND\VC和VJ=VSVC把反例给出的值赋给VC。 注意，该方法如何做到这一点取决于系统和所使用的模型检查器。 虽然对于硬件，我们通常有所有不确定信号和时间步长的值，但软件的模型检查器只给出通过程序的单个跟踪的值，并且不给出未到达的语句的信息。A. Griesmayer等人理论计算机科学电子笔记174（2007）9599ND我第二，我们将新信号ab0，.，abn−1，布尔域，对于每个vi∈VS，信号ndi具有与vi相同的域。 我们进一步替换fiibyfj的functionfI=<$abifiabifidi。因此，如果abi=true，则我们认为组件ci被错误地选择，并挂起成分如果abi=false，则组件按系统规定工作。j(iii) 我们构造了一个新的规格，即，（iabi≤ m）。否定的规范-定义J指出，当最大值的m个组件被暂停，即不可能改变最大m个组件，以便填充。（我们用数字1来表示真(iv) 我们要求模型检查器生成一个反例πJ，表明SJ并不满足条件。假设存在一个关于πJ和Sj的反例πJ反例的相关部分是abi和ndi的赋值。 组件的集合{ci|abi= true}称为诊断。反例的存在表明，当诊断中的一个分量被暂停时，S并不矛盾如果我们将诊断中的ci替换为行为类似于ndi的组件，所得到的系统在πJ规定的输入下满足条件。注意，来自πJ的输入与来自π的输入（如果存在）一致。因此，我们的主张是，通过我们的方法发现的诊断只包含可用于修复系统的组件对于给定的反例。 很明显，我们不能保证 无论输入如何，都要修复系统。找到一个对所有反例都有效的诊断要困难得多[15，23]。如果不存在反例πJ，则系统不能通过仅替换m组件。通常情况下，我们从m= 1开始，每当诊断失败时增加m。为了获得所有组件，我们可以多次运行模型检查器，每次排除已经找到的诊断元素这通常是浪费的，因为它迫使许多重新计算，而这些重新计算通常可以通过对模型检查器的小修改来避免。2.3讨论这里提出的理论是相当普遍的。它不限于有限域，只要第ii点中提到的修改可以表达。同样地，一个信号只能由一个分量定义的限制也是不必要的。如果它被删除，一般的约束系统可以诊断[8]。要求系统是一个顺序的、离散时间的系统是相当宽松的：实时程序满足这个要求，因为时间步可以被看作是单个语句的执行。密集时间（模拟）系统不适合我们的方法。一些可能的应用领域是时序电路，如[2]中所使用的布尔程序（参见[1]）。[17]）和C程序，这是本文的主题100A. Griesmayer等人理论计算机科学电子笔记174（2007）95清单1：循环展开return 0;如果（！printf（“%d”，index）; index++;如果（！（index 5））gotoend;6printf（如果（！printf（“%d”，index）; index++;11if（！（index 5））gotoend; assert（false）;结束语：3C程序为了将该方法应用于C程序，首先简要介绍了所使用的模型检查器CBMC和软件有界模型检查。第3.2小节介绍了我们在C程序中查找错误的方法，这是上一节中描述的一般方法的变体。3.1民银为了实现C的故障定位，我们使用软件模型检查器CBMC [3]。CBMC将ANSI-C源代码作为输入，并处理指针、数组和C数据类型，而不需要抽象。使用assert语句进行指定。CBMC非常精确地遵循C语义。例如，未初始化的变量在模型中引入了非确定性，C标准中的构造也是如此。给定一个C程序P和一个约束k，CBMC构造了一个程序的解绕Pk如果循环需要少于k次迭代，则通过创建循环的k个副本以及适当的if语句来展开循环向后goto语句和递归调用的处理方式类似。清单1给出了将以下循环展开到深度3的结果for（index = 0; index 5;index++）printf（第12行中的断言是一个展开断言，它是由CBMC添加的，以决定展开是否足够深。如果它被违反，我们发现一个运行遍历循环超过三次。我们必须再次致电CBMC，并给出更高的平仓上限在展开程序中，CBMC支持assume语句和assert语句。CBMC将展开的程序转换为命题逻辑公式，当且仅当程序的执行结束时，命题逻辑公式才是满意的在违反断言语句和满足所有假设它遇到的语句。通过标准SAT求解器检查满足性。A. Griesmayer等人理论计算机科学电子笔记174（2007）95101KKKKKK3.2故障定位假设我们给出一个反例，表明一个断言被违反了。反例包括输入值和非确定性结构。这样的反例可以从CBMC获得。和前面一样，我们将以同样的方式处理非确定性构造和输入值。我们认为，由反例选择的值为i0，.，il−1.我们选择的组件是程序中的表达式集，即，赋值语句的右侧，if、while和case语句中的条件，等等。假设我们有n个这样的分量：e0到en-1。显然，我们模型的信号选择是变量。构建插装程序的过程包括展开到深度k 我们现在构造PJ根据第2.2节定义的规则，如下所示：一次可以更改的组件数量决定了如何检测代码。在下文中，我们给出了单一故障的方法。扩展到多个故障是直接的，并在第3.4节中进行了描述。我们通过在P j的开头声明一个新变量diag将P改为P J，其值在{0，.，n-1}。我们进一步用表达式（diag == i？n o n d e t （）：ei）其中nondet（）返回一个不确定的值。diag的值决定了哪个表达式被挂起，而同时所有其他表达式的行为与原始程序P中的一样。CBMC将插装程序展开，得到PJ。最后，我们使用反例π中的赋值来设置PJ中的相应变量我们通过确保我们准确地报告那些不违反PJ中的任何断言的运行来否定指定。因为一个展开的程序不包含任何循环，我们可以通过在PJ的末尾添加一个语句assert（false），并将Pk中的每个assert语句assert（c）替换为PJ中的assume语句assume（c）来做到这一点。新的反例再次使用CBMC计算。如果找不到新的反例，我们可以寻找对偶故障或增加展开次数。在上一步中保持展开断言不变有助于调整正确的展开次数。诊断中的表达式正是那些可以改变以满足反例的注意，我们并没有固定Pk中反例没有访问的非确定性结构的选择-通过改变分支语句的条件，我们仍然可以找到包含非确定性的路径。因此，我们报告所有的表达式，其中有一个成功的执行PK的一些选择的非确定性组件尊重的选择在反例。（更精确的方法是检查执行是否成功，而不管其余不确定组件的行为如何，但这会引入混合量化器。102A. Griesmayer等人理论计算机科学电子笔记174（2007）95KK清单2：一个简单的C程序P=Pkvoidmain（）{inta，b，c，d;3if（a）{/n不确定性选择<$/a = 5;b = 6;c = a+ b; d=a b;if（a % 2 == 0）{inte;a = e;/n不确定性分配n/}return（c == 12 d == 36）;13}}很难计算）。对给定反例的完整诊断是迭代构建的：当找到表达式时，我们在程序代码中添加一个假设语句，以避免第二次报告相同的组件。CBMC会重复运行，直到没有更多的表达式被发现。一个更有效的方法是在SAT实例中添加阻塞子句。3.3例如下面我们用一个简单的C程序来说明我们的方法。清单2显示了一个程序P，它将变量a和b相加和相乘。作为具体说明，我们在第12行使用了一个assert语句。在第4行中，a被赋值为5，这是不正确的，应该是6。注意，代码中没有循环，因此Pk=P。假设反例将a、b、c、d分别设置为值1、vb、vc和vd。（值vb、vc和vd是不相关的，a可以设置为任何非零值。清单3显示了PJ。在第3行中，引入了新的变量diag反例在第6行中是固定的，但在第14行中e的值没有固定。语句assert（false）被添加到程序的末尾，每个表达式都被替换为包括对diag变量的适当检查。使用的数字对应于清单2中行号的表达式。在PJ上运行模型检查器为我们提供了一个诊断的反例等于4，而nondet（）返回值6。它还进入if的then块语句，并将一个不确定值赋给e，在下面也赋给a。最后两个赋值并不符合规范，因此是任意的。我们看到，第6行中a的赋值是所有可能反例的正确值。虽然通常我们必须找到一个对所有可能的反例都有效的表达式，但在这个例子中，我们可以直接使用这个信息来修复原始程序：我们将清单2第4行中的值5替换为6。没有其他诊断。3.4双重故障诊断对于两个（或更多）故障的方法的扩展是相当简单的。我们添加了两个变量diag1和diag2，而不是一个;这两个变量都被分配给一个不确定的A. Griesmayer等人理论计算机科学电子笔记174（2007）95103K清单3：修改后的解绕C程序PJ1voidmain（）{inta，b，c，d;intdiag;int n = nondet（）;6a = 1;b = vb; c = vc; d = vd;如果（diag == 3？public void run（）{a =（diag == 4？int n（）;b =（diag == 5？int n（）;11c =（diag == 6？mysql（）;d =（diag == 7？mysql（）如果（diag == 8？nondet（）：（a % 2））}inte;a =（diag == 10）？return（）;16}mysql（c == 12 d == 36）;}return（false）;}独立的价值如果其中一个诊断变量被设置为其编号，则诊断中存在表达式该方法的其余部分类似于上面描述的单个故障为了防止每个表达被检测两次，我们包括了diag1diag2的要求。<此外，我们首先执行单故障诊断并排除所有元组{diag1，diag2}，使得diag1或diag2处于单故障诊断中3.5讨论通过使用表达式作为组件，我们得到了一个细粒度和非常自然的模型，用于故障定位。检查表达式使我们能够定位赋值、函数调用和返回语句以及if语句或循环的条件中的错误。因为我们不仅检查表达式是否导致错误，而且还检查是否可以改变它以避免错误，所以我们的结果比可比方法更精确。清单2中程序的修正版本将6赋值给第7行中的变量a。Groce [11]、Zeller [26]、Ball等人[1]和本示例的动态切片[24]包括从线路4到线路7的所有分配，同时我们能够正确地将故障定位到线路4。为了找到一个诊断，我们必须表达一个表达式的可能替换。虽然对于表达式或赋值语句的左侧来说，这样做相对容易，但结构性错误（例如循环的if语句中遗漏了被遗忘的大括号的语句）很难定位，而更粗糙的方法可能会给出一个粗略的程序区域供验证工程师检查。我们的方法返回所有可以更改的表达式，以便我们可以从给定的反例生成正确的运行。请注意，如果错误值通过程序传播，则不可能分辨出是哪个错误值。如果程序是弱指定的，那么所涉及的表达式的一个重要特征就是改变。再看一下清单2中的示例。如果我们将第12行中的assert更改为assert（d== 36），则无法判断故障是位于第4行还是第7行。104A. Griesmayer等人理论计算机科学电子笔记174（2007）95表1西门子测试套件TCAS任务的结果#TC#诊断时间评分#TC#诊断时间评分v113115（17-19）29530.90616岁15（17-17）5850.906v269第五条（11-18）8360.97522页118 （8- 8）2230.950v323第七章（十三至十九）4230.956v23 419 （9- 9）8850.944v42015（18-19）5760.906v24 715（16-17）2540.906V510第七章（十七至十八）1590.956v25 38 （9- 9）680.950V61213（16-17）2530.91926 11第8条（16-19）3110.950V736第4条（9-18）7430.97527 10第七章（十七至十八）1530.956V8119（19-19）260.886v28 75 第二章（10-19）6420.988v99第9条（10-11）1140.94429岁18第3条（9-18）2240.981V101412（17-19）2690.925v30 57第4条（10-17）9390.975V1114第5条（10-14）1620.969第31页1414（15-16）4490.913V1270第七章（十六至十九）16640.956v32 214（16-16）390.925v134第9条（17-19）149v33 894（8-19）8920.369v14504 （4- 4）594v34 77第七章（十六至十八）19060.956V1510第七章（十七-十七）2830.956v35 75 第二章（10-19）10690.988V167015（17-18）12630.906第36页1232 （2- 3）877v1735第4条（9-18）13000.975v37 93第五章（9-19）8220.969v1829第4条（3-17）4990.975v39 38 （9- 9）660.950V1919第4条（9-17）6910.975v40 1239（10-15）30170.944V201815（18-19）7480.906v41 2015（18-19）9560.906因此，我们看到适当的规范大大改善了该方法的结果。为了产生可靠的诊断，我们考虑程序的所有断言语句。4示例我们通过考虑两个示例来说明该方法的适用性：以下部分显示了西门子测试套件的TCAS任务的结果[6]。西门子套件包含五个在文献中广泛使用的任务。每个任务由一个C程序和几个版本的错误介绍。已知断层的位置和类型。除了源文件之外，还提供了一些测试用例以及哪些代码版本通过了测试用例的信息。在第二个例子中，我们检查一个数据结构的实现部分4.2给出了红黑树的细节，它的属性以及如何通过断言来检查它们。所有程序都自动检查。如果没有另外说明，所有的编译都是由脚本完成的。如果一个程序有多个测试用例，则只对第一个测试用例检查完整的状态空间。在后续测试用例中，检索仅限于根据第3.2节所述的先前测试用例计算的诊断。4.1TCAs西门子测试套件的TCAS任务构成了飞机防撞系统。它由大约250行代码组成。为了A. Griesmayer等人理论计算机科学电子笔记174（2007）95105检查故障检测工具的有效性，该套件的作者创建了41个版本的程序。每一个都是通过添加一个或多个故障手动创建的，通常是单行中的更改。在下文中，我们将通过“v1”到“v41”来指代版本。该套件还包含一组1600个测试用例及其在每个TCAS版本上的结果106A. Griesmayer等人理论计算机科学电子笔记174（2007）95由于没有给出具体说明，我们使用失败的测试用例作为反例，并使用测试用例的正确值作为具体说明。除了没有给出测试用例的v38之外，测试套件为每个程序版本提供了3到130个失败的测试运行，总共1500个。该程序在赋值和条件中包含34个表达式，这些表达式被识别为错误的潜在原因，并如上所述进行检测。表1给出了每个版本TCAS的测试用例数量。第三列显示最终诊断的大小以及诊断大小的变化（如果分别为每个测试用例计算）。第四列中的时间给出了每个TCAS版本的总计算时间。请注意，在大多数情况下，测试用例的子集将导致相同的最终诊断。因此，适当选择要考虑的测试用例将显著减少计算时间。 由于这样的选择需要分析测试用例，并且我们不关注性能，因此考虑了所有可用的测试用例进行计算。最后一列给出了[22]提出的评分函数的结果。它基于程序依赖图（PDG），并给出诊断中报告的元素与错误语句之间的距离，范围为数字越大越好。对于其中三个版本，无法计算此分数，因为故障位于#define语句中，因此不是PDG的一部分。除了V33之外，所有的分数都很好。我们在v33中得到了最低的分数，因为在那个例子中，错误是在初始化四行中的数组元素时出现了错误的索引，而我们的单故障方法没有报告这些索引。尽管排名较低，但结果包含访问数组的唯一语句，因此看起来非常有用。在[11]中，Groce给出了TCAS的5个版本的分数，他的方法适用，并将其与Renieris和Reiss的结果进行比较[22]。Groce比较了几种有和没有delta切片和额外的解释的方法，我们在图1中总结了结果。垂直轴给出了Renieris [22]的评分函数的结果，它与用户在开始查看给定结果时必须查看的代码量成正比如果方法达到100%，则故障定位最准确。请注意，虽然所有方法都为某些示例提供了良好的结果，但只有本文中提出的方法在所有示例中得分最高或第二现在我们将仔细研究v2，它的源代码如清单4所示。省略了对示例和变量初始化不重要的函数。常量以大写字母书写，全局变量表示测试用例的输入值以大写字母开头，局部变量以小写字母开头。由于混淆了两个常数，在第4行的函数抑制偏爬中引入了故障，原始版本显示为上一行的注释。我们用CBMC报告的72个状态的错误跟踪来演示这个错误：它进入了第40行的if语句的主体。第42行中对NCB Climb的调用是不相关的，因为测试用例是这样的，OBT（）返回false，因此赋值A. Griesmayer等人理论计算机科学电子笔记174（2007）95107图1.一、TCAS实例与Groce、Renieris和Reiss的结果比较需要向上的RA是假的。在第43行中，调用NCB Desertification，它随后调用包含错误的函数Inhibit Biases Climb。该错误的结果是，在第23行中，updates被分配为true而不是false，这导致在第25行中错误地分配false，并在第29行中返回。因此，第43行中的向下需要RA被指定为假而不是真。这导致第48行中的条件为假，从而在第51行中设置错误的返回值。对于这个版本的TCAS，我们检查了69个测试用例，每个用例都给我们10到18个元素的诊断。通过我们的方法发现的最终诊断是第4行和第8行、第43行和第53行中的条件和左表达式，以下划线显示。我们检查是否可以删除作为诊断给出的每一行中的反例的错误：• 第53行很明显，如果我们在所有情况下都返回DOWNWARD RA，断言将不再被违反。事实上，一个错误函数的return语句，或者它的call语句，总是可以被一个实现正确行为的函数的调用所替换• 如果我们在第43行将need downward RA设置为true，我们就进入了正确的else分支并返回正确的值（在手头的反例中need upward RA为false• 8号线的维修比较复杂。看一下反例就可以看出，要删除这个错误，函数OBT在第42行调用时必须返回false，在第25行调用时必须返回true。 因为OBT比较两个输入变量， 它应该总是在运行中返回相同的值在这个位置进行修复108A. Griesmayer等人理论计算机科学电子笔记174（2007）95清单4：TCAS v21intInhibit Biased Climb（）2{1}3//返回（爬进？Up Sep + NOZCROSS：Up Sep）;4return（Climb Inh？Up Sep+MINSEP：Up Sep）;5 个文件夹67布尔OBT8{return（Own Tracked AltOther Tracked Alt）;}<910boolNCB Climb（）11{/省略声明/12up =抑制有偏攀升（）>Down Sep;13if（向上）14result =！（OBT（））||（（OBT（）（&&！(Downintn = nums（nums）;其他15个16结果= OAT（）（CV Sep> = MINSEP）17&&（Up Sep> = ALIM（））;18返回结果;19 个文件夹2021boolNCB Desert（）22{/省略声明/23向上=抑制有偏攀升（）>向下九月;24if（向上）25结果= OBT（）（CV Sep> = MINSEP）26&&（Down Sep> = ALIM（））;其他27个28结果- -（OAT（））||（（OAT（））&&（Up Sep>= ALIM（）;29返回结果;30 个文件夹3132intval（）33{/省略声明/34使能=高配置（OTA速率= OLEV）35&&（CV Sep> MAXALTDIFF）;36tcas eq =其他能力== TCAS TA;37意图不明=三份报告中有两份有效38&&其他RAC ==无意图;39alt sep =未解决;40if（enabled&&（（tcas eq&& intent not known））||！tcas eq））41{42个需要向上RA = NCB爬升（）OBT（）;43个需要向下RA=NCB Desperate（）OAT（）;44如果（需要向上RA需要向下RA）45alt sep =未解决;46else if（需要向上RA）47alt sep =右心房向上;48else if（需要向下RA）49alt sep =向下RA;还有50个51alt sep =未解决;52}53return alt;54 个文件夹5556publicintfindDuplicate（ int findDuplicate）57return（）;58/忽略全局变量的初始化/59assert（alt sep test（）==向下RA）;60}似乎不合适。• 诊断的其余元素是第4行中的条件语句的条件和我们在同一行中引入故障的表达式 该状况是诊断的一部分，因为故障是 错误地使用较大的常数MINSET而不是较小的常数NOZCROSS。因此，在导致错误行为的测试用例中，A. Griesmayer等人理论计算机科学电子笔记174（2007）95109表2TCAS任务的双重故障诊断结果。#TC#诊断时间#TC#诊断时间V6124（4-5）118v25310（10-12）82V811（1-1）6v31144 （4- 5）177v995（5-7）129v3225 （5- 6）20V16704（4-5）889V361266 （6- 8）1975V22116（6-8）184V39310（10-12）74v23425（5-6）588V401266（6-15）2722v2471（1-1）44抑制有偏爬升的值太高。通过将条件更改为始终选择第二个表达式（该表达式没有此常量），我们可以避免这种行为。虽然还有一些工作留给验证工程师来决定哪个位置是修复程序的最佳位置，但我们看到该方法给出了良好的结果，这些结果只指向我们有可能删除故障的位置除了诊断之外，该方法还为我们提供了nondet（）的值，选择该值是为了避免每个已识别表达式的错误行为。此信息对于了解如何修复程序很有价值。在上面的例子中，第4行条件语句的条件总是选择第二个较小的表达式返回。为了避免这个错误，我们也可以用一个负值来替换左边的表达式，表示返回的值应该更小。其他版本的TCAS甚至可以更好地替换错误的表达式。例如，在版本7中，错误是通过将常量初始化为501而不是500而引入的。检查该行的建议值，结果正确分配为500，以消除所有测试用例的故障4.1.1双重故障除了单一故障诊断，我们寻找的诊断，正是两个表达式被替换。结果在表2中给出。与表1的结果直接比较表明，计算实例所需的时间与单一故障情况相当。虽然单次运行CMBC所需的时间大约是单次故障诊断的三倍，但总体运行时间保持不变，因为较小的诊断规模迅速导致要检查的表达式集较小（CBMC调用较少）。4.2红黑树红黑树是一种自平衡的数据结构，其插入，删除和搜索的操作在O（nlogn）时间内执行[5]。它是一种自平衡二叉搜索树，其中每个节点都有一个颜色属性。除了对二叉搜索树的要求外，还必须满足以下额外要求。(i) 节点是红色或黑色。(ii) 根是黑色的。(iii) 叶子都是黑色的。110A. Griesmayer等人理论计算机科学电子笔记174（2007）95(iv) 每个RED节点的两个子节点都是BLACK。(v) 从任何给定节点到其叶节点的所有路径都包含相同数量的黑色节点。插入，删除和搜索操作的实现与通常的二叉搜索树。在这样的操作之后，检查树以检查它是否与上面的规则一致。如果不是，则执行恒定时间旋转和重新绘制操作以恢复一致性。这确保了树保持平衡并保证了时间界限。我们从Wikipedia上的Red-Black trees2条目中检查了实现，并以assert语句的形式添加了规范，如下所示：规则（ii）：插入操作后的单个断言。规则（iv）和二叉搜索树顺序：在插入操作之后，调用遍历树的例程。如果找到一个红色节点，它会检查两个子节点是否都是黑色的。同一例程还执行值的比较，以确保二叉搜索树的正确顺序。指针访问：有些函数隐式地假设它们是用有效指针调用的。添加断言是为了确保指针在其字段被访问时不为NULL，即使代码中存在错误我们规则（iii）总是为真，因为NULL指针被视为BLACKleaf。在这个例子中，规则（v请注意，所有assert语句都同时出现在源代码中，只允许满足所有这些语句的诊断。 通过检查一些测试用例对示例进行了测试，其中节点按以下顺序插入空树中（描述给出了对全功能数据结构的假设操作）：0，5这个简单的例子用一个值为0的节点重新命名树，并添加一个值为5的新节点作为它的右子节点。不需要重新绘制或旋转节点。5，1类似于第一个测试用例，但第二个节点作为根节点的左子节点插入。5，1，2最后一个操作创建了一个不平衡树。要恢复红-黑树的属性，需要进行两次旋转和重新分配颜色。5，9，4，6最后一次插入创建了一个平衡树，但是一个RED节点有一个RED子节点，这与规则iv相矛盾。若要恢复属性，需要在两个过程中重新指定颜色实现红黑树的源代码由大约250行代码组成。因为数据结构使用指针来连接节点，所以即使是这个小例子也很难诊断。允许CBMC2 http://en.wikipedia.org/wiki/Red-black树A. Griesmayer等人理论计算机科学电子笔记174（2007）95111插入任意值以分配给数据结构的指针可能导致树的完全重新排序，从而导致要探索的大的状态空间。因此，在这个例子中，执行诊断比检查具有少量不确定性或根本没有不我们在源代码中引入了两个错误：(i) 为了满足规则（ii），插入到树中的第一个节点是黑色的。这个任务被改成了红色。(ii) 每个节点首先被插入到树中，就像通常的二叉搜索树一样因此，遍历树以找到新节点的正确位置。在遍历例程中，比较从=改为==，导致树的顺序错误。第一个故障导致只有一个元件为每个测试用例提供正确的故障线。第二个故障不会导致第一个测试用例的树不正确。然而，第二个和第三个测试用例导致了包含正确行的三个表达式的诊断。第四个测试用例的状态空间超过了完整诊断的内存限制，但可以逐个检查先前测试用例的表达式是否也在第四个测试用例的诊断中。通过这种方式，我们能够排除一种表达，并最终诊断出两种元素。5结论和今后的工作我们提出了一种新的方法来定位C程序中的错误，通过构建一个修改的系统，允许任意改变给定数量的表达式新系统包含了原始程序的反向规范。如果我们能找到新系统的错误痕迹，我们就找到了修复原始程序的表达式。我们已经证明了两个例子的方法的适用性。该方法的运行时间仍然可以改进。很大一部分时间花在解析、展开和生成程序的内部表示上。在计算单个程序的诊断期间，该表示不会改变。通过使用阻塞子句和重新运行SAT求解器来找到完整的诊断