FDR: Hoare的CSP模型检查器内部结构分析及标记转换系统实现

理论计算机科学电子笔记187（2007）19-34www.elsevier.com/locate/entcsFDR ExplorerLeo Freitas Jim Woodcock吉姆·伍德科克1，2约克大学计算机科学系YO10 5DD York，英国摘要在本文中，我们描述了FDR的内部结构，Hoare的通信顺序进程（CSP）的细化模型检查器有了这些信息，就可以创建优化的CSP代码来执行更节省空间/时间的细化检查，从而能够分析更复杂和数据密集型的规范。 这些信息对于CSP用户和自动生成CSP代码的工具都非常有价值，如那些与安全分析相关的测试用例生成为CSP过程。我们还提出了一个简单的例子，使用该工具。最后，我们展示了如何将FDR的图形格式转换为图形符号（例如，，JGraph），从而实现CSP规范的标记转换系统关键词：精化，模型检查，CSP，FDR，标记迁移系统，应用程序编程接口1引言硬件和软件系统中不断飙升的复杂性增加了对可靠性和正确性的需求，最明显的是在高完整性和安全关键领域[1]。实现这一目标的一个有效方法是通过使用正式的规范和验证。然而，无论这些技术多么有用，由于不同组件的并发交互导致的可能的场景数量庞大，工具支持是必不可少的。例如，要分析的不同行为的数量可以达到10个不同的状态，在一个由10个20个吃饭的哲学家组成的并行网络上。在本文中，我们特别感兴趣的是使用其自动工具FDR [7]为进程代数CSP [15]的精化模型检查CSP是一种成功的技术，具有工业强度的工具支持，已使用了二十年。在1 我们非常感谢QinetiQ Malvern对我们研究团队的长期支持。2 电子邮件：leo@cs.york.ac.uk，jim@cs.york.ac.uk1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.08.04220L. Freitas，J.Woodcock/Electronic Notes in Theoretical Computer Science 187（2007）19在这种情况下，所有可观察到的行为都由一个标记转换系统（LTS）表征，表示CSP规范的（操作）语义[17，第4章]。然后，FDR被用来详尽地分析这些LTS的各种目的，主要是细化检查，确定性，死锁和活锁自由。由于与其他形式验证技术（如定理证明[2]）相比，模型检查的自动化程度很高，CSP和FDR的使用在学术界和工业界都非常有吸引力。FDR 将 两 个 CSP 规 范 编 译 成 合 适 的 LTS ， 以 检 查 它 们 是 否 来 自 细 化 排 序（S±mI）。这些通常是系统的抽象规范（S）或感兴趣的某些特定属性（表示为CSP过程），以及中间设计或更具体的实现（I），人们希望检查对给定模型（m）的细化，这定义了细节的粒度。为了执行检查，FDR从每个编译的LTS中穷举地搜索相互可达的状态对。也就是说，对于所有可能的迹线，通过遍历同一迹线上的两个LTS可以达到的状态。更确切地说，当且仅当一对在搜索中是相互可达的，它们遵循关于可用可见事件的两个LTS上的兼容转变的选择。不兼容行为的特征在于违反了选定模型的至少一个细化标准。这些标准包括每个相互可达对的信息，例如跟踪、可接受（或拒绝）行为和分歧。因此，如果发现一个不兼容的对，那么设计（I）不满足给定模型（m）上的属性或规范（S）定义的所有行为，因此建议的改进不成立，调试信息可用。所选模型（m）的粒度能够验证系统的不同方面，例如迹线模型（T）的安全属性、故障模型（F）的不确定性以及故障发散模型（FD）的发散（或catastrophic/不可预测）行为。关于（细化）模型检验的更多细节可以在[14，6]中找到尽管如此，这种按钮技术，使自动错误验证的正确性和完善。这在为FDR编写适当的CSP时会引起用户的相当多的麻烦，这通常意味着对有界模型的抽象。问题是，就我们所知，没有彻底和明确的指导来源。相反，人们需要筛选许多不同的（和不相关的）来源。假设用户对CSP有很好的了解，我们的工具可以帮助FDR用户生成更有效的CSP代码，并找到一些模糊的执行错误的原因，例如通道数据类型之外的通信。也许它可以更好地作为FDR和编写CSP代码的更高级工具之间的桥梁。FDR（版本2.82）的完整参考文献列表包括：手册[7]、模型检查算法[14，12]和内部自动机理论数据结构[3];关于FDR转换系统的广告信息提供了一L. Freitas，J.Woodcock/Electronic Notes in Theoretical Computer Science 187（2007）1921由于它与FDR的CSP有很好的兼容性，FDR能够自动分析相当大的系统。此外，如果人们探索CSP操作者的组成特性，如[13，p.198]中的一个例子所示，达到惊人的数字7101000个国家。这不是实际的州数由FDR检查，但是组合的系统组件的状态的总数。这意味着检查状态空间的一小部分与检查整个状态空间一样好。通过处理如此大量的状态，FDR不仅能够建模硬件，还能够建模非常复杂的软件设计，如[16]所示因此，我们提出的探索性工具的主要目的是为FDR用户提供更好的指导，并与其他外部CSP工具更好地集成。这是通过彻底的研究，实验和重建的可用信息从两个来源在一种“软件考古学”。这些来源是FDR作为这样的“考古学”调查的结果因此，可以在可接受的时间尺度内分析复杂的规范，并为自动生成CSP脚本的工具提供改进的可操作性。这种工具集成趋势遵循计算机研究中的一个重大挑战中提出的原则[1]。我们的工具已在很大程度上用于[4]中提出的工作。 我们还知道它已被用于巴西的一个项目中，用于从CSP编码的各种测试技术巴西的另一个项目将输出的FDRExplorer转换为测试用例生成工具TGV的特定格式[20]。在下一节中，我们将描述FDR的内部结构和对象模型，其中包括与我们的工具交互的FDR API。之后，第3节通过展示它如何扩展FDR的API来展示我们添加的功能 接下来，在第4节中，我们将给出一个运行示例。第5节描述了如何将底层FDR LTS转换为具有图形可视化工具支持的可视化图形格式[8]，并指出了未来如何进一步集成FDR与图形工具的方向最后，对全文进行了总结，并对未来的第六节方向相关工作。这方面的相关工作很少。FDR手册[ 7，附录C]中的简要信息这些脚本模仿FDR的一些就我们所知，只有一种工具可以利用FDR提供的脚本语言[11]。它提供了基于各种策略的死锁和活锁自由的特殊形式，用于识别表示CSP规范的图形中的模式此死锁检查工具打开与FDR服务器的连接，并使用可用的Tcl/Tk脚本来编译CSP规范并执行专门的检查，其中不处理调试信息。这些文字是原始的-22L. Freitas，J.Woodcock/Electronic Notes in Theoretical Computer Science 187（2007）19我们工作的灵感源泉。此外，Valmari2FDR在本节中，我们通过描述FDR的对象模型来解释FDR2.1罗斯福FDR的架构分为两层。顶层是图形用户界面（GUI）或直接批处理界面，两者都是使用面向对象的Tcl/Tk版本编写的。底层的FDR服务器是一个用C++编写的Tcl/Tk解释器。该解释器具有预加载的对象模型，该对象模型提供：（i）被称为CSPM的机器可读CSP的解析和编译;（ii）在机器可读CSP的编译过程中，各种精化模型检查算法的实现;以及（iii）关于精化算法的全面调试信息。从GUI，用户加载规范，添加/执行细化检查，并可视化地调查调试信息。在批处理界面中，用户可以执行相同的操作，但文本反馈会记录到标准输出中。批处理接口对于非交互式检查或通过网络进行检查非常有用。顶层接口实现的这些功能是Tcl/Tk脚本，这些脚本以适当调用底层FDR服务器中的对象模型方法的方式也就是说，使用正确数量的参数，以正确的顺序，并在正确的时间。因此，通过摆弄这些Tcl/Tk脚本（或创建新脚本），可以微调FDR：（i）详细调查LTS中不同点的个体证人和行为;（ii）如何创建更时空有效的CSP规范;以及（iii）将FDR的LTS格式转换为可用库的图形格式，这就是我们的探索工具所做的。它充当批处理接口顶部的另一个接口，允许对可用调试信息进行扩展控制，以及访问FDR这三点中最重要的是提供了关于如何优化CSP规范的见解。这是可能的，因为FDR根据CSP操作符生成的LTS的形状，将CSP操作符分为低级和高级操作符高级操作符是生成组合（和模块化）LTS的所有操作符最常见的高级运算符是hiding、parallelism和renaming。低级操作符是提供核心顺序语言的所有操作符，并生成对压缩不太敏感的LTS最常见的低级运算符是前缀、选择、顺序组合、原始过程和递归。因此，处理的级别越高，对应的LTS将越容易压缩。显然，并不总是能够提供L. Freitas，J.Woodcock/Electronic Notes in Theoretical Computer Science 187（2007）1923最紧凑的LTS由于所描述的过程的结构。尽管如此，在检查复杂或数据密集型规范时，记住这种结构证明非常有用[16，10]。这些信息可能不仅对处理复杂规范的经验丰富的CSP用户感兴趣，而且对自动生成CSP代码的其他工具也很感兴趣，例如使用CSP进行测试用例生成的安全分析工具[10，18]。通过检查隐藏在两个顶级接口中的对象模型方法，我们能够准确地告诉如何以及在何种情况下，可以提高编译的CSP LTS的紧凑性或效率。2.2可用功能对象模型提供了四个主要功能：（i）表示规范源的会话管理;（ii）表示具有嵌入式细化检查算法的编译LTS的解释状态机（ISM）除了在[7，Appendix C]中的简要解释外，据我们所知，对象模型的细节没有文档记录。会话管理。它允许管理（一组）用于细化检查会话的加载规范源。它实现两个功能：（i）脚本管理;(ii)脚本评估。脚本管理允许文件加载，并选择性地显示规范中的各种信息，例如加载的CSP过程和通道，关于精化声明和属性检查的断言，整个规范脚本中使用的表达式列表，等等。一旦规范被加载，脚本评估就成为FDR精化算法和LTS的入口点。它支持将CSP过程编译为LTS，以及计算数学表达式和表示属性检查的细化断言。解释状态机（ISM）。它们代表一个编译状态机，并且是FDR的核心功能：通过会话对象（通常来自CSP规范）对编译的LTS进行细化检查。也就是说，底层FDR服务器足够通用，不仅可以表示CSP，还可以表示和模型检查特定类别的LTS。显然，CSP的操作语义适合这一类别。每个ISM实现三个功能：（i）LTS描述;（ii）LTS结构;和（iii）LTS分析。LTS描述是一个数据库，其中包含进程名称、其原始ASCII脚本以及它所描述的进程所使用的事件的计算字母表更有趣的是LTS结构，它包含LTS的详细特征，例如细化搜索根节点，每个LTS节点的初始事件表示传出转换，通过特定事件到达的下一个节点，（最小）24L. Freitas，J.Woodcock/Electronic Notes in Theoretical Computer Science 187（2007）19在某些细化检查期间使用的每个节点的接受和发散计算，有关LTS压缩的高级信息，各种CSP运算符被视为低级或高级的方式，等等。最后，通过LTS分析，可以从各种嵌入式算法中进行选择，例如细化检查，死锁和活锁自由，或规范的确定性特征。假设对象。一旦为编译的ISM选择了一个模型检查算法，FDR服务器返回一个假设对象。它代表了一个关于ISM的断言。 假设对象生成调试信息（或成功报告），允许调查细化失败（或成功检查）的原因。它还包含简单的状态，定义检查是否已执行，检查状态是什么，以及LTS结构的哪些部分将检查。收集信息。它详细描述了细化失败的见证。该信息分为三个功能：（i）调试上下文;（ii）调试树;以及（iii）LTS节点及其子节点的行为。调试上下文是测试假设对象表示的断言的结果，并且作为单独的调试窗口存在于FDR GUI它包含三种信息：（i）参与者进程;（ii）每个参与者的调试树;（iii）包含每个参与者的错误行为的见证。调试树表示调试（或正确）进程的LTS及其特征行为。它在FDR GUI中表示为参与进程的树视图。虽然调试上下文可以表示成功的检查，但行为对象总是与细化失败相关，并且它们包含有关在某些跟踪发生后特定LTS的接受（和拒绝）的详细信息。它们表示调试树所表征的允许行为。 这在FDR GUI中显示为小窗口，其中包含关于特定调试树节点处的接受（或拒绝）的对比信息。对于成功的检查，没有调试信息可供用户使用。2.3FDR了解FDR由于完整的FDR下面我们将解释与这些类中的每一个最相关的方法。届会议load（Str，Str）：从给定的目录和文件名加载CSP脚本。compile（Str，M）：在所选的语义模型上编译给定的进程L. Freitas，J.Woodcock/Electronic Notes in Theoretical Computer Science 187（2007）1925Fig. 1. FDR对象模型为了返回ISM对象，compile方法要求进程名必须包含声明的每个形参的实际参数。可用的模型是它返回一个ISM对象。ISM。它将已编译的CSP进程表示为LTS。它们基于[3]中描述的除了关于这个对象表示的文本脚本的琐碎方法外，还有三组与结构[17，第4章，第8章]，算法[14，12]和压缩[13]相关的方法。结构方法如下：root：返回搜索开始的节点索引。alphabet：返回此ISM表示的进程的完整事件名称列表（包括通道名称和值）event（int）：返回进程alpha- bet中给定索引处事件的相应名称。如果索引大于元素的大小，则返回空字符串。每个进程在其字母表中都有两个预定义的事件，用于内部通信（索引为0的“tau”）和成功终止（索引为0的“tau”）。“ tick” atindextransitions：返回LTS转换。每个转换由大括号之间的三个数字表示（例如，，{10 3}），其中源节点索引（1）通过放置在两个节点索引之间的事件编号（0）到达目标节点索引（3）。此事件编号可在事件方法中用于检索26L. Freitas，J.Woodcock/Electronic Notes in Theoretical Computer Science 187（2007）19进程字母表中的相应元素divergences：以布尔值列表的形式返回每个节点索引的divergences。因此，如果LTS包含四个节点，所有节点都不是发散的，则该方法返回一个包含4个设置为false（或0）的布尔值的列表。对于故障-发散（FD）模型之外的检查，不计算此列表，并且假设每个节点索引不发散。acceptances ： 返 回 为transition中提到的每个节点索引设置的 （ 最 小 ）acceptances。每个接受集看起来像此外，由于节点索引1的接受集为空，它表示正在发生内部转换 通过检查节点1的相应发散信息，可以检查该内部转换是否是否会引起分歧。最后，包含空集的接受集（即，、{{}}）表示死锁节点。这里可以再次使用event方法来检索事件名称。initials（int）：返回一个给定节点索引立即可用的字母表元素列表afters（int，Str）：返回从源节点索引通过进程字母表中的事件名称到达的目标节点索引的列表。由于LTS不是完整的，这是一个部分方法，因为不是每个节点都有通过每个事件的转换因此，在这种（部分）情况下，该方法返回一个空的节点集。对于终端节点，也会返回相同的空结果，比如那些表示死锁的节点（例如、STOP）或成功终止（例如，，SKIP）。通过这些方法，人们能够理解FDR如何将CSP过程表示为LTS。这对于为FDR找到足够的CSP规范模式以及理解操作语义的模糊问题非常有用例如，在第4节中，我们展示了一些特殊过程的LTS是如何构造的。接下来，有一些方法可以让用户选择要执行的细化算法。它们创建Hypothesis对象作为断言：refines（Str，M）：假设（refinedBy（Str，M）：假设（deadlockfree（M）：假设（livelockfree（M）：假设（deterministic（M）：假设（最后，还有更先进的方法，描述了FDR如何编码低-和高级过程，以及[7，p.60]和[13]中描述的压缩技术的入口点cheap：返回根节点对应的是低级进程还是高级进程。由于高层过程更容易分解，因此探索CSP操作符的模块化结构，该标记可以用于适当地调整过程L. Freitas，J.Woodcock/Electronic Notes in Theoretical Computer Science 187（2007）1927这在处理复杂或数据密集型规范时特别有用operator：返回用作根节点表示的复合操作符的高级操作符名称，例如hiding或parallelism。wiring：返回一组与复合运算符关联的事件编号在廉价ISM中，例如隐藏集或同步集。parts：返回根节点索引可能表示的复合ISM的子组件ISM的列表。简体中文actors：返回见证中涉及的节点数。证人：返回找到的证人数量。actor（int）：返回一个actor索引的进程名，它由参与者的数量绑定，并指向一个节点索引。attribution（int，int）：返回所选参与者索引处所选见证的行为对象debugtree：返回一个调试树，其中包含有关细化失败的行为信息。搜索上下文还包含搜索根节点的行为，以及涉及的进程名称和找到的见证。它们描述了FDR行为此类的调试信息表示可用的最详细级别的调试它们包含了一些跟踪发生后接受（或拒绝）的信息3FDRExplorer有了FDR工作原理的知识，我们构建了一个扩展API作为Tcl/Tk脚本文件加载到FDR的服务器中。目前，我们有一个用户友好的输出，只是纯文本，从FDR LTS转换到具有图形可视化支持的图形符号语言[8]。前者是为FDR的用户或自动CSP代码生成工具设计的3.1可用功能我们设计的API包含分为五类的方法：（i）进程解析;（ii）进程编译;（iii）信息提取;（iv）帮助方法;以及(v)辅助方法28L. Freitas，J.Woodcock/Electronic Notes in Theoretical Computer Science 187（2007）19检查方法是一个人通常在一个精炼会话开始时调用的主要方法首先，记录当前会话的详细信息，例如已知 接下来，给定的进程列表（带有实际参数 如果需要的话）被编译成ISM，并记录有关其结构的详细信息。在此基础上，自动生成并检验了确定性、死锁和活锁自由三个假设.最后，如果这些假设为假，则记录关于它们包含的调试上下文的信息。这不仅包括调试上下文，还包括在细化失败的情况下的所有行为和调试树。如果脚本包含关于细化检查的断言，或者如果用户想要执行任何指定的细化，那么可以以相同的方式检查创建的假设对象。或者，如果脚本没有需要实际参数实例化的参数化进程，则不需要进程列表，并且自动检查当前会话中的所有进程编译方法可用于在所选CSP模型中为想要检查的进程列表生成ISM。它们由检查方法调用，但用户（或其他工具）可以使用它们来执行特定的编译任务。提取方法记录FDR对象模型中每个类可用的所有Tcl/Tk方法的信息（参见图1）。 也就是说，ISM对象的LTS结构、上述三个自动生成的假设对象的调试上下文（如果有的话）、每个调试上下文的调试树以及详细说明失败原因的相应行为帮助器方法为图1的FDR对象模型中的每个类的每个方法提供消息由于这可能会非常冗长，因此默认输出仅针对ISM、Hypothesis和BullgContext对象。然而，用户（或其他工具）可以有选择地调用可用FDR类的帮助器方法。最后，辅助方法提供了有关如何使用FDR资源管理器API本身、文件加载、Tcl/Tk对象的垃圾收集以及将工具挂钩到FDR服务器的主方法的帮助3.2FDR Explorer API我们在下面详细介绍了与上述每个类别最相关的方法。检验方法inspectProcs（File，List_Str_List，Bool）：从指向CSP脚本文件的文件句柄中检查给定的进程列表。该标记指示是否应删除创建的FDR对象。对于批处理执行，例如由工具执行的批处理，它应该设置为true（或1）。对于需要进一步检查的执行，它可以设置为false（或0）。inspectParameterless（File，Bool）：检查给定文件中的所有进程。如果任何进程具有参数，则会生成错误。对于给定列表中的每个进程，结果将记录到单独的文件中。因此，如果给定一个名为spec.csp的文件和一个进程列表{P（0）Q}，则两个名为L. Freitas，J.Woodcock/Electronic Notes in Theoretical Computer Science 187（2007）1929创建spec.P（0）.exp和spec.Q.exp，每个都包含相应的过程检查。此外，如果这些文件已经存在，则会被截断（即，在被写入之前清除）。汇编方法compileProcInModel（File，Session，Str，M）：从FDRSession对象编译给定模型中的给定进程，并在给定文件句柄上打印结果。参数化进程必须被实例化，否则FDR服务器会崩溃。它将创建的ISM对象返回给用户。compileProcs（File，Session，List）：编译failures-divergences模型中的进程列表。提取方法。在图1的图表中，每个类都有一个提取方法。它们将调用相应FDR类的每个方法的结果记录到给定的输出文件中。它们接收用于记录输出的文件句柄和相应的FDR对象。此外，ISM对象还有一些其他方法用于创建关于确定性、死锁和活锁自由的默认假设辅助方法。同样，每个FDR类也定义了一个helper方法。它们记录每个FDR类的每个方法所具有的角色的文本描述。我们还将常用的helper方法分组在一起。辅助方法FDRExplorerHelp：提供有关FDRExplorer API的说明。load（Str）：创建一个FDRSession对象，并加载给定的完整文件名。deleteAll（File，List）：从对象中释放分配的内存给定列表将结果记录到给定文件中。最后，为了将我们的工具集成到FDR中，我们将FDRExplorer API脚本挂钩到FDR4运行实例为了说明我们的工具的使用，我们在发行版中提供了一系列示例，以及一些额外的帮助文件和完整的类图模型[5]。这包括低级和高级操作员的示例，以及来自[9]的在本文中，我们选择了一个简单的例子来说明如何FDR的LTS结构的知识可以让洞察FDR的工作原理。目的是30L. Freitas，J.Woodcock/Electronic Notes in Theoretical Computer Science 187（2007）19了解FDR如何在外部选择中编码终止（SKIP）的存在。在[15，p.141]中，关于这种情况的定律如下：PQSKIP =PdSKIP=（SKIPH（PQSKIP））=（（PHSTOP）QSKIP）但是罗斯福是如何编码这些过程的呢？为了找到答案，让我们从工具分发包中的skip.csp通道c P =c -> PA= P[]SKIP B=P [> SKIPC =跳过|~|（P[]SKIP）D=（P| ~|停止）[]跳过结果在表1中给出。很明显，FDR的（P Q SKIP）编码比其他版本更有效，因为每个表示中的节点和转换的数量不同。进程A有3个转换和3个节点，进程B和C有6个转换和5个节点的相同LTS，进程D有7个转换和5个节点的最差LTS。由于这些过程的字母表是相同的，因此事件的结果也是相同的。在进程A中，节点0通过事件1（tick），一个接受集包含事件1和2（tickc），其中所有节点都是无发散的。其他的转换可以类似地解释。为了进一步研究这个问题，我们添加了断言，检查这些不同的表示如何相互关联。过程B、C和D在失效-发散模型中是等价的，因为它们相互细化。过程A精化过程B、C和D，但不被它们精化。这表明了在外部选择上最节省空间的终止编码（SKIP）的基本原理，在FDR中使用此外，由于我们默认执行无死锁检查，让我们检查进程D的输出。假设对象包含一个具有一个调试树和以下行为的见证：表演：跳接受：{}可以接受：{tick}{c}拒绝：{tickc}可以拒绝：{c} {tick}这意味着，在执行事件tick之后，D拒绝tick和c，而死锁自由的规范（参见[15，p.375]中的DF）可以拒绝任何一个事件，但不能同时拒绝两者。在FDR的调试窗口中，可以通过按下标有Acc.的按钮来查看。（ 或Ref。）.4.1调用API现在，让我们展示如何使用FDRExplorerAPI。假设目录$FDRHOME/bin位于Unix$PATH中，L. Freitas，J.Woodcock/Electronic Notes in Theoretical Computer Science 187（2007）1931alphabet=勾选Cevent（0）=tau转换={ 0 1 1} { 0 2 2} { 2 2}接受={{ 1 2}}{{}}{{ 2}}event（1）=tick事件（2）=c分歧= 0 0 0工艺A工艺Balphabet=勾选C过渡={00 1}{ 00 2}{ 1 1 3}{ 1 2 4}{ 2 1 3}{ 42 4}承兑={{1 2}} {{ 1}} {{}}{{ 2}}分歧=0 0 0 0 0工艺Calphabet=勾选C过渡={00 1}{ 00 2}{ 1 1 3}{ 1 2 4}{ 2 1 3}{ 42 4}承兑={{1 2}} {{ 1}} {{}}{{ 2}}分歧=0 0 0 0 0工艺Dalphabet=勾选C过渡={00 1} { 00 2} { 0 1 3} { 1 1 3}承兑={1 2 4} { 2 1 3} { 4 2 4}{{1 2}} {{ 1}} {{}}{{ 2}}分歧=0 0 0 0 0表1进程A、B、C和D的FDR LTS，来自fileskip.csp并且FDRExploerer.tcl位于$FDRHOME/lib中，我们在shell提示符下使用以下命令启动FDR服务器：威尼斯$fdr2tix-不安全-nowwindow现在FDR服务器正在运行，我们使用%source lib/FDRExplorer.tcl之后，扩展的API可用，我们可以开始检查进程。32L. Freitas，J.Woodcock/Electronic Notes in Theoretical Computer Science 187（2007）19假设文件skip.csp在当前目录中，我们可以请求所有4个进程的LTS结构，而不删除生成的对象%set lprocs{ A B C D}% inspectProcs''./跳过. csp“” $lprocs0由于文件中没有进程有参数，我们也可以使用命令%无参数检查''./跳过. csp“0作为执行检查方法的结果，将创建四个文件并命名为skipX.csp.exp，其中X将是A、B、C或D。它们包含有关每个进程ISM的详细信息，以及关于确定性的3个默认假设，以及已经检查过的死锁和活锁自由如果任何一项检查失败，还记录了关于调试上下文、调试树和行为的附加信息。最后，如果想要对返回的FDR对象执行操作，可以直接通过手动调用方法来完成。要使用的对象名称是FDR返回的名称。因此，我们可以键入一个命令，例如%会话1编译D-t如果我们希望FDR在当前会话的跟踪模型上重新编译进程D这将产生一个新的ISM，可以以类似的方式调用任何其他可用的方法。5图形可视化目前，从FDR LTS转换到可用图形格式的转换策略[8]确实非常简单。 对于从FDR的LTS的每个转换我们的工具扩展的目的是证明一个概念，即可以可视化CSP LTS和FDR生成的调试信息，从而提高CSP相关工具的用户友好性要执行这样的操作，需要将脚本从fdr2jgraph.tcl文件加载到FDR服务器中， 调用fdr2jgraph方法传递输入CSP文件名、进程名和要生成的输出文件JGraph兼容代码一个开放的可能性是开发一个更彻底的翻译策略，利用许多图形可视化库的各种功能。例如，用于渲染大LTS的图形布局算法，或用于包含接受和分歧信息的节点上的注释支持。另一个有趣的可能性是操纵生成的图，试图找到特定的模式，从而允许更深入地了解所表示的机器的性能，或者建议进一步压缩FDRL. Freitas，J.Woodcock/Electronic Notes in Theoretical Computer Science 187（2007）1933无法预见。稍后，有了这些信息，可以尝试调整/适应原始CSP脚本，以便执行更快，更流畅的检查。等通过CASPER工具[10]，通过不同的CSP规范模式成功实现了一种篡改CSP脚本的策略，该工具将安全协议符号转换为高度优化的CSP代码。这些调查也可以作为一个图形工具的基础，将正式表示CSP语义，从而允许用户正式绘制并发进程！6结论在本文中，我们为CSP [15]细化模型检查器FDR [7]提供了一个新的接口，它扩展了一个可用的用户界面API。它允许扩展对调试信息的控制，以及对LTS数据结构的隐藏功能的调查，这些数据结构用于表示用于精化模型检查的编译CSP规范有了这个工具，可以仔细研究CSP的操作语义，从而为类似于CSP的并发语言开发操作语义[4]。它也被其他人用于使用CSP和FDR的测试用例生成，以及这种新并发语言的Java代码生成工具FDRExplorer API的主要贡献是它能够更好地集成CSP脚本生成工具[18]，并为用户提供更好的信息。这表现为在LTS的不同点调查证人信息的能力，或者对CSP过程的更节省空间的表示进行推理。这些功能在原始FDR界面中不可用。这也遵循了英国计算机研究大挑战之一提出的工具集成趋势[1]。我们还展示了一个运行该工具的例子，用于找出FDR如何表示外部选择中存在终止（SKIP），我们发现这很有启发性。最后，我们解释了如何将可用的CSP LTS转换转换为具有可视化工具支持的图形符号格式[8]。这是与CSP可视化工具集成的第一步。更进一步，可以提供相反的翻译，从而使绘制的图形能够正式表示CSP规范，并可以直接传递给FDR进行细化检查。作为未来的工作，我们设想提供一个面向对象的版本的Tcl/Tk脚本。这将使FDRExplorer API能够集成到FDR的GUI中。另一个有趣的想法是提供从图形符号格式到FDR LTS格式的支持。这将使人们能够将一般图（或图形模式）作为有趣的CSP过程进行细化检查。此外，通过这种具有图形符号的双向链接，可以将FDR与LTS结构上的巧妙集合理论压缩技术集成在一起，如Valmari在[21]中提出34L. Freitas，J.Woodcock/Electronic Notes in Theoretical Computer Science 187（2007）19引用[1] J. C.比克塞吉角A. R. Hoare和J.C. P·伍德考克经过验证的软件库：迈向验证器的一步。英国计算机研究大挑战，指导委员会，2004年。[2] Edmund M.放大图片作者：Clarke and Jeannette M.翼形式化方法--最新进展与未来方向。ACM Computer Surveys，28（4）：626[3] 兰斯·克里夫兰和马修·轩尼诗测试等效性作为互模拟等效性。FACJ，5（1）：1-20. Springer-Verlag，1993.[4] 列奥纳多·弗雷塔斯 模型检查马戏团。 博士论文，约克大学，2005年10月。[5] 里奥·弗雷塔斯FDRExplorer v0.3. http：//www.cs.york.ac.uk/[6] 里奥·弗雷塔斯，吉姆·伍德考克，还有安娜·卡瓦尔康蒂. 状态丰富的模型检查。软件工程的创新-NASA期刊，2（1）：49[7] 迈克尔·戈德史密斯 FDR2用户 正式系统（欧洲）有限公司，2005年6月[8] JGraph用户手册，2006年。 http://www.jgraph.com/pub/jgraphmanual.pdf。[9] 乔纳森·劳伦斯。CSP和FDR在软件设计中的实际应用。在Ali E.阿卜杜拉，克里琼斯和杰桑德斯，编辑，25年的CSP。FACJ，2004年。[10] 给了洛。CASPER用户手册 牛津大学，1997年。[11]J. M. R.马丁无死锁并发系统的设计与构造。博士论文，白金汉大学，1996年。[12] J. M. R. Martin和Y.赫达特并发系统死锁和活锁分析的并行算法通信过程架构，2000年。[13] A. W. Roscoe，P.H. B. 加德纳，M。H. Goldsmith，J.R. Hulance，D.M. Jackson和J.B. 斯卡特古德分层压缩模型检查CSP或如何检查1020个用餐哲学家的死锁。LNCS Springer-Verlag，1019（1），1995年首次TACAS。[14] A. W.罗斯科经典思维中的模型检查CSP：纪念C。A. R. 霍尔国际计算机科学系列。Prentice-Hall，1994年。第21章，第353-378页[15] A. W.罗斯科并发的理论与实践。国际计算机科学系列。Prentice-Hall，1997年。[16] 彼得·瑞安，史蒂夫·施耐德，比尔·罗斯科，迈克尔·戈德史密斯，和盖夫·洛。 安全协议的建模与分析。艾迪森·韦斯利2001年[17] J. B.斯卡特古德机器可读CSP的语义及其实现。牛津大学女王学院博士论文[18] T. 斯里瓦塔纳库用偏差技术进行安全分析。博士论文，约克大学，2005年。[19] Tcl/Tk：工具命令语言。http：//www.tcl.tk/，2006年。[20] 测试序列发生器TGV。http：//www-verimag.imag.fr/TGV[21] A.瓦尔马里第二届计算机辅助验证国际会议论文集对状态爆炸的顽固攻击LNCS 531，第156-165页。Springer-Verlag，1990.