Java PathExplorer：程序验证和自动化测试工具的发展

网址：http://www.elsevie r. n l/l oc ate/en tcs/vol um e55. ht ml 18页使用Java PathExplorerKlaus Havelund1，Grigore Rosu21Kestrel技术2高级计算机科学研究所http://ase.arc.nasa.gov/美国宇航局艾姆斯研究中心，加利福尼亚州，94035摘要我们目前的Java PathExplorer（JPaX），用于监视Java程序的执行工具的发展最近的工作 JPaX可以在程序测试期间使用，以获得有关程序执行的更多信息，并且可以在操作期间进一步应用于调查安全关键系统。 该工具有助于程序字节码的自动化检测，然后在执行过程中向观察者发出事件。观察者检查事件对用户提供的高层次的需求规格，例如时序逻辑公式，并对较低层次的错误检测程序，通常并发相关的，如死锁和数据竞争算法。用Maude重写逻辑来定义高层需求规格说明及其底层逻辑，然后用Maude重写引擎直接检查，或先转换成有效的数据结构，再用Java检查。1介绍软件的正确性在我们社会的许多部门中正成为一个越来越重要的问题。人们的生活往往依赖于软件系统，即使他们往往没有意识到这一点。大多数技术实验的成功，包括航天器和航天机构内的漫游者技术，在很大程度上取决于软件的正确性。人们普遍认为，未来的航天器将变得高度自主，在没有地面通信的情况下做出决定，因此所需的软件变得更加复杂，增加了任务失败的风险。解决软件正确性这一微妙问题的两种常用方法是程序综合和程序验证，前者给出了高度的置信度，但似乎只适用于非常有限的特定领域问题，后者则关注于检测现有程序中尽可能多的错误c2001年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。2程序验证的两个重要方面是测试和形式化方法的使用。然而，传统的测试技术是非常特别的，并且不允许系统需要满足的高级逻辑特性的正式规范和验证。另一方面，传统的形式化方法，如模型检测和定理证明通常是非常繁重的，很少能成功地在实践中使用，没有大量的手工劳动。NASA艾姆斯研究中心的自动化软件工程小组在程序综合[14，5，19]和程序验证[8，9，18，7，11]两个领域研究了确保软件正确性的高级形式化方法已有一段时间。这里不讨论程序合成，但值得注意的是，从逻辑形式、suchanitestatemachines、Buch自动机或动态程序设计算法中的C语言是程序验证中常用的一种我们已经使用形式化技术（特别是模型检查）进行了各种验证案例研究，以分析航天器软件[8]。此外，还开发了两个模型检查器，它们都支持使用显式状态模型检查技术对Java程序进行完整的状态空间探索[9，18]。这些技术允许证明具有几百万个状态的程序的时序逻辑属性，但不能应用于大型程序。本文是继[10，16，11]之后的第四篇文章，描述了我们在运行时验证方面的工作，可以粗略地定义为将测试和形式化方法相结合。测试具有很好的伸缩性，并且是目前为止在实践中最常用的验证软件系统的技术。测试和时序逻辑规范的合并是为了实现这两种方法的好处，同时避免了一些特设测试的陷阱和定理证明和模型检查的复杂性。在本文中，我们提出了一个新的运行时验证系统，称为Java路径浏览器（JPaX），通过分析（探索）特定的执行轨迹来监视Java程序的当前状态。一般的思想包括从执行的程序中提取状态事件，然后通过远程观察者进程分析它们观测器执行两种验证，即基于逻辑的监测和错误模式分析。基于逻辑的监控包括检查执行程序上的正式需求规范，由系统用户以高级逻辑编写。逻辑目前在Maude [2]中实现，Maude是一个支持重写逻辑和成员关系方程逻辑的高性能系统。在Maude中，人们可以非常自然和容易地定义新的逻辑，例如时态逻辑，以及它们的操作语义。目前，JPaX支持两种内置逻辑，未来时间和过去时间线性时态逻辑。在Maude中实现这两个逻辑以及一个处理原子命题的基础结构模块，这些命题很可能是任何其他更一般逻辑的一部分，覆盖不到130行。因此，对于高级用户来说，定义新的逻辑应该是非常可行的。的当前版本3Maude可以在800Mhz处理器上每秒进行多达300万次重写，其编译版本旨在支持每秒1500万次重写。因此，我们决定使用Maude作为逻辑监视引擎，在JPaX的早期阶段，它根据规范执行事件的一致性检查。错误模式分析包括使用各种错误检测算法来分析事件的一个执行跟踪，这些错误检测算法可以识别容易出错的编程实践，例如可能导致数据竞争和/或死锁的不健康的锁定规则。这些算法的重要和吸引人的方面是，即使在错误没有显式地发生在检查的执行跟踪的情况下，它们也会发现错误的可能性。它们通常是快速和可扩展的，并且经常捕捉它们被设计为捕捉的问题，也就是说，运行选择中的随机性似乎并不意味着分析结果中的类似随机性。在JPaX中已经实现了两种关注并发错误的已知算法，一种用于死锁，另一种用于数据竞争，但是系统被设计成用户可以相对容易地附加新的这种算法。在程序测试中使用时态逻辑的想法并不新鲜，据我们所知，已经在商业Temporal Rover工具（TR）[4]和MaC工具[13]中进行了研究。TR允许用户指定未来时间时态公式作为程序中的注释，然后在编译之前将其翻译为适当的Java代码。MaC工具在精神上更接近我们在本文中描述的内容，除了它的规范语言是固定的，与Maude语言相比非常有限，并且不支持错误模式分析。另一方面，像可视化线程[6，17]这样的工具包含硬连线的错误模式分析算法，因此用户不可能更改或扩展由于被监视程序和观测服务器的编程语言不需要相同，因此最终系统应该允许监视由以不同编程语言编写的子程序组成的程序，所述不同编程语言还包括C++和C。然而，为了简单起见，本文中描述的系统将只关注Java。一个案例研究的90,000行的C++代码的流动站控制器已进行，导致检测的死锁与最小量的eort。主要设计目标之一是使系统尽可能通用和通用，允许处理多语言系统和新的验证规则被定义，甚至使用Maude定义新的规范逻辑。我们的希望是使JPaX成为实验的基础，而不是一个固定的系统。本文的结构如下。第2节给出了JPaX的概述。第3节描述了编写需求规范的基本逻辑形式，而第4节描述了调试并发程序的一些错误检测最后，第5节包含结论和对未来工作的描述。42JPaX概述JPaX可以被看作由三个主要模块组成：一个instrumentation模块、一个observer模块和一个通过观察到的事件流将它们联系在一起的互连模块（参见图1）。该检测模块执行一个脚本驱动的自动检测程序进行观察。被插装的程序在运行时将向互连模块发出相关事件，互连模块进一步将它们传输到观察模块。观察者可以在不同的计算机上运行，在这种情况下，事件通过套接字传输。因此，JPaX的输入包括对两个实体的引用：要监视的字节码格式的Java程序（使用标准Java编译器创建）和定义所请求的验证类型的规范脚本。输出是一组（可能是空的）警告，打印在一个特殊的屏幕上。规格仪器验证Java程序编译观察员僵局达塔拉切仪器LTLMaude. . .执行（JVM）Fig. 1. JPaX概述更具体地说，规范脚本定义了应该激活哪种（如果有的话）错误模式检测算法，以及应该执行哪种（如果有的话）基于逻辑的监控，以及在这种情况下的要求是什么对于基于逻辑的监控，我们受到MaC语言框架[13]的启发，并将规范分为检测脚本和验证脚本。验证脚本识别要检查事件的高级需求规范。这些规范中的命题是抽象的布尔代数，因此不直接引用具体程序中的实体。指令脚本在具体的布尔程序谓词和抽象命题之间建立这种联系。如[13]所述，这种分层方法的优点是可以在不考虑低层次问题的情况下创建需求规范，甚至可以在构建程序之前创建目前，脚本是用Java编写的。因此，可以使用高级Java语言构造来定义布尔值插装字节码字节码事件流调度员5要观察的谓词。Java字节码插装是使用Compaq强大的Jtrek Java字节码工程工具[3]执行Jtrek可以轻松读取Java类les（字节码les），并在检查其内容时将其作为抽象语法树遍历，并插入新代码。插入的代码可以访问各种运行时数据结构的内容，例如调用时堆栈，并且在最终执行时将向观察者发出观察者接收事件并将其分派给一组观察者规则，每个规则执行在验证脚本中请求的特定分析。通常，这种基于模块化规则的设计允许用户在不干扰遗留代码的情况下容易地定义新的运行时验证过程。观察者规则是用Java编写的，但可以调用用其他语言编写的程序，例如Maude。Maude在高级需求规格说明中起着Maude重写引擎可以以两种不同的方式使用：在程序执行期间作为监控引擎，或者在执行之前作为翻译引擎。在前一种情况下，执行事件被提交给Maude程序，Maude程序反过来根据需求规范对它们进行评估。在后一种情况下，规范被转换为最适合程序监视的数据结构，然后将其发送回Java，并在Java程序中用于检查执行期间的事件JPaX构建在一个名为PathExplorer（PaX）的通用环境上，该环境仅由互连模块和观察者模块组成目标是通过仅提供语言规范模块，使得可以监视其他编程语言（例如C和C++）的程序这样的实验是与美国宇航局艾姆斯机器人小组的成员Rich Washington合作进行的实验只是激活了死锁检测规则，并定位了应用程序中尚未通过测试发现的死锁可能性3基于逻辑的监控基于逻辑的监视包括根据用户提供的以某种逻辑编写的需求规范检查执行事件，通常是以状态作为模型的断言逻辑，或者以跟踪作为模型的时态逻辑。JPaX允许用户使用Maude代数规范语言以灵活的方式定义新的逻辑。Maude [2]是一个模块化的规范和验证系统，它非常有效地实现了重写逻辑。一个Maude模块由操作符声明，以及与操作符和通用量化变量相关的方程组成。 模块可以组合。重写逻辑的行为就像一个通用逻辑，在这个意义上，其他逻辑，或者更准确地说，它们的语法和操作，6语义，可以在重写逻辑中实现。JPaX目前提供线性时态逻辑，包括未来时间和过去时间，作为内置逻辑。请注意，多个逻辑可以并行使用，因此每个属性都可以用最合适的语言表示。由于当前逻辑的Maude实现非常紧凑，我们将它们包括在下面。当我们给出例子时，将在y”3.1命题演算我们从下面的命题演算模块开始，这是JPaX中大量使用的，因为大多数逻辑都基于它。它实现了Hsiang [12]提出的一个有效程序来确定命题的有效性：fmod PROP-CALC是exFORMULA。* 构造函数 ** 派生运算符 *op_\/_：公式公式->公式。op_/\_：公式公式->公式[asynchronous]。op_++_：公式公式->公式[asshopping]。变量X Y Z：公式。var As*：AtomState*. 等式true/\X = X。eq false/\X = false。op _->_：公式公式->公式。op _<->_：公式公式->公式。OP！_公式->公式。等式X1/Y =（X/Y）++ X ++ Y。eq！X = true ++ X。等式X-> Y =真++ X ++（X/\Y）。等式X<-> Y = true ++ X ++ Y。eq false ++ X = X。等式X ++ X =假。等式X/|X = X。等式X/I（Y ++ Z）=（X/IY）++（X/IZ）。* 语义等式（X/\Y）{As*}=X{As*}/\Y{As*}。等式（X++ Y）{As*}= X{As*}++ Y{As*}endfm模块FORMULA，这是扩展（进口），定义的基础设施，为所有的用户定义的逻辑。这将在随后的章节中进一步描述现在，它可以说它包括一些指定的基本排序（或类型），例如语法公式的公式;公式数据结构的公式DS，当比公式本身更多的信息应该被保留用于下一个转换时，如在过去时间LTL的情况下;原子的原子，或状态变量，在状态中表示布尔值;原子状态用于将布尔值分配给原子，以及原子状态 *用于这种分配与nal分配，即，跟踪结束之后的那些，需要一个特殊的评估，如在未来时间和过去时间LTL部分中所描述的（我们对执行跟踪结束的语义是一个不改变状态的连续进程）。在某个程序状态下保持的命题是从执行的插装程序中生成的 也许由模块FORMULA提供的最重要的操作是操作fg：FormulaDS AtomState -> FormulaDS，当在程序执行期间发生（抽象）状态变化时，该操作更新公式数据结构。 注意，在命题演算的情况下，这个更新操作基本上是评估新状态中的命题（最后两行）。用户可以像上面的模块一样自由扩展所有这些类型和操作运算符在op和ops（当引入多个运算符时）符号之后引入运算符可以被赋予方括号中的属性7例如结合性和交换性。在var和vars符号之后引入了方程中使用的通用量化变量。最后，在eq符号之后引入规格说明显示了Maude灵活的mix- x表示法，使用下划线保留参数，它允许我们以最自然的方式定义逻辑的语法3.2未来时间LTL我们提出的第一个监控逻辑是建立在命题逻辑上的，是未来时间LTL的一个变体[15]。 Future Time LTL是一种以执行轨迹为模型的逻辑，便 于 程 序 监 控 。 LTL 提 供 了 运 算 符 suchaX （ al-waysX ） ， X（eventuallyX），X（nextX）和X[Y（XuntilY），以及它们与标准命题运算符的组合在形式化方法的文献中，涉及到模型检验和定理证明等问题然而，在测试环境中，跟踪是不可能的：被监视的程序迟早会被停止，因此它的执行跟踪也会停止。因此，操作语义必须考虑这一点。未来的LTL可以比我们最初在命题演算上想象的更容易实现fmod FT-LTL是来自PROP-CALC。我不知道op []_ ： 公 式 -> 公 式 。op<>_ ： 公 式 -> 公 式 。 opo_：公式->公式。op _U_：公式公式->公式。***语义学 *变量X Y：公式。var As：AtomState.int [] X {\displaystyle x}=（[] X）/\X{As}。int x<（X）{x}=（<>X）\/X{As}。eq（o X）{As} = X。等式（X U Y）{As}= Y{As}\/（X{As}/\（X UY））。int[] X {\displaystyle x}= X{As *}。Eq（> X）{As *}= X{As *}。等式（oX）{As *}= X{As *}。等式（X U Y）{As *}= Y{As*}。endfm四个LTL运算符使用符号添加到命题演算的运算符中：[]（总是），<>（最终），o（下一个）和U（直到）。这些操作符的操作语义基于公式转换思想，并由8条规则定义，分为两组，均为来自FORMULA模块的操作符fg：FormulaDSAtomState-> FormulaDS。请注意，在未来的时间LTL情况下，公式本身被用作数据结构（公式是公式DS的子类）。这个运算符定义了一个公式如何被一个状态变化（一个新的状态）的发生所转换，并在命题叶上求值。f g运算符背后的直觉可以详细阐述如下。 假设一个公式X，我们想要在第一个状态为As的执行跟踪上保持。然后方程Xf As g= X'，其中X'是通过将fg运算符应用于X（和As）而得到的公式，具有以下直觉：为了使X保持在迹的其余部分上，给定迹中的第一状态是As，则X'必须保持在As“之后的迹上。第一组规则描述了这种语义，假设状态As不是跟踪中的最后一个状态，而最后四个规则适用于状态As是跟踪中的最后一个状态。 术语As *8表示轨迹中的最后一个状态，并且反映了以下直觉：夜间轨迹可以被认为是夜间轨迹，其中，夜间跟踪在夜间重复。每个运算符的两个规则实现了以下简单的等价：s_tj='itj='fsgs_endj='i'f sg=true;其中s_t是由状态s后跟非空跟踪t形成的跟踪，s_end是由s后跟跟踪结束（nite跟踪中的最后一个状态）组成的跟踪作为一个例子，考虑公式[]（X->>Y）和一个跟踪，其中第一个状态As使X为真，但Y为假。在这种情况下[]（X-><>Y）f As g =[]（X-><>Y）^<>Y（模命题演算重写）。这反映了这样的事实，即在状态改变之后，除了原始的always{公式之外，<>Y现在必须在剩余的跟踪上为真。文[10]给出了该算法的正确性证明。尽管它的总体指数复杂度，该算法往往是相当可接受的，在实际情况中。在使用JPaX进行的全球具体实验中，我们没有注意到这个简单的8规则算法与Dimitra Giannakopoulou开发的基于自动机的算法之间有任何显著差异，后者在1，400行Java代码中实现。chi自动机启发的算法，适用于nitetraceLTL（见3.4小节）。然而，用于程序监控的LTL的这种nite跟踪语义具有一些看起来不自然的特征。在执行跟踪结束时，当被观察的程序终止时，观察者需要对检查的属性的有效性做出决定。让我们再次考虑公式[]（p->>q）。如果在被监控的执行过程中，每个p后面都至少有一个q，那么在某种程度上，我们可以说这个公式是满足的;尽管我们应该意识到这不是一个确定的答案，因为如果程序没有被停止，这个公式在未来可能会被很好地违反。如果p是真的，后面没有q，那么可以说这个公式被违反了，但它如果让程序继续执行，可能会非常满意。此外，在执行过程中，每个p后面都可能有一个q，只是最后一个p被违反了，在这种情况下，如果我们强行终止程序，我们可能会期望程序是正确的。 当然还有LTL属性，在监控过程中给予用户绝对的信心。例如，违反安全属性反映了被监视程序的明显不当行为。我们从LTL监测实验中吸取的教训是双重的。首先，我们了解到，与模型检查或定理证明不同，LTL公式，特别是它们的违规或满足必须用额外的信息来查看，例如公式在执行跟踪中的“执行情况”的统计数据。第二，我们形成了一种信念，9LTL可能不是基于逻辑的监控的最合适的形式主义;其他更具体的逻辑，如实时LTL，间隔逻辑，过去的时间LTL，甚至未发现的，可能比纯LTL更感兴趣。在下一小节中，我们将描述过去时间LTL在Maude中的实现，这可能是一种更自然的运行时监控逻辑。3.3过去时间LTL过去的时间LTL是有用的，特别是安全性能。这些属性非常适合于基于逻辑的监控，因为它们只涉及过去，因此它们的值在沿着轨迹的任何状态中总是真或假，并且永远不会像在未来时间LTL中那样被确定。然而，令人惊讶的是，过去时间LTL的实现比未来时间LTL的上述实现稍微繁琐。它也是建立在命题演算之上的，通过添加两个常用的过去时间运算符，~表示previous，S表示since，然后是适当的数据结构和语义。该实现与[13]中使用的实现类似（根据私人通信），它也使用了过去时间逻辑的版本。我们在这里介绍过去的时间逻辑模块，然后给出一个逐步的解释。fmod PT-LTL是ex PROP-CALC。我不知道OP ~_公式->公式。op _S_：公式公式->公式。* 语义数据结构 *op ptLtl：公式->公式DS。op原子：Atom Bool -> FormulaDS。上一页：FormulaDS布尔-> FormulaDS。OP和：FormulaDS FormulaDS Bool -> FormulaDS。op xor：FormulaDS FormulaDS Bool -> FormulaDS。OP since：FormulaDS FormulaDS Bool -> FormulaDS.var A：Atom.var As：AtomState. varB：Bool.变量X Y：公式。变量D D' Dx Dx' Dy Dy'：公式DS。eq [atom（A，B）]= B。eq [prev（D，B）]= B。eq [since（Dx，Dy，B）]= B。eq [and（Dx，Dy，B）]= B.eq [xor（Dx，Dy，B）]= B。eq ptLtl（true）{As}=true。eq ptLtl（false）{As}= false。等式ptLtl（A）{As}=atom（A，（A{As}==true））. eq ptLtl（~ X）{As}= false。ceq ptLtl（X S Y）{As}=since（Dx，Dy，[Dy]）ifDx：= ptLtl（X）{As}/\Dy：= ptLtl（Y）{As}。ceq ptLtl（X/| Y）{As}=and（Dx，Dy，[Dx] and[Dy]）如果Dx：= ptLtl（X）{As}/\Dy：= ptLtl（Y）{As}。ceq ptLtl（X++ Y）{As}= xor（Dx，Dy，[Dx] xor[Dy]）如果Dx：= ptLtl（X）{As}/\Dy：= ptLtl（Y）{As}。***语义学 *EQ原子（A，B）{As}=atom（A，（A{As}== true））.等式prev（D，B）{As}= prev（D{As}，[D]）。ceq since（Dx，Dy，B）{As}=since（Dx '，Dy'，[Dy ']或B和[Dx]）如果Dx'：=Dx{As}/\Dy'：=Dy{As}。ceq和（Dx，Dy，B）{As}=和（Dx '，Dy'，[Dx ']和[Dy']）如果Dx'：=Dx{As}/\Dy'：=Dy{As}。ceq xor（Dx，Dy，B）{As}= xor（Dx'，Dy'，[Dx '] xor [Dy']）如果Dx'：=Dx{As}/\Dy'：=Dy{As}。10endfm模块rst介绍了逻辑的语法，previous{操作符和since{操作符。接下来的两个部分介绍了过去时间LTL公式所需的语义数据结构及其语义。数据结构由FORMULA模块中引入的排序FormulaDS表示，并且需要在执行期间表示公式这11与未来时间LTL相反，在未来时间LTL中，公式表示其自身，并且通过将公式转换为必须保持在迹的其余部分上的新公式来执行由状态转换引起的转换。 在过去的LTL中，这种技术不适用。相反，对于每个公式，引入了一个特殊的树状数据结构，它跟踪公式在前一个状态下的所有子公式的布尔值。 这些值用于在下一个状态中正确计 算 整个公式的 值 。 操 作 ptLtl/ 创 建 表示公式的 数 据 结 构 。FormulaDS类型的构造函数对应于不同种类的过去时间LTL运算符：atom（用于原子命题），and，xor，prev和since。因此，例如，对于某个原子命题A的公式~ A（previousA），在A在当前状态下为真，但在先前状态下为假的示例情况下，由prev（atom（A，true），false）表示。 因此，第二个布尔参数表示公式的当前值，并由[]操作返回。从公式创建初始数据结构的ptLtl操作是通过等式来定义 的， 该 等式还 定 义 了对初始原子状态的操 作 ： FormulaDSAtomState-> FormulaDS。因此，这定义了如何初始化公式的数据结构。请注意，此操作现在应用于公式的数据结构。 三个二元运算符（since、and和xor）的方程是使用条件方程（ceq）定义的。 条件在if关键字之后提供，并引入方程中使用的新变量。3.4高效的观察者生成基于逻辑的监视会给程序的正常执行增加开销。由于许多逻辑的有效性问题具有很高的复杂性，因此设计和实现非有效性算法是非常容易的。我们特意决定，在JPaX的早期阶段，更重要的是将我们的精力集中在设计和试验更有表现力和更自然的逻辑来进行监控，而不是为特定的逻辑实现非常有效的算法，这些算法可能很快就会被证明不是最合适的。然而，由于LTL似乎是一个很好的候选逻辑，我们开始研究有效的运行时公式验证算法的未来时间和过去的时间LTL。更确切地说，我们正在寻找从公式中生成有效观察者的算法（Java）代码或数据结构，“编码”公式，可以与观察到的程序同步执行或修改，当公式被违反时返回适当的消息。在对LTL [10，16，11]的运行时验证算法进行试验后，每个算法都有其优点和缺点，我们意识到，为了正确地比较这些算法，首先需要理解并建立标准，“良好”的运行时验证算法。考虑一个固定逻辑。 以下是当前影响JPaX中运行时算法选择的优先级列表：12前瞻设计。向后访问执行跟踪的算法涉及存储跟踪，并且在违反公式时不能抛出异常或引导你的智慧。一个算法是指数的痕迹的大小是不可用的，而一个算法是指数的公式的大小是可用的，但最好避免。- 是的从公式生成代码或数据结构所需的时间不能忽略，但它被认为不如前面的标准重要。盲目实现语义的用于未来时间LTL的平凡重写算法是立即的（也参见[10]），但是它在迹的大小上是指数的，所以它是不切实际的。第3.2小节中所示的简单而优雅的过程在[10]中被证明是正确的，最坏情况下仅在公式的大小上是指数的到目前为止，我们发现它在实践中非常好，而且它只需要几行Maude代码就可以实现，这使得它在JPaX的初期阶段是一个非常好的选择。由未来时间LTL公式[16]时间复杂度为O（nm），其中n是轨迹的大小，m是轨迹的大小公式不幸的是，这些算法向后访问执行跟踪，所以它们不能满足rst标准。 幸运的是，同样的想法也适用于过去的时间LTL，并通过对偶化，产生相同复杂度的前向算法。因此，过去时间LTL是一个非常好的可计算的监控逻辑。此外，它表达安全要求的自然性使我们相信它是比未来时间LTL更好的选择。然而，我们接下来非常简要地提出了一些概念，导致未来的时间nite-trace LTL公式检查算法，这是我们所知道的满足上述标准它向前访问执行跟踪，最坏情况下的运行时复杂度是O（nk），其中n是跟踪的长度，k是公式的变量数。完整的细节以及最优性证明将很快出现在其他地方。我们首先介绍一些编码公式所需的数据结构。直观地说，二叉转换树是一棵二叉树，其中节点是原子命题，而叶子是状态或真值。为了简化编写，我们使用一个类似C/Java的操作符？：有典型的i在学费：a？t1 ：t2 表示\ifathent1 否则t2“。例如，如果P=fa;b;cg是一组“原子命题”，S=f1;2;3 g是一组“国”，则a？（b？1：2）：1和a？（c？2：false）：（c？true：（b？3：1））都是良型hP吗？Si-二叉转移树。 下面我们给出一个简洁的形式定义，不耐烦的读者可以跳过它。设Bool为集合ftrue;false g，并考虑两种分别用于命题和状态的 P r o p 和 S t a t e 。定义3.1给定集合P：Prop和S：State，分别，那么hP？我-13二叉转移树（或简称hP？S-BTT或甚至BTT）是有序自由代数T（P;S[Bool]）在由Prop、State和BTT类组成的签名上的BTT类项，其中State是BTT的子类，并且运算1 （怎么样？：）：道具BTTBTT！BTT。 如果S为空，则hP？i-BTT被称为P-二叉决策树（或简称P-BDT或BDT;参见[1]）。如果BTT的大小成为一个重要问题，那么可以改变这一点定义利用子树的重复，从而获得有向非循环图而不是树，就像二叉决策图的情况一样（例如参见[1]）。然而，BTT的大小似乎并不重要，因为它不影响上述三个标准中的任何一个。定义3.2 BTT nite状态机（或简称BTT FSM）由集合P和S以及将S中的每个元素映射到h P？S i-BTT。BTT nite trace FSM是BTT FSM连同将S中的每个元素映射到P-BDT中的总函数end。函数end决定当跟踪结束时状态是否接受接下来应该定义“接受执行”跟踪的概念，但空间不允许我们进入更正式的方面。 我们只展示了LTL公式（a！b）可以被编码为BTT nite trace FSM：在这种情况下，P=fa;bg，S=f1;2 g，next（1）=a？（b？1：2）：1，end（1）=a？（b？true：false）：true，next（2）= b？1：2，end（2）= b？true：false。这种数据结构的直观性如下。如果被监视的程序，比如P，处于一个不是被观察轨迹的结束的状态，那么：如果观察者处于状态1然后在P的当前状态下评估原子命题a，如果这是如果为真，则评估b，如果为假，则将观察者的状态改变为2;如果观察者处于状态2，则仅评估b，如果为真，则将观察者状态改变为1。如果决定停止对P的监测，则类似地评估结束BDT。请注意，当执行跟踪中出现a而后面没有b时，将返回false。读者可能已经注意到，我们特别注意了原子命题的求值：它们只在需要时才被求值。这是因为求值过程通常很长;例如，原子命题可以测试数组是否排序。我们在Maude中设计并实现了（不到200行代码）一个相对简单和优雅的过程，可以生成最佳BTTnite跟踪FSM从任何LTL公式。尽管它的最坏情况下的指数复杂性，它是相当快的典型公式，它从来没有需要超过30秒（在400 MHz笔记本电脑上）生成最佳数据结构;仅在手工制作的人工公式上需要1秒以上。这个初始化时间只在监视开始时花费一次。以下是最佳BTT的几个示例 夜迹Nite状态机1用mix- x表示法编写。14是吗？（b？1：2）：1b？一比二121111下一个状态由我们当前的实现生成：式一（一）a_： a）（a！b）、aU（ bU c）1端是吗？true：false true是吗？（b？true：false）：true b？true：falsec？true：（a？1：（b？2：false））c？true：false2c？true：（b？2：false）c？true：false请注意，如果没有统计分析，活性属性在nite trace LTL中实际上没有意义特别地，当且仅当a在被监视程序的最后观察状态中为假时，违反公式a公式（a_：a）在nite trace LTL中总是成立的，我们的最优生成器证明了这一点。4错误模式分析基于逻辑的执行跟踪分析可以揭示特定领域的高级错误，但它意味着在设计应用程序要求或/和它们的底层逻辑时需要人为干预。然而，许多错误都是低级的，通常是由于糟糕的编程实践或缺乏注意力造成的，而且其中一部分有趣的错误可以自动显示出来。即使这些错误模式中的一些可以使用适当的需求形式主义来指定，然后使用与上面相同的基于逻辑的方法来执行，我们认为这个过程对于这种错误来说太重了，实际上，允许用户将指定的高效算法附加到JPaX上更合适。我们已经用Maude和Java实现了下面描述的算法，但是当前的JPaX使用Java实现。错误模式运行时分析算法探索执行跟踪并检测错误可能性。这些算法的重要和吸引人的方面是，即使在错误没有明确发生在检查的执行跟踪的情况下，他们ND错误的可能性。它们通常是快速和可扩展的，并且经常捕获它们被设计为捕获的问题，也就是说，运行选择中的随机性似乎并不意味着分析结果中的类似随机性。交易o是，他们有较少的覆盖面比重量级的正式方法，并经常提出的问题，经过仔细的语义分析，原来不是错误。JPaX中已经实现了两个关注并发错误的算法：Eraser [17]数据竞争分析算法和基于分析锁周期的死锁分析算法。这两种算法都是15以前由Compaq在Visual Threads工具中实现，用于C和C++。受VisualThreads工具的启发，我们之前还在Java Pathworld中实现了数据竞争算法和死锁算法的变体[7]，修改了[18]中描述的Java虚拟机。我们在JPaX的错误模式分析的贡献是使这些算法的Java使用字节码仪器，将它们与基于逻辑的监控，并允许高级用户以灵活的方式编程新的错误模式分析规则。本节的其余部分将简要介绍数据争用和死锁检测算法。4.1数据竞争分析我们在这里简要描述了在并发编程中如何容易发生数据竞争，以及如何在JPaX中实现Eraser [17]以在Java程序上工作当两个或多个并发线程访问一个共享变量，至少有一个访问是写，并且线程没有使用显式机制来防止访问同时发生时，就会发生数据竞争。Eraser算法通过研究被监控程序的单个执行轨迹来检测数据竞争，试图推断是否存在可能存在数据竞争的有效运行。我们用下面的例子来说明数据竞争分析。1. class Value{2.int x= 1; 3.4.public void add（Value v）{x= x+ v.get（）;} 5.6.public int findDuplicate（）{findDuplicate;} 个文件夹8.9. class Thread {10.价值v1;价值v2; 11.12.public void run（String s，String s）{13.this.v1= v1; this.v2= v2;14.this.start（）;15.16.17.public void run（）{v1.add（v2）;}18. 19.20. 类主{21.公共静态空main（String[] args）{22.Value v1= new Value（）; Value v2= new Value（）;23.new Task（v1，v2）; new Task（v2，v1）;24.}25. 个文件夹Value类包含一个整数变量x，一个通过添加另一个Value变量的内容来更新x的同步方法add，以及一个仅返回x值的非同步方法get。Task是一个线程类：它的实例是用start方法启动的，start方法执行用户定义的run方法。在Main中，在Value类的两个实例v1和v2上启动了两个这样的任务。当在Eraser选项打开的情况下运行JPaX时，会发现潜在的数据竞争，报告第4行和第6行中的两个线程在无保护的情况下访问了Value类中的变量x16分别生成的警告消息给出了可能出现数据争用的场景，总结如下。一个Task线程可以调用带有参数Valueobjectv2的对象v1上的add方法，其内容因此通过非同步的get方法读取另一个线程可以同时做同样的事情，即，在v2上调用add方法。因此，v2的内容可以由两个线程同时访问实际上会发出两个数据争用警告，因为另一个任务可以在v1和v2互换的情况下执行相同的行为。粗略地说，该算法在JPaX中的工作原理和实现如下。当变量被读取或更新时，以及当由于执行Java的同步语句或从同步方法调用/返回而获得或释放锁时，被监视程序的仪表化字节码向观察者发出适当的事件观察者维护两个数据结构：一个线程映射，它跟踪每个线程拥有的所有锁;一个变量映射，它将每个（共享）变量与过去所有访问线程共同拥有的锁集合的交集相关联。如果该集合变为空，则存在潜在的数据竞争。更准确地说，当变量第一次被访问时，访问线程在那一刻拥有的锁存储在变量的变量集中。其他线程的后续访问导致该集合被重新绑定到与这些线程所拥有的锁的交集。一个额外的状态机也为每个变量维护，以跟踪有多少线程访问了该变量以及如何访问（读/写）。这用于减少错误警告的数量，例如变量由单个线程初始化而没有锁（这是安全的），或者几个线程只在初始化后读取变量（这也是安全的）。死锁检测死锁的可能性通常很难发现，但是当多个线程以不同的顺序获取锁时，会发生经典例如，如果一个线程获得了一个锁，然后在没有释放它的情况下又获得了另一个锁，而另一个线程首先获得了第二个锁，然后又获得了第一个锁，那么就会出现死锁。在前面的Java示例中，如果错误地试图通过将第6行中的get方法也定义为synchronized来修复数据竞争，则可以简单地创建这样的情况：6. public int findDuplicate（）{现在很清楚，数据竞争算法将不再返回警告，因为变量x不再能从两个线程同时访问。然而，现在有一个死锁的可能性，JPaX检测到了它。更确切地说，当在修改后的程序上运行JPaX时，发现了一个锁顺序问题，并发出了一个适当的警告消息，总结了两个Task线程以不同的顺序获取Value它还指出线程可能死锁的行号：第4行，调用get方法的17add可以锁定第二对象。请注意，不需要在已检查的跟踪中出现此死锁，就可以发出此警告。事实上，即使死锁永远不会