组件行为规范的模型检查：真实经验中的调试技术

理论计算机科学电子笔记160（2006）197-210www.elsevier.com/locate/entcs组件行为规范的模型检查：一个真实的生活经验Pavel Jezek帕维尔·耶泽克1，4布拉格查尔斯大学软件工程系捷克共和国Jan Kofron扬·科夫龙2，4布拉格查尔斯大学软件工程捷克共和国Frantisek Plasil3，4布拉格查尔斯大学软件工程系捷克共和国摘要本文是基于一个真实的经验与行为规范的非平凡的基于组件的应用程序。经验是，这样一个规范的模型检查会产生非常长的错误轨迹（提供反例），数量级为数百个状态。分析和解释这样的错误跟踪以定位和调试实际规范是一项繁琐的工作。我们提出了两种旨在解决这个问题的技术：状态空间可视化和协议注释，并分享了应用它们的积极经验，使调试过程更有效。保留字： 组件行为、验证、模型检查。1电子邮件地址：jezek@nenya.ms.mff.cuni.cz2 电邮地址：网址：kofron@nenya.ms.mff.cuni.cz，kofron@cs.cas.cz3 电邮地址：网址：plasil@nenya.ms.mff.cuni.cz，plasil@cs.cas.cz4这项工作得到捷克科学院项目1 ET 400300504、捷克共和国赠款机构项目GACR 102/03/0672和法国电信的部分支助，外部研究合同号为46127110。1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.05.023198P. Jezek等人理论计算机科学电子笔记160（2006）1971介绍1.1软件构件行为与模型检测模型检验是形式化验证方法之一。检查系统的重要属性（例如没有死锁，数组元素索引在限制范围内）假设描述系统行为的模型可用。该模型定义了一个状态空间，并通过其穷举遍历来验证所需的属性在软件模型检查的情况下，模型可以从系统规范中获得，如ADL（例如Wright [15]，FSP [5]，行为协议[1]）或通过源代码分析（Bandera [10]，SLAM [7]项目和Java Pathview [11]）。模型检测面临两个关键的固有问题-状态空间爆炸和错误跟踪的复杂性和解释。错误跟踪是通过状态空间的路径，表示违反所需属性的特定计算。关于错误跟踪的主要问题是，在数百个状态的数量级上的非常长的跟踪可能非常难以分析和解释[21，22，23，24]。有两种广泛使用的穷举遍历状态空间的策略：深度优先搜索（DFS）和广度优先搜索（BFS）。软件单元（例如软件组件）的规范这是由于需要对大型数据类型域和并行性（线程/进程）进行建模。因此，基于BFS的策略不能实际使用，因为它们对内存的要求很高;相反，必须选择基于DFS的策略。不幸的是，与BFS相比，DFS有一个缺点-它发现的错误跟踪通常不是最短的。1.2论文的目标和结构行为协议[1]是软件组件行为规范的一种方法。它们用于SOFA [16]和分形[4]组件模型中的行为规范。我们在组件行为规范的几个重要案例研究中使用了行为协议，这些案例包括大量组件。这包括一个非平凡的基于组件的测试床应用程序在法国电信资助的一个项目，旨在将行为协议集成到分形组件模型。其中一个关键的经验教训是，错误的跟踪长度问题是严重的，必须认真解决。本文的目标是（i）与读者分享在指定非平凡的基于组件的应用程序的行为过程中获得的经验，并表明错误跟踪长度问题确实很严重，以及（ii）描述我们设计的技术来解决这个问题。这些目标在本文的其余部分中反映如下：第2.1节和第2.2节简要描述了行为协议，第2.3节说明了如何将它们用于组件行为规范，并演示了将用作运行示例的非平凡应用程序片段上的错误跟踪长度节中3，作为关键贡献，所提出的解决技术，P. Jezek等人理论计算机科学电子笔记160（2006）197199描述了误差迹线长度和解释问题节第4节载有对拟议技术的评价，而第5节讨论了相关工作。第六节总结全文并提出未来的研究方向。2行为协议检查2.1行为协议和软件组件软件组件是软件的构建块，并通过接口绑定进行通信[4，15，16]。组件可以通过其提供者（服务器）接口提供某些功能，并且可以从其环境请求其他功能虽然它需要（客户端）接口，但它需要（其他组件）作为一个例子，考 虑 图 3 上 的 DhcpServer 组 件 。 它 是 由 另 外 两 个 组 件 构 建 的 复 合 组 件 -ClientManager 和 DhcpManager ， 这 两 个 组 件 通 过 它 们 的 API 接 口 绑 定 。DhcpServer有一个提供接口（Mgmt）和两个需要接口（PermanentDb和Callback）。行为协议[1]是描述组件行为的表达式;行为意味着组件接口上的活动被视为接受和发出的方法调用事件的序列（跟踪）。行为协议5在语法上由事件表示（令牌）、操作符（图1和括号）组成。对于接口i上的方法m，有四个事件令牌变体：我是一个！i.m↑Acceptinganivocation：？i.m↑Emittingaresponse：！i.m↓Accceptingaresponse：？i.m↓此外，定义了方法调用的三个语法缩写：Issuingamethodcall：！I.Misanabbreeviationfor！i.m↑;？i.m↓Accceptingamodcall：？I.Misabbreeviationnfor？i.m↑;！i.m↓一种方法的程序：？我的快递员是谁？i.m↑;expr;！i.m↓m eaning，表示在发出和接受其他事件方面，m对呼叫的反应。操作者意义;顺序：a;b表示在执行a之后执行b+备选：a+b表示执行a或b*重复：a*表示a执行零到有限次数|和-平行：a| b生成由a和b定义的序列的所有任意交织||或平行：a|| b代表（a| b）+ a + bFig. 1. 基本协议操作员原则上，行为协议与CSP类似，但它们不是通过递归方程定义的，而是仅通过表达式定义的，并且生成的轨迹是有限的。此外，并行运算符|和||原则上是语法缩写（可以用+和;代替）。涵盖了CSP意义上的并行组合同意操作员（第2.2节）。由于行为协议的完整定义需要比本文提供的更多的空间，我们请读者参考[1，2]。200P. Jezek等人理论计算机科学电子笔记160（2006）197作为一个例子，考虑图1中的行为协议的片段二、 根据它，ClientManager组件能够在接口上并行地接受RequestNew、Update和Return方法调用，并执行任何有限次数。如果Return方法调用被接受，组件的反应是在其Callback接口上执行Disconnected此外，可以随时发出Disconnected（？Listener.RequestNew||？Listener.Update||？返回{！回拨。已断开连接}）* 的文本|！回拨。已断开连接 *图二. ClientManager帧协议虽然行为协议可以定义无限的轨迹集，但每个轨迹都是有限的-重复操作符表示其参数重复的任意有限数量。每个行为协议定义了一个有限自动机，其转换由协议的事件标记图例说明：接口名称接口名称需 要 提供绑定图三. DhcpServer复合组件体系结构一个组件的框架这些通信事件子组件出现在行为中。使用图中3为例，其帧协议仅包含Mgmt、PermanentDb和Callback接口的事件组件是通过DhcpManager和ClientManager组件的帧协议的并行组合来创建的Ted客户经理收听者Mgmt请求新更新返回收听者德赫普什永久IPDhcpServerMgmt回调PermanentDbGetIPPermanentDb迪科内克CallbackP. Jezek等人理论计算机科学电子笔记160（2006）1972012.2方案依从性和组成使用行为协议描述组件行为的主要好处在应用程序的设计阶段。开发人员可以检查他/她组成的组件是否具有兼容的行为：它可以检查组件的兼容性水平（例如ClientManager 和 DhcpServer 组 件 之 间 ） 和 垂 直 （ DhcpServer 框 架 协 议 和 由ClientManager和DhcpServer框架协议的并行组合创建的架构协议之间）[1]。水平协议兼容性是通过同意操作符[2]定义的，它基本上是一个将子组件的通信事件转换为内部（τ）事件的并行组合这类似于CSP，但除此之外，同意合成检测三种合成错误：不良活动，无活动和无限活动。当组件在接口上发出调用，而提供该接口的组件无法接受（ac-根据其行为协议）这样的呼叫。没有活动是死锁，无限活动意味着在同意运算符和合成错误在[2]中有详细描述。垂直兼容性通过方案合规性获得[1]。协议符合性在组件的框架协议和其架构协议之间定义2.3示例：测试台应用程序在本节中，我们描述了在第21节中提到的测试床应用程序（“无线互联网接入”）的一个片段一点二该应用程序是一个相当复杂的系统，允许各种航空公司的客户通过本地Wi-Fi网络从机场休息室访问互联网整个无线互联网接入应用程序由大约20个分形组件组成。其中一个关键组件是DhcpServer复合组件（图3）。它在最低级别与系统的客户端通信，即负责管理客户端的IP地址，监控本地无线网络的整体状态，并将此信息提供给系统的其余部分。本节介绍了一个简化版本。2.3.1DhcpServer架构原则上，DhcpServer复合组件以两种功能模式工作，可以通过Mgmt接口进行交换：(i) DhcpServer为新客户机动态生成IP地址（这是默认功能，也可以通过在Mgmt接口上调用HTTP TransientIPs方法来设置）。(ii) DhcpServer根据客户端的MAC地址与通过PermanentDb接口可访问的外部数据库中的IP地址之间的映射202P. Jezek等人理论计算机科学电子笔记160（2006）197管理界面）。当客户端从网络断开连接时，DhcpServer在其Callback接口上调用Disconnected如 前 所 述 ， DhcpServer 功 能 是 由 它 的 子 组 件 实 现 的 ： ClientManager 和DhcpServer。DhcpServer的架构和子组件之间的绑定如图所示3 .第三章。（！Listener.RequestNew||！Listener.Update||！Listener.Return）*见图4。 Dhcptron的帧协议Dhcpdee组件负责与网络客户端和网络基础设施的“真实”通信。在内部，它使用现有的系统基础设施来管理客户端节点。发生在网络级别的事件由Dhcparr统一，Dhcparr将它们转换为方法调用。由于它们可以在任何时间到达，因此相应的帧协议必须表达固有的并行性（图1）。4）.ClientManager接受来自DhcpServer的网络事件通知，并在内部（RequestNew和 Update ） 处 理 它 们 ， 或 将 它 们 转 发 到 DhcpServer 的 环 境 （ 通 过Callback.Disconnected）作为Return处理的一部分。（（A.1一？Listener.RequestNew||？Listener.Update||？返回{！回拨。已断开连接}A.2）* 的文本|！回拨。已断开连接 *）的方式|什 么 ？管理员永久IP ↑）;！管理员永久IP ↓ ;（A.3B.1BB.2（（？.RequestNew {！PermanentDb.GetIP}||？Listener.Update||？返回{！回拨。已断开连接}）* 的文本|！回拨。已断开连接 *）*））的方式|什么？管理员登录TransientIP↑）;！管理员登录TransientIP ↓B.3图五. ClientManager的框架协议（突出显示的行表示形成第节中描述的组成错误的事件。2.3.3）ClientManager 协议的A部分表示ClientManager的P. Jezek等人理论计算机科学电子笔记160（2006）197203静态”功能。A.1和B.1部分表示ClientManager处理Dhcpardian通知的能力，并描述了对这些通知的部分A.2和B.2捕获ClientManager在内部检测客户端断开连接的能力，导致调用Disconnected。ClientManager的功能模式交换机制在部分A.3和B.3中被反映：在任何时候，ClientManager可以接受请求模式改变的方法调用（？管理永久IP↑或？管理员将临时IP↑），但我不会立即回复。相反，它会一直等待，直到完成了对RF缓存上所有挂起的方法调用的处理，并将其删除！管理员登录永久IP↓或者那个！管理员临时IP↓response。C谎言又开始了接受在所述接口上的进一步调用，并根据其新设置的功能模式对它们作出响应。2.3.2DhcpServer帧协议DhcpServer的帧协议如图6所示。DhcpServer的子组件之间的交互这一点在图1中的帧协议的C部分中得到了说明。图6：The！Callback. ClientManager子组件可以调用断开连接的调用，作为对已接受？返回调用或由于其内部检测到客户端断开连接（节。2.3.1）;然而，这两个原因在DhcpServer帧协议中无法区分。协议的D部分表示DhpcServer（C！回拨。已断开连接 *|！回拨。已断开连接 *|（一）？管理员永久IP ↑;（D.1！永久数据库获取IP*+（操作员选择DD.2）*！管理员永久IP↓;？管理员登录TransientIP ↑））;！管理员登录TransientIP ↓）见图6。DhcpServer的帧协议的第一个版本（而不是+，|运算符应该在这里使用，如第 节中的错误跟踪所 示。2.3.3）2.3.3检查组成错误和符合性设置复合组件（例如Dhcp-服务器）的应用程序开发人员还创建其框架协议，而子组件（ClientManager和Dhcp）的框架协议由其各自的作者创建。开发人员有客户端管理器和Dhcpdee的框架协议（Sect.2.3.1）在这个意义上是兼容应该强调的是，即使组件通过类型兼容的接口连接，也可能发生行为不兼容。204P. Jezek等人理论计算机科学电子笔记160（2006）197复合组件开发的下一步在DhpcServer组件的第一个版本的开发过程中，+运算符被用于其帧协议中（图6）。然而，这种协议不符合其架构协议（第2.3.1节）。使用行为协议检查器，错误被发现并通过错误跟踪报告（图10）。7）。(S0)τ.Return↑（S1）τ.Update↑（S2）τ.Update↓（S3）τ.RequestNew↑（S4）τ.RequestNew↓(S5)τ管理永久IP↑（S6）τ回调.断开连接↑（S7）τ回调.断开连接↑（S46）τ回调.断开连接↓（S47）τ回调.返回↓(S48)τ.返回↑（S49）τ.更新↑（S50）τ.更新↓（S51）τ.请求新↑（S52）τ.请求新↓(S53)τ回调.断开连接↓（S54）τ回调.断开连接↑（S55）τ回调.断开连接↓（S56）τ回调.返回↓(S57)联系我们（S117）τ.RequestNew↓（S118）τ.Update↑（S127）τ. Update ↓（S128）τ.Return↑（S129）τCallback.Disconnected↑（S130）τCallback.Disconnected ↑（S171）τCallback. Disconnected ↓（S188）τ.Return↓（S189）τ.Update ↑（S190）τ. Update ↓（S191）τ.RequestNew↑（S192）τ.RequestNew↓（S193）τ回叫.断开连接↓（S226）τ管理.恢复永久IP↓（S227）τ恢复.返回↑（S228）τ恢复.更新↑（S229）τ恢复.更新↓（S230）τ恢复.请求新↑（S231）！永久数据库GetIP↑见图7。 表示符合性错误的然而，仅仅从这样一个简单的错误跟踪中识别出实际的错误并不是一个简单的任务。 关键的问题是，真实组件的错误跟踪往往是相当神秘的，特别是，几个方法调用的帧协议可以并行发生。这导致错误相关事件与“后台”中处理的其他事件交错。例如，只有图7上突出显示的事件导致DhcpServer的帧协议（图6）的D.1和D.2部分需要并行处理的结论 可以发布！PermanentDb.GetIP调用（在B.1中）与接受？管理员临时IP↓调用（见B.3）。3错误痕迹分析与解释方法在行为协议中，错误跟踪的结束在状态空间（由协议定义）中被反映为状态F。行为协议的一个特殊特征是，到达F的每个跟踪都是错误跟踪。 因此，F是一个错误状态。 因此，错误状态表示一组错误轨迹SF。(Note错误状态的存在不是LTS的一般特征找到SF的所有元素意味着完全遍历状态空间。然而，有时，与错误状态相对应的整个错误轨迹集的知识对于错误原因的识别可能是非常有益的由于错误跟踪的集合可能是巨大的（甚至是有限的），P. Jezek等人理论计算机科学电子笔记160（2006）197205它作为一份痕迹清单不会有多大帮助。因此，需要额外形式的SF表示。3.1简单错误跟踪如第2.3.3节所示，识别合规性或组成错误的错误跟踪可能很长，难以解释。此外，由于所使用的DFS策略，错误跟踪可能包含没有捕获错误的“本质”的状态。例如，图7中的错误轨迹的状态子序列S5、S226、S230、S231也形成错误轨迹，但是首先找到较长的错误轨迹。在这方面，其他国家是“不重要”的国家。过滤出这些“不重要”的状态（找到与错误状态相关联的错误跟踪集的规范表示）是一个挑战。我们可以想象一种基于迭代重新搜索状态空间的滤波技术，它将利用发现错误的深度知识3.2状态空间可视化为了使错误解释更容易，我们提出的检查输出之一是状态空间可视化。可视化是与协议相关的状态空间的图形表示（第2.2节）。对于与第2.3.1节相关的状态空间，这在图8中示出（为了简洁起见，这里仅捕获状态空间的一部分）。这有助于通过跟踪状态空间中的错误跟踪来显然，状态空间的大小可能是一个问题-一个状态空间有超过1,000个状态是很难想象的。因此，只可视化状态空间的一部分成为实际需要。从这个角度来看，只捕获包含错误状态及其“邻域”的部分是一个简单的我们用一个非常积极的经验采用了这个想法。这样的结果仍然提供了有用的信息，足够详细以确定错误的本质在哪里。从技术上讲，我们的可视化输出从错误跟踪上的状态开始的所有转换-这有助于找到与原始协议的对应关系。3.3方案注释另一种表示错误状态的方法是注释协议。考虑协议P和Q通过同意操作符的组合。如果组合产生错误状态S中的组合错误，则状态S由标记放入P和Q中表示为了说明，考虑图9，其中DhcpServer的注释帧协议的片段对应于Sect.2.3.3描述。有利的是，不需要构造整个状态空间，但它允许仅注释在组合中以操作数为特征的协议。 例如，由图9中的注释协议指定的错误跟踪集合，以及DhcpServer内部的注释架构协议，产生错误跟踪：206P. Jezek等人理论计算机科学电子笔记160（2006）197···联系我们τ回调。断开连接↑··.更新↑τMgmt. PermanentIP ↑联系我们S226管理员登录永久IP ↑S5τ回调。断开连接↑·返回↑管理员永久IP ↓S230τ.RequestNew↑·S231 τ回调。断开连接↑·τMgmt. TransientIPs ↑·τMgmt. TransientIPs ↑τ回调。断开连接↑·S0见图8。状态空间可视化-虚线表示由于本文篇幅有限而省略的较长路径。状态S231是错误状态F。τCallback.Disconnected↑;τCallback.Disconnected↓;τMgmt. PermanentIps↑;τMgmt. PermanentIps↓和τMgmt. PermanentIps↑;τMgmt.PermanentIps↓;τCallback.Disconnected↑;τCallback.Disconnected↓有两个问题需要解决这个技术：(i) 备选项中的相同前缀。例如，考虑以下帧协议：（？i.m1;？i.m2）+（？i.m1;？i.m3）。如果一个错误的状态是指示后？i.m1，相应的注释协议采用以下形式：（？i.m1 HERE>;？i.m2）+（？i.m1 HERE>;？（i. m3）即使其中一个选项可以被删除，我们还是倾向于保留这两个选项，以提供更多的错误背景(ii) 对输入协议执行的转换。在协议检查器中，协议在解析过程中被修改（例如 ， 什 么 ？ i.m 分 解 成 o ？ i.m↑; ！ i.m↓andthetheformattinginformationislostt）.将错误状态映射回源协议可能是困难的。幸运的是，这些转换通常仍然会产生一个合理可读的协议，该协议经过注释，为规范调试提供了有用的信息4评价在第2.3节中提到的案例研究工作中，结果表明，将所有三种形式的检查输出结合起来是最有前途的方法。尽管协议注释（3.3节）看起来是一种非常通用的技术，但在复杂的情况下，还必须提供其他检查输出，因为跟踪注释的复杂协议中的所有路径选择可能容易出错。P. Jezek等人理论计算机科学电子笔记160（2006）197207（（？回拨。断开↑;！回拨。断开连接↓<这里>）*）|（（！管理员PermanentIps↑;（（？PermanentDb.GetIp↑;！PermanentDb.GetIp↓）*）+（？管理员PermanentIps ↓;！管理人员临时Ips ↑）;？管理层瞬变Ips ↓*）的情况）见图9。 DhcpServer注释帧协议-简化。案例研究中最复杂的组件具有多达60个事件的行为协议;这些行为协议生成具有数十万个状态的状态空间。在开发此类组件期间遇到的典型错误会产生长度约为100个状态的错误跟踪然而，也有一些错误状态生成了数百个状态的错误跟踪。然后，开发人员花了大约一个小时（通常甚至更多）来识别实际的错误，以防只有普通的错误跟踪可用。在Sect.3种方法，提高了调试在我们的案例研究应用程序的进一步开发过程中，开发人员使用了这些技术的组合，解决典型错误的平均时间缩短到原来的三分之一或四分之一至于普通错误跟踪检查输出，一个问题是组件行为中存在“局部循环”。通常，相对于系统的其他部分，本地环路遍历的实际数量在错误定位方面没有意义。这些循环延长了错误跟踪，使其更加复杂和难以分析。显然，如果循环是嵌套的，情况会更糟。 一个愿望是消除那些对系统其余部分的“不干涉”。 这是一个具有挑战性的问题-目前，只有最高级别的循环被识别并以自动化的方式消除。带注释的协议与Bandera Toolset中使用的方法非常相似[10]和PREfast [3]，因为它们是基于对输入协议中发现组成错误的位置的强调。与Bandera和PREfast不同，在行为协议中，两个操作之间的位置被突出显示以表示错误状态。5相关工作在[23]中，作者通过提出一种方法来解决反例复杂性和解释问题，该方法将“正”和“负”作为相关的正确迹和错误迹的在[21]中选择了一种有趣的方法，作者通过构建与特定错误轨迹“最接近”的正确轨迹来分析错误解释的复杂性在[24]中，作者描述了一种算法（“增量调试”），用于找到一个最小的测试用例，识别程序中的错误。这个想法可以用来修改错误跟踪，以找到一个“足够接近”的正确错误。在[22]208P. Jezek等人理论计算机科学电子笔记160（2006）197其中在单个检查运行中生成多个错误跟踪静态驱动程序验证器（SDV）[6]是一个用于验证WDM（Windows驱动程序模型）[8]驱动程序正确行为的工具驱动程序的 如果规则如果违反了，则生成程序的错误跟踪并将其映射回驱动程序的C源代码。由于WDM驱动程序非常复杂，为了使检查可行，Windows内核模型和SDV中使用的规则都必须简化。因此，由SDV生成的误差迹线相对较短并且易于解释。而且，由于它们还包含与遍历内核模型相对应的状态，因此这些部分可选地隐藏在检查输出中。这个解决方案也适用于我们的简单错误跟踪（3.1节）：在方法调用中生成的事件可以被分组到然而，由于不容易识别单个元数据的开始和结束，因此不容易识别单个元数据的开始和结束（特别是在元数据的情况下），因此不容易识别单个元数据的开始和结束。我想你会喜欢的未使用），在行为协议检查器中采用该思想不是一个简单的任务。至于经典的模型检查器SPIN [9]，在违反LTL中指定的检查属性的情况下，Spin允许遍历跟踪到错误状态，同时观察变量值，进程通信图和突出显示的源代码。有时，错误跟踪长度使得这种方法非常难以使用，并且识别实际问题可能非常具有挑战性。尽管在大多数情况下，简化SPIN中错误跟踪解释的方法工作良好，但其建模语言Promela [9]不是合适的指定软件组件。由于Promela中的这种指定通常会产生一个很大的状态空间，无法在合理的时间内遍历。至于其他工具，Java Pathwords（JPF）[11]，Bogor [17]，BLAST [18]，SMV[12]，Moped [19]和MAGIC [20]处理反例，并将它们作为错误跟踪提供。具体来说，JPF、Bogor、BLAST、Moped和MAGIC打印导致错误状态的步骤序列，并由源代码的相应行进行注释，而SMV工具提供了由SMV规范语言编写的输入文件行组成的错误跟踪。Moped类似于SDV，因为它首先将输入程序（Java）转换为LTL语言，在LTL中生成反例。然后将它们翻译回输入语言。 MAGIC工具检查C程序的行为，通过LTS描述的规范。除了错误跟踪之外，它还可以使用GraphViz包[13]的点工具（也由行为协议检查器使用）生成控制流程图和LTS在所有情况下，特别是在JPF的情况下，错误跟踪可能会变得非常复杂，并且不容易解释。6结论和今后的工作在项目工作期间（第2.3.1节），事实证明，除了简单的错误跟踪外，还需要额外的检查输出来加速错误检测和调试过程。因此，我们引入了两种方法：（i）状态P. Jezek等人理论计算机科学电子笔记160（2006）197209空间可视化，和（ii）注释协议。使用所有三种方法相结合，发现最有益的（定位错误，然后更有效（节。（4））。当检查由真正复杂的行为协议描述的几个组件的组成/合规性时，会出现问题。由这样的协议生成的大的状态空间导致错误跟踪通常非常长并且难以解释。尽管如此，在我们看来，这是值得追求的，因为我们相信组件因此，我们未来的工作重点是改进行为协议检查器目前使用的方法;特别是，自动删除不必要的“本地循环”的方法至于状态空间可视化，需要一种用于检测状态空间的“重要”部分的自动化方法与Bandera [10]和PREfast [3]类似，动态指示错误跟踪中特定位置与协议相关部分之间的对应关系的可能性可能会进一步简化和加速调试过程。引用[1] F. Plasil，S. Visnovsky，软件组件的行为协议，IEEE软件工程学报，第28卷，第11期，2002年[2] J. Adamek，F.张文，软件结构错误与更新原子性：静态分析，《软件维护与演化：研究与实践》，第17卷，第4期，John Wiley，2005年[3] 预禁食-http://www.microsoft.comwww.example.com/whdc/devtools/tools/PREfast. mspx[4] E. Bruneton，T. Coupaye，M. Leclerc，V. Quema，J-B.史蒂芬妮一种开放组件模型及其在Java中的支持。第七届SIGSOFT基于协作的软件工程国际研讨会（CBSE 7），LNCS 3054，爱丁堡，苏格兰，2004年5月。[5] J. Magee，J. Kramer，[6] SDV -http://www.microsoft.com/whdc/devtools/tools/SDV.mspx[7] T.球，S。K. Rajamani，SLAM项目：基于静态分析的可重构系统软件，POPL 2002，ACM，2002年[8] WDM -http://www.microsoft.com/whdc/archive/wdm.mspx[9] Spin，Promela -http://spinroot.com/spin[10] 班德拉- http://bandera.projects.cis.ksu.edu[11] Java路径查找器-http://javapathfinder.sourceforge.net[12] SMV -http://www-2.cs.cmu.edu/模板检查/smv. html210P. Jezek等人理论计算机科学电子笔记160（2006）197[13] GraphViz- http://www.research.att.com/sw/tools/graphviz[14] 马赫，M.，Plasil，F.，Kofron，J.，行为协议验证：战斗状态爆炸，国际计算机与信息科学杂志，ACIS卷。号62005年3月1日[15] Wright-http://www-2.cs.cmu.edu/访问/wright[16] SOFA -http://sofa.objectweb.org[17] 茂物- http://bogor.projects.cis.ksu.edu[18] BLAST-http://www-cad.eecs.berkeley.edu/[19] 助力车-http://www.fmi.uni-stuttgart.de/szs/tools/moped[20] MAGIC-http://www-2.cs.cmu.edu/chaki/魔术[21] N. Kumar，V. Kumar，M. Viswanathan，错误解释的复杂性，VMCAI'05，ACM，2005年[22] 鲍尔，Naik，M.，Rajamani，S.，从症状到原因：在反例跟踪中定位错误POPL 2003会议记录，ACM，2003年[23]Groce，A.，Visser，W.，什么错了：解释反例，SPIN软件模型检查研讨会论文集，LNCS 2648，Springer，2003年[24] Zeller，A.，隔离计算机程序的因果关系链FSE 2002会议录，ACM 2002