XRT: 可扩展探索框架及其应用程序[-20字]

理论计算机科学电子笔记144（2006）3-26www.elsevier.com/locate/entcsXRT沃尔夫冈·格里斯坎普·尼古拉·蒂尔曼·沃尔夫拉姆·舒尔特微软研究院，美国雷德蒙1摘要XRT处理.NET托管程序集时，它提供了分析、重写和执行重写程序的方法。尽管XRT的状态表示允许任意的探索策略，但它特别针对事务性探索进行了优化，其中事务可能由许多指令步骤组成。XRT支持扩展，其中一个扩展是用于符号探索的模块，它捕获了安全CIL的完整域。XRT目前的应用是在测试领域，即参数化单元测试和基于模型测试的状态空间探索。 本文概述了XRT的体系结构，并概述了应用程序。关键词：XML模型检测，可扩展探索框架，混合具体/符号状态1引言近年来，模型检测在软件中的应用越来越受到人们的关注软件模型检查技术允许检测困难以发现数据竞争等错误，并验证模型和/或实现满足关键的时间属性。模型检查器发现错误的效率通常取决于应用程序域。例如，SPIN [13]在检查协议模型方面效果很好，SLAM [4]和BLAST项目是成功的，因为它们专注于设备驱动程序，VeriSoft [11]在检查某些1电子邮件：wrwg@microsoft.com，nikolait@microsoft.com，schulte@microsoft.com1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.01.0024W. Grieskamp等人/理论计算机科学电子笔记144（2006）3不能通过重新执行映射到模型检查器的输入语言的软件，而Zing [ 3 ]在检查并发面向对象抽象的细化方面是成功的。针对不同应用领域的专门化是软件模型检验成功应用的关键。然而，大多数现有的模型检查器都是单片的，即状态表示和探索高度交织在一起，输入语言是固定的。Bogor项目[17]和Java Path Finder项目[1]通过提供一个开放的框架来解决这个问题，该框架可以专门用于不同类型的应用程序域。XRT是一个新的状态探索框架，遵循与Bogor和JPF类似的目标，使用JPF开创的虚拟机级别上的执行方法它支持公共语言CIL的完全安全（可验证）的中间语言，并提供各种级别的扩展点，包括指令集，状态表示和探索策略。它从一开始就与一个特定的扩展一起开发，即不受限制地支持混合的具体/符号状态和探索，其中逻辑变量可以覆盖CIL程序中出现的所有值，包括对象和数组。XRT的开发主要是由测试领域的应用程序驱动的。与MSR [21]开发的定理证明器ZAP一起，它为MUTT提供了基础，MUTT是一个围绕单元测试技术和工具的项目，其第一个成果在[22]中描述它也是基于模型的测试工具Spec Explorer [5]的下一个版本的核心，如[12]所述本文为对技术感兴趣和知情的读者提供了XRT架构的高级概述。我们首先概述了核心体系结构，然后描述了符号探索的扩展，最后概述了当前的应用程序。补充技术材料见附录。2核心架构XRT的核心由三个主要的子系统组成，它们提供程序模型、状态表示和执行环境。 这些子系统基于严格的通用组件模型，XRT应用程序也希望使用该模型：公共功能由服务接口描述和公开，使用此功能的组件通过其服务接口类型查询实现者，确保组件可替换性。W. Grieskamp等人/理论计算机科学电子笔记144（2006）352.1程序模型XRT中的程序由程序集组成。程序集可以直接加载，也可以在程序执行期间使用标准的.NET程序集加载规则作为副程序加载。程序集的元素是惰性加载和执行的。例如，一个方法的字节码在第一次执行之前不会被加载和重写。这样，XRT就可以运行在一个大的代码库上（比如mscorlib.dll，.NET的核心程序集），而这个代码库只在动态控制流程需要的时候才被处理。MetaData程序模型以传统的方式表示元数据每个实体（包括程序集本身）上的.NET自定义属性都是可用的，这对于处理程序的检测通常很有用代码表示可执行代码的基本实体是方法体，方法体表示为控制流程图，节点是基本块。每个基本块以分支指令（指向其他块）（序列）、返回指令或展开指令结束，并具有特殊的异常退出，如果引发异常，则该异常退出指向正在执行的块。如果一个异常没有在一个特定的块上下文中处理，异常出口将指向一个只包含一个展开指令的块指令由我们称为XIL的语言表示，XIL是CIL的缩写。XIL类似于三地址代码，并对局部变量进行操作，这些局部变量来自原始程序中的局部变量和参数，以及为评估堆栈位置而引入的临时变量XIL处理安全、可验证的CIL的所有概念，包括方法、局部变量、字段和数组元素的地址指令集记录在附录A中。这里应该提到一个特殊的XIL指令，因为它提供了主要的扩展点：CALLPRIMITIVEp（l），其中p是指向某个元级代码的委托，l是序列局部变量。为了解释该指令，执行引擎调用委托，如稍后所讨论的。一种方法可以有许多不同的方法。Flavors允许在一个XRT探索会话中使用同一方法的多个代码版本重写器定义了一个指令重写器的流水线，当第一次请求给定方法的重写器时，这些重写器在方法代码的初始XIL版本上运行每个指令6W. Grieskamp等人/理论计算机科学电子笔记144（2006）3重写器获取一个方法体的控制流程图并映射到另一个方法体。在最简单的情况下，它可以只执行一些重写局部替换;更复杂的重写器可能会产生一个全新的控制图。基础结构以各种方式支持重写器。例如，在控制流程图表示的顶部提供数据流程分析框架，其允许在重写之前分析方法主体方法和类型替换指令重写的另一种方法是方法或类型替换。对于方法替换，可以提供一个元级别的委托，当方法被调用时调用它，而不是解释方法例如，它用于替换String等框架类型上的本地方法调用。通常，方法替换将使用反射调用被替换方法的本机这对于没有副作用的方法是可能的，这些方法对可以转换为原生形式的数据表示进行操作（例如，数字和字符串）。类型替换将整个类型（包括其堆表示）替换为具有兼容签名的另一个类型。这在程序模型中是透明的，即当被替换的类型或它的一个方法被查询时，替换将被传递，并且被替换的类可以是未被替换类型的基类。类型替换可以通过声明的方式完成，一个自定义属性，它声明加载类型集中的一个类型被另一个签名兼容的类型替换。当替换可以在XRT下常规执行的标准C#/.NET代码中实现时，使用此方法，例如处理本机类型实现。类型替换也可以通过调用XRT编程替换通常用于替换具有特殊意义的类型，例如.NET线程。附录B包含一个.NET框架类型System.Random的编程类型替换示例。2.2状态表示XRT的状态编码程序状态的完整快照，包括静态数据、堆和带有调用堆栈的线程。XRT区分两种状态表示。活动状态是状态的可变版本，允许完全读取和写入访问。压缩状态（在文献中也称为折叠状态）是允许快速散列和压缩的不可变版本活动状态可以通过解压缩压缩状态来获得W. Grieskamp等人/理论计算机科学电子笔记144（2006）37反之亦然。压缩在当前实现中，压缩状态被实现为分量的内部化（散列压缩）向量解压缩压缩状态的成本很低，因为最初活动状态只是对压缩状态的包装，而活动状态是从压缩状态导出的。只有当访问处于活动状态的组件时，这些组件才处于压缩状态，它们才从压缩状态中取出，解压缩，并缓存在活动状态中。例如，活动状态可以处理调用堆栈顶部的方法调用序列，其中调用堆栈的较低部分在压缩状态下保持不变。当活动状态被压缩时，将基于在活动状态中执行的改变与从其导出的压缩状态相比的增量来创建新的压缩状态压缩类似于复制GC算法，因为它遍历活动状态的可达对象图，并将可达对象重新定位到新的压缩状态。只有在这个时候，并且只有对于活动的、可到达的值，才需要计算结构共享;对于未更改的部分，它是从旧的压缩状态中接管垃圾收集和状态对称当前状态实现使用引用计数机制来检测压缩状态下的死对象，这是近似的，因为对象图中可能存在循环。引用计数只需要在压缩期间维护当计算散列码时，或者比较两个压缩状态的给定对象类型的堆时，引用计数信息用于跳过死条目。假设死对象在对所有活压缩状态的全局垃圾收集用于防止包含内化表的全局背景无限增长它还检测关于那些可以确定性排序的状态分量的对称性然而，它必须只偶尔执行，以便其成本摊销在勘探会话。需要为XRT w.r.t.做更多的增量检测对称性，并使用组件排序的算法，最有可能适应以前在这一领域所做的工作[14、20、18]）。状态扩展核心状态提供了一种插件状态扩展的方法。为此，它区分每个值的编码是在核心还是在扩展中所有对扩展值（可以是值或引用类型）的解释都被转发到状态8W. Grieskamp等人/理论计算机科学电子笔记144（2006）3扩展名. 像状态一样，扩展具有活动和压缩表示，并且核心的压缩算法调用扩展并根据需要回调。由状态扩展实现的接口比核心状态的接口更简单，这证明了自定义状态不仅仅是通过替换整个核心状态实现来实现的。特别是，状态扩展不需要处理线程、调用堆栈和位置地址，而只需要处理值和对象的表示当前状态扩展的主要应用是向XRT添加符号状态，如第3节所讨论的。2.3执行环境执行代码的基本工具是执行器组件。其中，它提供了一个方法，该方法采用活动状态并迭代活动线程的指令步进（包括调用和返回），直到命中挂起点。挂起可以由CALLPRIMITIVEp（l）指令的委托或方法替换的委托触发当被执行器调用时，这样的处理程序可以返回一个表示挂起的对象;在这种情况下，执行器将停止迭代并将挂起对象传递给其调用者，通常是探索算法。挂起和探索挂起可以充当状态探索图中的选择点它可以捕获压缩状态和传出事务的解析。（我们使用事务的概念而不是转换或步骤，以强调事务可以由许多逻辑状态转换/指令步骤组成在枚举时尚未计算暂停的交易相反，挂起为其事务提供了一种计算方法，该方法将解压缩挂起中包含的状态，并调用执行器在给定路径中继续执行，直到命中下一个挂暂停由接口类型给出，并且在一个通用探索算法中可能存在许多不同的实现XRT框架提供了表示顶级入口点方法（探索图的初始节点）的激活、线程调度挂起等的标准挂起，并且它促进了自定义挂起的创建在附录B中，我们展示了一个代码示例，其中说明了自定义挂起的实现。重新执行通常，如果挂起表示用于探索的分支点，则应解释导致挂起的指令W. Grieskamp等人/理论计算机科学电子笔记144（2006）39在不同的条件下，在每个分支中再次为此，压缩状态在每个线程的基础上提供了一个标记，让一个原语调用处理程序标记它的指令的重新执行活动状态提供有关事务和执行当前指令的相关挂起的信息当重新执行标记被设置时，它确保原始调用处理程序看到的事务属于它在第一次执行时创建的挂这样，内部状态就可以从初始执行点传递到重新执行点。附录B中的示例说明了重新执行的用法。3符号状态扩展XRT核心状态的一个扩展这允许用符号表示任意.NET类型的值。接下来，我们将概述此扩展的设计。我们称XRT加上它的符号状态扩展XRTS。术语符号值由内部化（散列consed）术语表示。有一些常用的术语表示基值、逻辑变量、对象引用、对象和数组状态、CIL的一元和二元操作、这里我们只讨论三种特殊形式的术语：类型、对象状态和域术语。整个术语语言记录在附录C中。XRTS每个术语都有一个关联的基本类型。如果基类型是引用类型，则它所表示的对象的运行时类型可能更具体，并且可以也是象征性的对象状态由所谓的字段映射表示，数组状态由所谓的元素映射表示。这两种表示都是从定理证明器社区[7]中采用的。场映射在逻辑上是一个将对象项映射到表示对象的场赋值项的函数;类似地，元素映射是一个从对象项和索引项到元素赋值项的函数字段和元素映射在语法上由一系列对初始映射值的更新定义。详情见附录C一个领域术语表示一组值。域项的构造函数是空集、单例集、范围集（用于数字）和集合并集。在XRTS中，我们使用领域术语来表示术语的成员约束例如，如果创建了一个新的逻辑变量，其基类型是引用类型，如果没有另外指定，则该变量的范围将覆盖对象引用在创建变量的状态下，该变量可用于该基类型;这一事实由域约束表示术语总是使用所谓的术语人来构建和分析10W. Grieskamp等人/理论计算机科学电子笔记144（2006）3{}{}联系我们与求解器相关联的老化器。术语管理器的默认实现执行术语的内部化和规范化（包括求解器可以通过根据需要添加进一步的规格化来覆盖此实现。求解器和假设集求解器是XRTS框架中的一个组件，其API公开了假设集的构造，假设集表示一组抽象的约束。像状态一样，假设也是压缩的积极的形式。对假设的操作包括术语简化、可满足性和包容性检查、域查询和假设拆分。这些查询中的每一个的结果都可能是不确定的。简化取一个项，并将其重写为一个更简单的项，它可能以这种方式成为基础满足性检查给定的假设集是否包容检查一个假设集是否被另一个假设集所包容（即模型集是另一个模型集的子集）。对术语域的查询处理如下。如果项的显式域约束在假设集中，则它确定项的域。否则，可以为每个复合项计算项的导出域，前提是子项具有域。例如，考虑一个表示两个具有范围约束的逻辑变量相加的项。可以计算加法项的导出域，并且其范围将从各个范围的开始之和导出域是实际域的近似，其可以进一步受到其他约束的限制术语域用于假设集分裂。分裂是相对于一个术语执行的，并导致枚举新的假设集，其中给定的术语具有更专门的域。更详细地说：如果定义域d是一个并集，那么得到的假设集将表示并集的左操作数和右操作数;如果d是一个范围，则范围将在中间分裂。例如，设t是一个布尔项，定义域为t0 1，其中0和1分别表示假和真。在t上分裂将产生两个新的假设集，一个包含t0，另一个包含t1。 对于每种情况，求解器现在都有了完整的知识，并且可以根据分割的假设集进一步简化术语。解算器可以堆叠，其中一个解算器使用基础解算器。XRTS带有一个默认的求解器实现，它支持成员约束的快速决策阳离子），并支持域和分裂，并且可以利用底层求解器进行满意度和包容检查。在这种配置中使用的底层求解器目前是ZAP [7]或ZAP [21]。如果没有W. Grieskamp等人/理论计算机科学电子笔记144（2006）311如果存在底层求解器，则默认求解器将使用有限域求解技术[16]进行满足性检查（如果适用），并作为最后手段使用全局搜索。符号状态和状态扩展符号状态由一个映射集，以及从字段和数组类型到其当前字段和元素映射的映射每个实例字段都有一个字段映射，每个值类型都有一个元素映射，但所有引用类型作为元素的数组都只有一个元素映射，以允许协方差。最初，字段和元素映射可以是空的（封闭世界），从而限制通过引用类型的逻辑变量访问字段和元素，仅在随后创建的对象上，或者它们可以由逻辑变量表示（开放世界），从而创建一个可以通过引用类型的逻辑变量访问的无界符号域符号状态可以独立于XRT核心状态而存在，因此可以在没有核心状态可用的上下文中使用符号状态连接器使用XRT的状态扩展API将核心状态连接到符号状态连接器的主要概念责任是处理压缩，以及核心状态的对象世界与符号状态的同步。对于最后一点，核心状态和连接器一起工作，以实现对象从核心状态到符号状态的迁移，保持对象例如，当对引用类型的逻辑变量执行字段更新时，迁移此更新可能会处理该变量域中的任何对象，因此我们需要将所有这些对象迁移到符号状态。相反，从象征性国家到核心国家的迁移并不总是可能的只有当符号对象是基础的，它们才能通过触发垃圾收集被带回到具体的状态。符号探索符号探索由指令重写器实现（参见.第2.1节）和自定义暂停添加到执行环境（参见第2.3节）。重写器一方面用它们的符号对应物代替某些指令，例如一元和二元运算符，是实例检查和虚拟方法地址的查找;另一方面，它在具有多个控制流出口的指令之前引入检查点XRTS例如，对于条件分支，将创建检查点，用于测试条件在当前假设集中的计算结果是真还是假;如果检查是不确定的，符号执行创建一个符号挂起。产生的事务表示分支上假设集的拆分12W. Grieskamp等人/理论计算机科学电子笔记144（2006）3条件检查点的其他实例包括类型测试、非空测试等。请注意，满足性检查仅在检查点处执行;事实上，这是在符号探索期间可以加强假设的唯一地方4电流应用我们勾勒出两个有前途的应用程序的XRT，这两个都是在测试领域，并激发了建设的框架。在过去的几年里，我们开发了一个基于模型的一致性测试工具，称为SpecExplorer [5]，现在Microsoft产品组每天都使用它来测试Windows的部分和Web服务基础设施。该工具使用模型上的状态空间探索来测试实现的一致性，无论是在线（通过从模型探索中产生测试套件）还是在线（通过将探索过程与一致性检查合并）。为了实现模型的开发，Spec Explorer对其建模语言Spec#使用了特殊的编译技术目前正在开发的下一代Spec Explorer通过XRT，我们满足了客户关于最后一点，我们已经开发了一个所谓的动作机器框架[12]，在XRTS之上实现，并强调组合方面。动作机编码状态转换系统，从抽象状态机器，状态图，场景/用例机器，到实现。作用机可以使用乘积、一致性（交替精化[2]）和作用精化的组合子来组成XRT中动作机器的实现得益于指令重写和使用符号状态作为组合的粘合剂每个动作机器运行自己的内部状态浏览器，避免了内部步骤交错的爆炸在合成中，动作机器在同步的步骤上同步，其中一个步骤由给定的动作标记为一个术语和一组假设。如果两个作用机的作用项一致，且它们的假设集在屈服替换下满足，则两个作用机的乘积机执行一步。例如，在sce- nario机器的实现中使用了指令重写。场景由C#或VB程序表示，W. Grieskamp等人/理论计算机科学电子笔记144（2006）313像常规方法调用一样调用系统的“参与者”的方法，与关于传递参数的断言和假设交织在一起。为了独立于演员的实际实现来探索场景，演员方法调用由指令重写器抽象，并由产生动作机器的相应步骤的挂起来详情参见[12]。参数化单元测试[22]扩展了当前使用封闭单元测试的行业实践，定义为无参数方法。参数化单元测试将两个关注点分开：1）它们为所有可能的测试参数指定所涉及方法的外部行为2）通过实例化参数化的单元测试，可以将测试用例重新获得为传统的封闭单元测试此外，参数化的单元测试可以被解释为所涉及的方法行为的符号摘要这些摘要作为自定义重写规则，允许符号执行扩展到任意抽象级别。在我们的原型实现中，使用XRTS下的符号探索来计算覆盖所有路径所需的参数实例化–此外，符号摘要也是通过XRTS下的探索从参数化单元测试中创建的，使用特殊的指令重写器来抽象代码ap。适当地。 对汇总方法的调用被解释为对汇总堆，调用XRTS这些条款的规则这允许使用一个非参数化单元测试在另一个模块的参数化单元测试中将模块作为公理详情参见[22]。5讨论相关的工作模型检查器，如Spin [13]或Zing [3]，使用编译方法，而不是JPF [1]，Bogor[19]和XRT，这导致了一个相当不同的架构，很难联系起来。总的来说，我们认为汇编和解释这两种方法各有利弊。解释方法的一个优点是其较低的另一方面，编译最终可能会达到更好的性能;然而，我们相信为了真正利用这种潜力，必须编译到像C或C++这样的语言，它提供了对机器模型的完全访问。JPF [1]开创了在标准虚拟机级别上进行探索的方法 由于JPF面向JVM，XRT面向JVM，14W. Grieskamp等人/理论计算机科学电子笔记144（2006）3XRT处理的内容更丰富，包括用户可定义的值类型以及引用参数和方法的地址。Bogor [19]与XRT密切相关，从一开始就致力于为状态探索提供一个可扩展的框架，而JPF最初被设计为一个显式的状态模型检查器，直到最近几年才发展成为一个通用的探索框架。Bogor和XRT共享第一设计原则，如严格的组件化架构，系统的中心模块可以通过定制实现进行交换然而，如果涉及到扩展点的细节，系统就不同了。Bogor使用自己的输入语言BIR，它提供了一种定义类型扩展的机制，这些扩展的签名在BIR中指定，其实现在某些Java模块中给出。这种扩展机制类似于XRT的编程类型替换。JPF提供了一种用另一种Java类型替换一种Java类型的方法，这类似于XRT的声明性类型替换。然而，Bogor和JPF似乎都不支持系统化的代码重写方法，如XRT的代码重写器和指令重写器流水线所给出的那样。我们的经验，指令重写是一个主要的扩展设施，我们目前的所有应用程序。Bogor以及JPF和XRT的扩展机制之间的另一个区别似乎是XRT动态计算事务长度（原子计算步骤）的能力。在XRT中，原始调用处理程序可以根据当前程序状态决定是否创建挂起/选择点。例如，在符号探索中，只有当分支条件未确定时，才会创建分支的选择点，即：求解器不能在当前上下文中将条件简化为真或在茂物，线程的事务长度由BIR固定动态计算事务的能力在动态约简技术的上下文中可以被JPF和Bogor的状态实现使用状态折叠，XRT也是如此。Collapsing随着Spin的实现而流行目前，XRTXRT的未来工作将需要解决这个问题。与检测状态对称性正交的是偏序约简[6]，它已经在具有线程和锁的面向对象并发软件的上下文中进行了研究，例如。在[10，8]中。我们在XRT中有一个完全动态偏序约简的原型，它将[9]中的工作扩展到有状态探索和任意搜索策略;然而，这个原型在发表之前需要进一步的研究。当涉及到混合具体/象征性的探索，有一个扩展，W. Grieskamp等人/理论计算机科学电子笔记144（2006）315[15]与XRTS相似的JPF，Zing的一个也在准备中然而，这些扩展并不解决对象的完全符号表示;相反，对象是枚举的，并且只有值类型可以是符号的。茂物的设计者认为，具有符号状态的茂物扩展是可取的，但可能需要重构其架构[17]。据我们所知，XRT是第一个完全混合具体/符号探索的实现，包括符号对象和数组的处理，并允许在封闭和开放的对象世界中进行探索。至少，性能基准测试是一门黑色艺术。然而，需要更多的实验数据来系统地评估XRT和XRTS的性能。在这一点上，目前的应用程序表明，XRT例如，参数化单元测试能够生成为以下各项提供路径覆盖的参数：一个相对复杂和非正交的实现，如哈希表，在30秒内有趣的场景。随着越来越多的应用程序运行在XRT之上，我们将有更多的机会来评估XRT在实际负载下的效率。未来的工作XRT需要进一步改进。一个重要的主题是增加更好的方法来检测状态对称性，另一个是巩固XRT中原型的动态偏序约简技术感兴趣的另一个领域是面向目标的启发式搜索，这是测试以及模型检查的重要性，为此，我们正在寻找基于程序切片的技术，并尝试使用我们的符号计算框架来扩展它们最后，我们目前，我们的主要重点是推动基于模型的测试和单元测试的应用程序引用[1] Java Pathology主页，http://javapathfinder.sourceforge.net/。[2] 巴 尔 河 ， T. A. Henzinger ， O. Kupferman 和 M. Vardi ， Alternating refinementrelations，in：Proceedings of the Ninth International Conference on ConcurrencyTheory（CONCUR163-178。[3] 安德鲁斯，T.，S. Qadeer，S.K. Rajamani，J. Zeroof和Y. 谢振：基于模型检验的并行软件结构开发，见：CONCUR 2004，2004。[4] 球，T。和S. K. Rajamani，SLAM项目：通过静态分析的可重构系统软件，在：POPL 2002，2002。[5] 坎 贝 尔 角 ， W. 格 里 斯 坎 普 湖 Nachmanson ， W.Schulte ， N.Tillmann 和M.Veanes，基于模型的测试面向对象的反应式系统与规范浏览器，技术报告MSR-TR-2005-59，微软研究院（2005年），提交。[6] Clarke，E.M.，O. Grumberg和D.Peled，16W. Grieskamp等人/理论计算机科学电子笔记144（2006）3[7] Detlefs，D.， G. Nelson和J.Saxe，《程序检查的定理证明器》（2003年）的报告。URL citeseer.ist.psu.edu/detlefs03simplify.html[8] Dwyer，M. B、J.Hattery. Robby和V.P. Ranganath，Exploiting object escape andlockinginformationinpartial-orderreductionforconcurrentobject-orientedprograms，Formal Methods in System Design25（2004）。[9] 弗拉纳根角和P. Godefroid ，Dynamic partial-order reduction for model checkingsoftware，在：POPL[10] 弗拉纳根角和S. Qadeer，Transactions in software model-checking，Electronic Notesin Theoretical Computer Science（2003）。[11] Godefroid，P.，软件模型检查：VeriSoft方法。[12] Grieskamp，W.和N. Tillmann，Action machines-[13] Holzmann，G.J.，“自旋模型”，Addison-Wesley，2003年。[14] 约瑟夫河，并发动态软件模型检验的对称性约简，Software Tools forTechnology Transfer（STTT）6（2004），pp. 302-319[15] Khurshid ， S. ， C. S. Pasareanu 和W.Visser ， Generalized symbolic execution formodel checking and testing ， in ： Proc.9th International Conference on Tools andAlgorithms for the Construction and Analysis of Systems，2003，pp.553-568[16] 阿索特，K。和p.J. Stuckey，[17] 马修湾Dwyer，M. H. R.，John Hatterman，Building your own software modelchecker using the bogor extensible model checking framework，in：Proceedings of the17th Conference on Computer-Aided Verification（CAV 2005），2005年。[18] Musuvathi，M.和D.Dill，增量堆规范化算法，技术报告MSR-TR-2005-37，Microsoft Research（2004）。[19] 罗比，J.H.，马修湾Dwyer，Bogor：一个可扩展的高度模块化的模型检查框架，在：欧洲软件工程会议和ACM SIGSOFT软件工程基础研讨会第四次联合会议（ESEC/FSE 2003）会议，2003年。[20] 罗比，J。H. R. 一、M. B. Dwyer，用于模型检查动态软件的空间缩减策略，在：Proc。 SoftMC03软件模型检测研讨会，2003年。[21] 测试、验证和测量，微软研究院，Zap定理证明器，http：//research.microsoft.com/tvm/网站。[22] 蒂尔曼，N.，W. Schulte和W. Grieskamp，参数化单元测试，技术报告MSR-TR-2005-64，Microsoft Research（2005），将出现在FSE 2005中。W. Grieskamp等人/理论计算机科学电子笔记144（2006）317122←22THROWlRETHROW UNWIND分支b，l？CALLINDIRECTl？ ← l2（l）返回l？一元l1<$l2二元l1<$l2<$l3呼叫原语p（l）NEWOBRAYl1，τ[l2]ISPLENCEl1←l2，τ加载量ILOADCONST I <$CLOADLOCALADDRI1<$I2LOADFIELDADDR I1<$I ？ . fLOADELEMENTADDR l1← l2[l3] ， τ？ 加 载 单 元l1<$l2[l3]存储单元l1[l2]<$l3加载方法l1<$l？. mLOADINDIRECT l1← l2存储间接l1←l2图A.1. XIL的非冗余子集AXIL图A.1介绍了XIL我们写l代表局部变量，l代表局部变量序列，l？对于在指令的上下文中可选的局部。例如，分支指令有一个可选的local;根据local的值，执行会在标签处继续如果没有局部给定，则跳跃是无条件的。我们使用c表示一个常量，m表示一个方法，f表示一个字段，τ表示一个.NET类型。⊕以及一元和二元运算的范围图A.1省略了XIL指令，这些指令也可以使用基于地址的计数器来表示：例如，加载字段的值可以通过加载字段的地址，然后在该地址上执行间接加载来表示只有在加载和存储数组元素时，才需要单独的指令来检查数组协方差。请注意，地址是表达.NET概念（如委托和引用参数）的基础。静态字段和实例字段地址的加载由相同的load-field-address指令表示，其中实例是可选的。请注意，CIL通过使用对象引用可能发生的结构地址来统一处理结构（.NET值类型）字段和对象字段，我们也为XIL进行了调整。大多数说明应该不用说，但有些需要解释。 NEWOBABYlτ创建一个原始对象;调用一个tor，它被当作一个实例方法，必须立即跟随。LOADMETHODADDRl1←l？. m使用可选l的运行时间ty pe？演出一个虚方法查找（或者如果l？ 存在但为空）;如果l？2 2如果省略，则将采用给定方法的地址。 注意到方法地址实际上只是地址，并不聚合接收方对象（.NET委托和方法地址之间没有一对一的映射 因此在18W. Grieskamp等人/理论计算机科学电子笔记144（2006）31←CA L LINDIRECTL？←l2（l）接收器必须作为第一个元素提供如果方法地址l2指向实例方法，则为l 把广告-除了通常的空解引用（null-dereference）和索引越界检查（index-out-of-boundchechks）之外，由于数组协方差，对数组元素的处理或存储数组元素执行以下检查。加载执行程序l1l2[l3]， τ？需要类型参数τ，如果数组的元素类型是引用类型。 在这种情况下，这 个 指 令 检 查 数 组 的 元 素 类 型 是 否 如 果 不 是 ， 则 引 发ArrayTypeMismatchException。STOREELEMENTl1[l2]←l3指令检查l3是否可分配给数组如果不是，则引发ArrayTypeMismatchException当由THROW指令显式地或作为另一指令的副作用引发异常时，异常对象被存储为状态中的当前异常，并且控制流程继续控制流程图中的当前块的异常退出块。指令LOADEXCEPTIONl检索当前异常对象（如果没有当前异常，则为null）并将其存储在l中。这个指令后面通常是对l的类型检查，当类型检查失败时，后面是RETHROW指令当一个方法被RETURN指令正常保留时，当前异常被重置为null如果一个方法留下UNWIND指令，则当前异常将在调用方中引发指令CALLPRIMITIVEp（l）是XIL的扩展点这里p表示委托（在XRT框架中，即在Meta级别上），其由指令步进器调用以解释该指令。与C#等源语言相比，XIL的类型系统中的简化适用;这些简化源于CIL指令与内存和计算堆栈交互的方式。像布尔型、字符型、32位以下的有符号和无符号整数都被压缩成一种类型，int32。相应地，其他基本类型被折叠成int64和double。加法之类的算术指令总是对折叠类型进行操作.原始类型的语义通过相应的扩大和收缩转换来保留。在CIL中，这些转换在加载和存储指令中大多是隐式的;在XIL中，转换总是显式指令。我们说两个类型是表示兼容的，如果它们映射到相同的折叠原语类型（int32，int64或double），或者它们都是相同XILW. Grieskamp等人/理论计算机科学电子笔记144（2006）319• 如果字段地址是从对象或结构中选择的，则此字段实际存在;• 如果加载了虚拟方法地址，则该方法实际存在;• 如果选择了元素地址，则对象实际上是一个数组;• 仅将表示兼容值从一个位置移动到另一个位置;• 如果一个方法被间接调用，那么被寻址的方法B示例：探索随机选择我们给出了一个代码示例，展示了如何在任意.NET程序中编写一个简单的随机选择资源管理器。图B.1显示了如何执行类型替换，如何编写使用重新执行的原始调用处理程序，以及如何定义自定义挂起。图B.2显示了执行简单状态空间探索的代码。该示例是完整的，并且图B.1中的RandomChoiceExplorer类派生自一个XRT类ApplicationBase，它有助于应用程序的构建。这个类提供了XRT组件的命令行解析和标准设置，由于它本身就是一个组件，因此允许使用GetRedService查询服务，以及每个组件可用的Configuration图B.1中的Setup方法执行类型替换，并返回正在探索的程序的顶级入口点在查询提供程序模型的IProgram组件之后，安装程序加载程序集。然后它对System.Random执行类型替换。在替换的System中，我们要定义的唯一方法是Random，它是int Next（intmin，intmax）。 原始方法提供一个范围为最小值到最大值的随机值。Handle方法是基本的调用处理程序，它替代System.Random.Next。它决定是否第一次执行，在这种情况下，创建一个代表随机选择的选择点的挂起。否则，它将计算当前事务中随机选择的值，并将其存储在结果参数中。transactionContext返回在其中执行此调用处理程序的上下文的事务。一笔交易是由创建它的暂停和一个标识从该暂停出去的特定交易的索引给出的。在随机选择的简单情况下，我们可以使用索引来计算结果值。20W. Grieskamp等人/理论计算机科学电子笔记144（2006）3{}个字符。}partial classRandomChoiceExplorer：ApplicationBaseIMethodImplementation Setup（）IProgram program = this. GetMyRedService IProgram>（）;IAssembly assembly =program.LoadAssemblyFrom（this.Configuration.ProgramName）;IMethodFlavor methodFlavor =program.SystemAssemblies.MSCorLibSystem. out. println（“System. out. println”）;randType.DefineMethod（“System.Random.Next（System.Int32，System.Int32）"，methodFlavor，newPrimitiveCall. Threshold（this.Handle））;return assembly.EntryPoint.GetImplementation（methodFlavor）;}Isuspension Handle