自动生成合理的Java组件环境的方法

理论计算机科学电子笔记253（2009）145-160www.elsevier.com/locate/entcsJava组件合理环境的自动构建Pavel Parizek，Jiri Adamek，Tomas Kalibera分布式系统研究组布拉格查尔斯大学软件工程系{parizek，adamek，kalibera}@dsrg.m.cuni.cz摘要在软件组件验证中，其中一个挑战是隔离组件的模型检查。孤立组件的环境是未知的，因此模型检查器的部分输入丢失。这个问题可以通过自动生成人工环境来解决-组件及其环境形成一个完整的程序，可以使用通用模型检查器进行验证针对Java组件中的并发错误，我们提出了一种自动生成合理的人工环境的方法，该方法可以有效地检测JavaPathPath中的并发错误。这样的环境并行执行那些组件的方法，这些方法通过Java的并发构造进行交互，因此可能包含并发错误。 我们采用静态代码分析来识别集合方法的并行执行，以及根据交互程度对集合进行排序的度量。该技术的优点说明了对现实生活中的Java组件进行实验的结果关键词：软件构件，模型检测，环境建模，状态爆炸，并发错误，软件度量1介绍可靠和健壮的软件系统的开发通常涉及将整个系统分解为组件，并应用形式化方法，如模型检查[4]，以发现组件代码中的错误。在本文中，我们关注的是用Java实现的组件--我们使用术语组件来表示Java中的所有类型的开放系统，这些系统具有一组公共方法（由一个或多个类提供）形式的定义良好的接口，如库和插件。为了支持典型的构件软件开发过程，不仅要能够验证整个构件应用程序，而且要能够验证单个构件。原因是组件可以独立开发-组件的真实环境（例如应用程序的其余部分）可以 在组件开发时未知。此外，模块化验证-每次检查一个组件-有助于提高模型检查的可扩展性，因为组件通常具有比整个系统更小的状态空间1571-0661 © 2009 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.09.033146P. Parizek等人理论计算机科学电子笔记253（2009）145然而，一般来说，不可能将模型检查直接应用于孤立软件组件的代码，因为它是一个开放系统，而模型检查仅适用于封闭系统。组件的行为取决于使用它的上下文，即真实环境与组件交互的方式。因此，核查所需的部分信息缺失。我们称之为环境缺失问题。在Java组件的情况下，这个问题可以通过以下事实来说明：Java的常见模型检查器（JPF [22]，Bogor [18]）仅适用于具有main方法的完整Java程序-特别是，它们不能应用于不包含main的孤立组件。解决环境缺失问题的一个常见方法是构建一个人工环境[15]。在Java组件验证的上下文中，虚拟环境采用Java程序片段的形式，模拟特定真实环境的行为-虚拟环境与组件代码一起形成可以进行模型检查的完整Java程序（封闭系统）。人工环境通常由一个驱动程序组成，该驱动程序调用组件的方法和组件依赖项的存根虽然人工环境的Java代码可以手工编写[10]，但首选的方法是从其行为的高级模型自动生成[20][14]。该模型可以手工编写或自动构建，例如，基于要检查的组件的行为[5]。自动化环境生成的关键挑战是如何定义人工环境的行为模型-从模型生成Java代码是简单的[20][14]。行为模型的重要方面是：组件代码的覆盖率更具体地说，通常很难构建一个人工环境，（i）以触发组件代码中大多数错误的方式运行组件，从而允许模型检查器 找到它们，并且（ii）足够简单，允许模型检查器在由于状态爆炸而耗尽内存之前检测到至少一些错误[21]。在这篇文章中，我们的目标是使用Java PathPath模型检查器（JPF）[22]有效地检测Java组件中的并发错误（死锁，竞争条件）因此，在我们的例子中，挑战是决定人工环境的行为应该是什么，以便使JPF能够在由于状态爆炸而耗尽可用内存或合理时间之前找到至少一些并发错误。请注意，尽管状态爆炸通常是由程序中大量的并行线程和/或大数据域引起的，但我们只关注并行性的水平，因为大数据域在我们的情况下不是问题（见第二节的结尾）详情请参见1专注于Java代码中并发错误的检测，我们已经确定了以下方法来自动构建人工环境的行为模型，可以使用现有技术：• 通用环境[6]是最通用的环境：它调用每个P. Parizek等人理论计算机科学电子笔记253（2009）145147方法的任意有限次数，并与所有方法的其他调用并行（包括同一方法的并行调用）。它允许JPF找到所有的错误，并且可以很容易地以自动化的方式构建另一方面，在大多数情况下不可能使用这样的环境，因为使用JPF的验证由于大量的并行线程而容易出现状态爆炸，即使使用众所周知的方法来解决状态爆炸。• 方法对的随机选择是基于这样一个事实，即在许多情况下，仅使用两个并行线程就可以触发竞争条件和死锁。人工环境的行为模型定义了一个必须并行执行的方法对序列（一个并行方法对序列），生成的环境执行序列中的所有方法对，一次一个。为每对组件的方法定义一个并行方法对，并且这些方法对是随机排序的-这样，JPF尝试检查所有组件方法对的这种方法的优点是（i）相对较高的覆盖率-可以找到由两个线程的并行执行触发的所有错误-以及（ii）易于自动生成环境与使用通用环境相比，使用JPF进行检查不太容易发生状态爆炸，但是遍历许多并行对的状态空间可能比遍历单个元组的状态空间花费更多的时间。此外，由于并行方法对是随机排序的--那些涉及错误的方法可能在一个并行方法对序列的末尾• 通过搜索可疑模式来选择方法对是我们在[ 13 ]中首次提出的构建环境行为模型的方法。它基于代码的启发式静态分析，在组件方法对的Java字节码中搜索特定的可疑并发相关模式。环境的行为模型被定义为一系列并行方法对，根据静态分析，该技术通常可以在合理的时间内使用JPF检测Java代码中的并发错误。然而，它也有一个缺点-它只支持涉及Java方法对的模式，并且自然地，所支持的模式不能覆盖Java中所有可能的并发错误。因此，覆盖率低于通用环境和随机方法对的情况-在短时间内检测到一些错误，但根本没有发现其他错误。这三种方法在组件代码的覆盖率、JPF对状态爆炸的检查以及模型构造的自动化等方面都存在一定的缺陷例如，使用通用环境进行检查容易出现状态爆炸，而使用模式只允许发现一些并发错误。因此，我们提出了一种技术，用于自动构建合理的环境行为模型该技术的核心思想是环境的构建148P. Parizek等人理论计算机科学电子笔记253（2009）145Fig. 1.整个验证过程--右边的大盒子代表理性的人工环境的构建，里面的小盒子显示了构建的具体方法行为模型直接从组件(i) 一个简单的静态分析，通过Java的并发相关结构（例如访问共享变量）获取有关组件方法之间交互的特定信息(ii) 一种软件度量，用于度量方法之间的交互程度更具体地说，只有那些应该用JPF检查其并行执行是否存在并发错误的方法对（和集合）才被静态分析和度量选择-然后行为模型定义所选并行对和集合的序列。从技术上讲，我们在行为协议中表达了合理人工环境的行为模型[16][14]，这是我们小组开发的组件行为规范的形式主义。组件的方法参数的值用户负责定义覆盖组件代码中所有控制流路径的最小可能参数值集-这样，可以避免大数据域（状态爆炸的原因之一）。在行为协议中定义了行为模型，并在Java类中指定了参数值，环境生成器[12]用于从模型中生成人工环境的Java代码，然后应用JPF 在由组件及其人工环境组成的完整程序上，以发现组件代码中的实际并发错误（如果存在有一些）。整个过程如图所示1.一、总之，本文的主要贡献是一种技术，用于有效地检测Java代码中的并发错误与JPF隔离组件，其中涉及（i）自动生成一个合理的人工环境（JavaP. Parizek等人理论计算机科学电子笔记253（2009）145149代码）从其行为协议中定义的行为模型，以及（ii）通过静态分析和软件度量自动构建行为模型本文其余部分的结构如下。第2节介绍了一个简单的例子，用于说明该技术的关键思想。第3节介绍了所提出的技术的细节-特别是软件度量，通过并发结构来衡量Java方法之间的交互程度。第4节提供了对该技术的评价。论文的其余部分是相关的工作和结论。2运行实例在整篇文章中，我们说明了我们的技术的各个方面的Java代码的一个简单的组件OrderProcessor（图2）-它的代码是免费的并发性错误的目的是简单。请注意，placeOrder和payOrder方法不通过Java的并发构造进行交互，因为它们访问不同的共享变量，并且不使用公共锁对象-前者访问orders变量，而后者仅访问发票。3理性环境行为模式的构建我们的技术背后的想法是，并发错误可能发生在两个或多个Java方法的并行执行期间，只有当方法通过Java的并发相关结构进行交互时，例如，如果它们访问相同的共享变量。 将这种观察扩展到启发式，我们假设方法之间的高交互使得并发错误更有可能-具有高交互的方法的Java代码包含大量可能以错误的方式使用的并发相关构造。我们将Java方法之间的交互程度定义为通过Java的并发相关构造对方法之间的相互交互进行的严格评估（通过软件度量）。从技术上讲，Java方法具有相互交互的功能，如果它们的实现使用以下构造：• 对共享变量的读/写访问-对象、字段、局部变量和数组元素，• 通过相同对象（监视器）上的同步块和方法的互斥，以及• 通过在相同的监视器上调用wait和notify然而，同步块和wait/notify方法的调用都可以被认为是访问共享变量的特殊情况，因为在Java字节码中，锁定和解锁操作（对应于同步块）以及wait和notify调用涉及对共享对象的访问，150P. Parizek等人理论计算机科学电子笔记253（2009）145public class IOrderProcessor { privateMap orders= new HashMap（）;privateMap invoices= new HashMap（）;public int findDuplicate（intfindDuplicate）{Order o= new Order（getId（），count，false）;orders.put（o.id，o）;返回o.id;}}public int findDuplicate（int i，int n）{public void run（）{Order o=（Order）orders.get（id）;o.shipped= true;Invoicei= new Invoice（o. id，o.count）; invoice.put（i.orderId，i）;return i.价格;}}}public boolean compatibility（intp， int i）{Invoicei=（Invoice）invoices.get（id）;if（i.price<= money） i.paid=true;}}}图二. OrderProcessor组件的Java代码代表监视器。因此，可以将Java方法之间与并发相关的交互推广到对共享变量的读/写访问。显而易见的想法是评估Java方法之间的交互程度通过一个度量，该度量考虑了方法的字节码。我们提出了一个新的软件度量，共享变量访问（SVA），用于一组Java方法。一般来说，用于构建合理环境的行为模型的算法将方法列表作为输入，其中给定组件的每个方法至少出现两次-这对于允许在相同方法的两个实例上应用SVA度量并因此允许检测Con-A是必要的。P. Parizek等人理论计算机科学电子笔记253（2009）145151⊆--关于我们----并行执行同一方法的两个或多个实例时出现的货币错误。然而，为了简单起见，我们只解释了一组S的方法的算法。对列表的一般化是直接的，例如，通过将不同的子集添加到对应于相同方法的元素。模型构建的实际过程包括以下四个步骤：1) 共享变量访问的识别：使用简单的静态分析来获取S中方法的Java字节码中共享变量访问的所有必要信息，即。为SVA指标提供输入-详情见第2.1节。3.1.2) 度量值计算：为集合S的每个子集Si计算SVA度量的值（第3.2节）-S的包含没有交互的方法的子集（由度量的零值标识）被丢弃，因为缺少任何交互的并发性都消除了并发性错误的可能性3) 子集的排序和修剪：S的剩余子集根据它们的SVA度量值以降序排序，形成有序列表L -JPF应用于子集的顺序，目的是检查每个子集中方法的并行执行，以这种方式确定。然后，列表L被修剪：如果存在具有更高度量值的元素Lj（对应于Sj），则从L中移除对应于S i的元素L i，使得S i S j，因为（i）检查L j中的方法的并行执行将发现通过检查L i中的方法的并行执行将检测到的所有错误，并且（ii）由于排序，L i将在L j之后被检查。4) 生成环境选择S的几个子集而不是使用它们的并集背后的基本原理排序优先考虑那些具有高度量值的方法子集，因此更可能具有并发错误，目标是在低时间和内存中检测错误。特别是，具有最高SVA度量值的子集中的方法的并行执行首先由JPF检查-在理想情况下，该子集包含其并行执行导致并发错误的方法（假设组件代码中存在错误在 简 化 的 OrderProcessor 组 件 的情况下（ 第 2 ） ， 它 提 供 了 集 合 SOP=placeOrder、confirmOrder、payOrder、结果步骤1-3可以是例如包含SOP的所选 子 集 的 列 表 LOP= （ placeOrder ， confirmOrder ， payOrder ， placeOrder ，confirmOrder，confirmOrder，payOrder）。LOP中元素的实际顺序取决于度量。然而，集合placeOrder，payOrder并不包含在LOP中，因为这两个方法并不通过Java并发结构进行交互。152P. Parizek等人理论计算机科学电子笔记253（2009）1453.1通过静态分析识别共享变量访问静态分析的目的是提供有关组件方法的Java字节码的所有信息，SVA度量需要这些信息作为输入。具体而言，分析提供：• 组件的方法的集合• 共享变量的列表，即由集合中的任何两个或更多个方法访问的变量（列表的大小为[0，∞]），以及• 从集合中访问每个方法中每个共享变量的次数-显然，该次数必须在[0，∞）中。给定一个实现组件的Java类，分析将分别应用于每个方法。它涉及（i）以类似于[23]的方式构造方法的控制流图，以及（ii）每个控制流路径中Java字节码指令的线性扫描，识别路径中所有共享变量访问。对共享变量的访问由任何指令表示，从共享存储器中读取变量的内容或写入这样的变量。由于共享变量访问的数量可能会在控制流路径上有所不同，因此我们将方法的共享变量访问数量定义为所有控制流路径数量的平均值。 通常，不同控制流路径的数量 是大致相同的，因此平均值是一个很好的近似值。然而，请注意，静态分析通常是不精确的，因为它只适用于静态类型和共享变量的名称。有两个原因：（1）分析所使用的ASM库[1]没有提供有关变量运行时值的额外信息，以及（2）为了效率，我们决定不执行任何复杂的数据流分析。这种不精确的结果是分析可能会报告“虚假的交互”，即它可能会报告两个方法通过访问共同的共享变量进行交互，而实际上它们访问具有相同类型的不同变量。另一方面，这种分析是保守的--它3.2并发方法间交互程度的度量在设计SVA指标时，我们确定了以下三个选择，这些选择决定了该指标是否以及在多大程度上优先考虑（即产生更高的值）：(C1)集合中的低或高（或任何）数量的方法(C2)特定变量的极端共享优于变量的均匀共享，其中极端共享意味着在一种方法中对所选变量的访问次数较高，而在其他方法中对该变量的访问次数较低，而均匀共享意味着在所有方法中对该变量的访问次数相对较高;（C3）所有方法对单个变量的极端共享优于均匀共享所有变量的所有方法。P. Parizek等人理论计算机科学电子笔记253（2009）145153∞−−- -||−∞∞然而，我们认为，实现的选择不能在设计时的度量和没有知识的组件进行检查，因为不同的选项的选择可能是适当的不同的组件-它应该有可能实现所有三个选择（C1，C2，C3）在运行时。因此，我们决定通过参数化函数实现SVA度量函数的输入是所有方法的Java字节码信息在给定的集合（通过静态分析获得）中，函数的输出是区间[0，]中的单个实数，表示集合中方法之间的交互程度。为了反映选择C1、C2和C3，实现SVA度量的函数被设计为具有三个独立的参数（α、β和γ），这允许在很大程度上配置度量更具体地说• 参数α的值确定是否极端共享（对于α> 0. 5）或均匀共享（对于α<0。5）一个变量是优选的，以及优选到什么程度，• 参数β的值决定了一个变量的极端共享（对于β> 0. 5）或所有变量的均匀共享（对于β<0。5）是优选的，并且• 参数γ的值决定了优选低或高（或任何）数目的方法，以及优选到何种程度。关于参数选择C2和C3的重要方面是它们具有相似的性质-具体地说，它们都涉及根据特定参数（α或β）的值从给定集合中选择代表性元素，其中集合的元素量化某种现象-访问共享变量的次数在我们的例子中-并且所选择的值表征整个集合。 例如，所选值可以是集合中所有元素的中值（最大值、最小值）。在这两种情况下（C2和C3），我们决定使用分位数函数。 从技术上讲，有序数据集上的P分位数标识了将数据集划分为 两部分：一部分包含数据集的低100P%，另一部分包含其余部分。特别地，0. 5分位数对应中位数，0分位数对应最小值，1分位数对应最小值。分位数为最大值。 通过改变α和β的值，可以将SVA度量配置为偏好极端共享或均匀共享。至于选择C1，我们必须找到一个表达式，允许根据方法的数量和参数γ的值来增加和减少度量具体地说，我们正在寻找一个内射和连续函数，它将[2， ）中的方法数和[0， 1]中的γ值映射到[0，1]中的实数。区间[0，）。从满足这个要求的许多函数中，我们选择了Mtan（2γ−1），其中M代表给定的方法集。如果tan（2γ 1）0，则优选低数量的方法，反之亦然。<然而，尽管SVA度量的配置有各种可能性高于集合M2的度量154P. Parizek等人理论计算机科学电子笔记253（2009）145−−-||--||||关于我们−联系我们我们的优势- -比集合M2中的方法更好。根据上述所有推理，实现SVA度量的函数具有以下形式，其中qX代表X分位数，M代表给定的Java方法集合，V代表集合M，并且Ai，j表示方法Mj中对变量V i的访问次数：(1)qβ（qα（Ai，j，j=1.. |），i = 1.|) ,i = 1.. |）·|M|tan（2 γ − 1）|tan(2γ−1)该函数通过三步过程进行评估。首先，一名代表通过Ai，j，j=1.的α分位数，从M中所有方法中访问V i的次数的有序列表中为每个变量V i选择访问次数。M. 然后，通过访问各个变量的代表性数量的有序列表的β分位数，选择以任何方法访问集合V中的任何共享变量的代表性数量。最后，将到目前为止计算的中间结果乘以子表达式Mtan（2γ−1），以考虑方法集的大小M和γ的值。当为给定方法集的每个子集计算SVA度量值时，将创建方法子集的有序列表-子集根据度量值以降序方式排序。请注意，SVA度量的参数（α、β和γ）的值只影响列表中方法子集的顺序，而不影响特定子集的包含或排除。例如 在订单处理器组件的情况下（第 2），使用值α = 1，β = 1和γ = 0。107301（在这种情况下tan（2 γ 1）= 1）导致订单（placeOrder，confirmOrder，confirmOrder，payOrder，placeOrder，confirmOrder，payOrder），而使用值α = 0。5，β= 0。5，γ=0。5（在这种情况下tan（2 γ 1）=0）导致顺序（placeOrder，confirmOrder ， payOrder ， placeOrder ， confirmOrder ， confirmOrder ，payOrder）-这种差异背后的主要原因是，由于γ的值，在第一种情况下更倾向于使用较小的方法集。4评价为了对所提出的技术进行评估，我们开发了一个原型工具，该工具将静态分析和SVA度量的实现与JPF和JPF的环境生成器集成在一起[12]。原型工具以完全自动化的方式工作作为输入，它接受• 要检查的组件的Java代码（例如一组Java类），• 可以并行执行的组件的公共方法列表（并行方法），• 在组件初始化期间必须调用的方法序列;在许多情况下这是空的（当不需要显式初始化• 在Java类中指定方法• SVA指标的参数值P. Parizek等人理论计算机科学电子笔记253（2009）145155对于给定的组件，我们的工具创建合理的人工环境（Java代码），然后在由组件及其环境组成的完整Java程序上运行JPF由于该技术的目的是检测并发错误，因此我们确保JPF只搜索死锁和竞争条件。在SVA度量的实验评估应该回答的问题中，我们确定以下三个是最重要的1) 所提出的技术是否真的可以有效地检测Java组件中的并发错误？2) 所提出的技术是否比第1节中描述的替代方法（随机选择方法对并搜索可疑模式）得到更好的结果？如果是，在哪些方面？3) 应该使用什么SVA度量参数的值组合，以最小化在为了回答这些问题，我们在两个真实的Java组件上进行了大量的实验我们使用 了 ConcurrentHashMap 类 （ Java 中 的 2000 行 代 码 （ loc ） ） ， 它 来 自 GNUClasspath （ 版 本 0.97.1 ） [8] 和 Daisy 文 件 系 统 [17] （ 800 loc ） 中 的java.util.concurrent包的实现，Daisy文件系统[17]被用作CAV/ISSTA 2004事件中挑战问题的分配DaisyDir类用作入口点。Daisy文件系统包含作者准备的并发错误（S。Qadeer），以评估各种验证工具。在ConcurrentHashMap的情况下，我们已经通过re手动注入了错误（竞争条件）在size方法中调用lock（）和unlock（）4.1实验配置我们已经在以下几种人工环境中进行了实验，所有这些都是基于特定方法集或方法对的并行执行• 随机对-随机选择的方法对，• 模式- 通过搜索可疑模式选择的方法对[13]，• 有序对- 通过静态分析和SVA度量选择和排序的方法对，以及• 有序列表-通过静态分析和SVA度量选择和排序的方法列表。方法在有序对和有序列表中的选择和排序是通过第3节中描述的算法进行的-区别在于使用有序列表意味着选择任意大小的列表，而使用有序对意味着选择大小为2的列表在有序对和有序列表的情况下，我们对SVA度量的不同配置进行了几次实验，以找到SVA度量156P. Parizek等人理论计算机科学电子笔记253（2009）145JPF检查。 我们已经确定了代表合理违约的SVA指标参数值的几种组合。每个参数值组合的名称由三个字母组成，表示选定的值：第一个字母对应于参数α，第二个对应于β，第三个对应于γ。我们为参数α和β选择了以下三个值：• 0的值对应于U（用于均匀共享的偏好• 对应于E的值1（用于极端共享的偏好），以及• 0的值。5对应于C（代表中央，即极端和均匀共享之间的东西）。对于γ，我们只选择了两个值：• 0的值。5对应于字母N（不依赖于方法列表的大小; tan（2 ×0. 5 −1）=0在表达式中（1），以及• 0的值。107301对应于S（对于较小的方法列表的偏好; tan（2 × 0. 107301 − 1）=−1（表达式中）①的人。为了说明，名称EES意味着α的值是1，β的值是1，并且γ的值为0。107301.请注意，只有0的值。5（字母N）用于有序对的参数γ，因为方法的数量总是相等的 到2-不需要表达对方法列表大小的依赖性由于所提出的技术旨在在合理的内存和时间内检测并发错误，因此我们以JPF可用的时间和内存都有限的方式确认了实验-限制设置为1024 MB和4小时。我们在初步实验的基础上设定了这些限制。所有实验均在以下配置（ 硬件和软件）上进行：配备2xDualCore CPU（Intel）（2.3GHz）和4GB RAM的PC，Gentoo Linux（2007年10月提供所有最新更新），Sun Java SDK build1.6.0_02-b 05（64位，混合模式）。关于JavaPathlog，我们使用2007年10月的当前版本，并为每个实验打开了偏序约简。4.2实验结果我们进行的实验结果列于表1中。我们测量的每个实验的特征是以秒为单位的总时间和JPF所需的内存量（MB）。总时间包括建造人工环境（及其行为模式，即人工智能）所需的执行静态分析和计算SVA度量所需的时间）和JPF查找错误所需的时间该表还包含列9/24）或0（如果没有JPF运行超过限值）。“时间”和“内存”列所有运行均超过其中一个极限）。如果没有P. Parizek等人理论计算机科学电子笔记253（2009）145157在特定实验中检测到错误，例如 由于非常积极的选择方法对或方法列表，则使用符号Daisy文件系统ConcurrentHashMap时间存储器>限制时间存储器>限制有序对EEN1490943130CCN1510953060UUN978310230893030有序列表EEN15204113690EES149043325800CCN147043434110CCS147045056220UUNn/an/a2/24143680UUS978210230642290模式1510-（57）- （165）0随机对17153109/24651690表1实验4.3结果讨论实验结果（表1）表明，所提出的技术-使用基于SVA度量构建的人工环境-相对于替代方法（随机选择方法对和搜索可疑模式），可以显着减少使用JPF检测Java组件中并发错误所需的时间和内存，如Daisy文件系统所示。然而，由于我们的技术是基于启发式的，期望它在所有情况下都能给出更好的结果是不现实的。例如，基于随机对的人工环境检查需要的时间和内存略少于ConcurrentHashMap的有序对（并且明显少于有序列表）。对于SVA度量使用不同的参数值可能会产生非常不同的结果，以及（ii）158P. Parizek等人理论计算机科学电子笔记253（2009）145关于并发错误的有效检测的最佳选择将是使用有序对或有序列表，其中SVA度量参数的值的那些组合优选极端共享（即EES和EEN）。同样，由于SVA度量基于启发式，因此期望EES和EEN的组合将为所有组件提供最佳结果是不现实的5相关工作尽管已经在以主流语言如Java和C实现的软件组件的模型检查中进行了大量研究（参见，例如，[7]和[3]）和构建组件模型检查的人工环境[15][20][21]，我们不知道任何其他方法试图通过自动降低环境复杂性，在有限的时间和内存当状态爆炸是由大量并行线程引起时，解决状态爆炸的众所周知的方法包括偏序约简[4]和状态空间遍历的逻辑学[9] -然而，这些技术只能在完整程序的模型检查期间应用，而不是为隔离组件构建人工环境。[21]中描述的环境构建方法使用Bandera Ensemination Generator（BEG）[20]从用户提供的行为模型自动生成驱动程序（Java代码），并通过静态分析从真实环境的现有实现（如果可用）自动提取存根。与我们的方法的关键区别在于，我们支持完全自动生成人工环境的合理行为模型，而在[21]的情况下，至少对于驱动程序来说，必须手动指定合理的行为模型(ii)涉及相当少数量并行线程。同样，我们也不知道现代面向对象编程语言（C++，Java）的任何并发相关的复杂性度量。虽然在Ada（[11]，[19]）中有几种方法来度量并发程序的复杂性，但没有一种方法可以代替我们的SVA度量。特别是，它们要么测量并发程序的控制流复杂度[11]，要么瞄准Ada特定的结构，如主动会合[19]。6结论提出了一种利用JavaPathData模型检查器（JPF）快速检测Java代码中并发错误的新方法。的该技术的核心思想是在Java字节码静态分析和Java方法集的新软件度量（SVA）的基础上，为隔离组件自动生成合理的人工环境。 静态分析识别通过并发相关P. Parizek等人理论计算机科学电子笔记253（2009）145159Java的构造（例如访问共享变量）和SVA度量根据方法之间的交互程度对集合进行排序。然后，以这样的方式生成人工执行，即首先由JPF检查具有最高SVA度量值的集合中的方法的并行执行，我们的实验与几个现实生活中的Java组件表明，所提出的技术可能会给一些组件的替代方法（随机方法对，搜索可疑模式）显着更好的结果-特别是，它使检测并发错误与JPF可能在有限的时间和内存，如果JPF是应用于完整的程序组成的组件和合理的环境的基础上构建的SVA度量。然而，期望该技术将为所有组件提供更好的结果是不现实的，因为它基于启发式。还要注意的是，该技术并不执行详尽的验证，因此只能用于显示代码中存在bug，而不是不存在-特别是，它不会发现由特定的复杂方法调用序列引起的并发错误虽然本文提出的技术针对的是用Java实现的组件，但它可以移植到另一种编程语言（例如，C或C#），提供了一个模型检查器，支持用该语言编写的多线程程序的验证。在未来，我们计划（i）采用更精确的Java代码的静态分析（例如指向和形状分析），以提供更准确的评估方法之间的相互作用，和（ii）设计几个版本的SVA度量使用不同的功能和比较所有版本的几个组件。我们还希望对拟议的方法进行更广泛的评估，更多的组件，假设我们将有包含一些并发错误的复杂组件-使用错误播种技术（例如[2]）是获得此类组件的选项确认这项工作得到了捷克科学院的部分支持（项目1ET 400300504）。引用[1] ASM：Java字节码操作框架，http://asm.objectweb.org[2] 布拉德伯里，J.S.，J. R. Cordy和J. Dingel，并发Java的突变运算符（J2SE 5.0），第二届突变分析研讨会论文集（Mutation 2006），2006年[3] Chaki，S.，E. Clarke，A. Groce，S. Jha和H. Veith，C中软件组件的模块化验证，IEEE软件工程学报，30（6），2004年6月[4] 克拉克，E.，O. Grumberg和D.Peled，[5] Cobleigh，J. M.，D. Giannakopoulou和C. S. Pasareanu，组合验证的学习假设，在第九届国际会议的工具和算法的构造和系统分析，LNCS，卷。2003年第2619号来文160P. Parizek等人理论计算机科学电子笔记253（2009）145[6] Giannakopoulou，D.，C. S. Pasareanu和H. Barringer，软件构件验证的假设生成，第17届IEEE自动软件工程国际会议（ASE）论文集，IEEE CS，2002年[7] Giannakopoulou，D.，C. S. Pasareanu和J.M. Cobleigh，Assume-guarantee Verification of Source Codewith Design-Level Assumptions，第26届ICSE会议论文集，IEEE CS，2004年[8] GNU克拉斯帕斯，http://www.gnu.org/software/classpath/[9] Groce，A.，和W. Visser，Heuristics for Model Checking Java Programs，Proceedings of the 9thInternational SPIN Workshop on Model Checking of Software，LNCS，vol.2002年第2318号来文[10] 休斯，G.，S. P. Rajan，T. Sidle和K. Swenson，并发Java程序中的错误检测，SoftMC 2005会议录，ENTCS，144（3）[11] 马修斯，M。E、和S.Tu，《测量并发程序中的控制流复杂性》，1995年第13届PNSQC会议记录[12] Parizek，P.，Java Path环境生成器，http://dsrg.mff.cuni.cz/projects/envgen[13] Parizek，P.，和F. Plasil，软件组件的部分验证：环境构建的启发式，第33届EUROMICRO SEAA会议论文集，IEEE CS，2007年[14] Parizek，P.，和F. Plasil，Specification and Generation of Environment for Model Checking of SoftwareComponents，2006年FESCA会议录，ENTCS，176（2），2007年[15] 帕萨雷亚努角美国，M. Dwyer和M. Huth，Assume-Guarantee Model Checking of Software：AComparative Case Study，第六届SPIN软件模型检查研讨会论文集LNCS，第1680卷，1999年[16] Plasil，F.，和S.陈晓，软件构件的行为协议，北京：软件工程出版社，2002年。[17] Qadeer，S.，Daisy文件系统，CAV/ISSTA关于并发软件规范、验证和测试的联合特别活动，2004年，http://research.microsoft.com/www.example.com~qadeer/cav-issta.htm[18] 罗比，M。B.陈晓，一种可扩展和高度模块化的模型检测框架，第九届欧洲软件工程会议论文集，2003[19] Shatz，S.M，Towards Complexity Towards Ada Tasking，IEEE Trans.SW. 工程师：14（8），1988年[20] 特卡丘克岛，M. B. Dwyer和C. S.陈文生，软件模型检测，2003年第一届中国软件工程学术研讨会论文集，[21] 特卡丘克岛，和S. P. Rajan，自动环境生成在商业软件中的应用，在ISSTA'06会议录中，ACM出版社，2006年[22] Visser，W.，K. Havelund，G. Brat，S. Park和F. Lerda，Model Checking Programs，AutomatedSoftware Engineering Journal，10（2），2003[23] 赵，J，分析Java字节码中的控制流。福冈研究所的报告技术，2000年