软件构件模型检测环境生成方法研究

理论计算机科学电子笔记176（2007）143-154www.elsevier.com/locate/entcs软件构件模型检测环境的描述与生成Pavel Parizeka，1，Frantisek Plasila，b，1软件工程查尔斯大学，数学和物理学院布拉格，捷克共和国{parizek，plasil}@ nenya.ms.m.cuni.cz捷克共和国科学院计算机科学研究所捷克共和国布拉格cs.cas.cz摘要孤立的软件组件的模型检查本质上是不可能的，因为组件不形成具有显式起始点的完整程序。 为了克服这个障碍，通常需要创建一个组件的环境，该组件是模型检查的预期对象。我们提出了基于行为协议的自动化环境生成方法[9];据我们所知，这是唯一一个为软件组件的模型检查而设计的环境生成器。 我们比较它与Bandera环境生成器工具[12]中采用的方法相结合，该工具设计用于Java类集的模型检查。关键词：软件构件，行为协议，模型检测，环境自动生成1引言模型检测是软件系统形式化验证的方法之一，目前受到广泛关注。尽管如此，在软件的模型检查可以广泛应用于实践之前，仍然有一些障碍必须解决，至少部分可能最大的问题是软件系统典型的状态空间的大小。这个问题（状态爆炸）的一个解决方案是将软件系统分解成小的和定义良好的单元，组件。然而，一个组件通常不能被孤立地检查，因为它没有形成一个应用模型检查所固有的完整程序。因此，有必要创建组件环境的模型1这项工作得到捷克科学院（项目1ET 400300504）和法国电信的部分支助，外部研究合同号为46127110。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.02.036144P. Parizek，F.Plasil/Electronic Notes in Theoretical Computer Science 176（2007）143对程序进行模型检查，然后对整个程序进行检查，包括环境和组件。环境的创建方式应该尽量减少由组合引起的状态空间大小的增加1.1论文的目标和结构本文旨在解决的问题，自动生成的环境中的Java语言实现的软件组件的模型检查主要目标是介绍我们基于行为协议的方法[9]，并将其与Bandera环境生成器工具[12]中采用的方法进行比较，这是我们所知道的唯一其他Java方法。本文的其余部分组织如下。第2节提供了一个例子来说明环境生成的问题，第3节介绍了Bandera环境生成器（BEG）[12]。第4节首先概述了行为协议[9]，然后介绍了主要贡献-描述了我们基于行为协议的环境规范和生成方法。第5节提供了两种方法的比较，并简要介绍了我们的概念实现证明。论文的其余部分包括相关的工作和结论。2动机为 了 说 明 如 何 创 建 一 个 环 境 ， 我 们 提 出 了 一 个 简 单 的 例 子 - 一 个 Java 类DatabaseImpl和这个类的手写环境，假设DatabaseImpl是模型检查的目标。该类实现一个接口，并需要设置一个接口类型的内部引用因此，它也可以被看作是一个数据库组件，具有一个提供的接口和一个必需的接口。DatabaseImpl类源代码的关键片段如下所示public voidstart（）;public void stop（）;public void insert（int key，int value）;public String get（int key）;}public class DataImpl实现IDatalog { private ILoggerlog;public void start（）{ log.start（）;}公共void stop（）{P. Parizek，F.Plasil/Electronic Notes in Theoretical Computer Science 176（2007）143145return（）;}publicint findDuplicate（int [] nums）{...}public String getString（String s）{...}}一般来说，环境应该允许模型检查器（i）搜索并发错误（通常通过引入并行执行的几个线程来反映），以及（ii）检查所有控制流程路径（通常通过随机选择所有方法的参数值来解决由其源代码的“重要”片段捕获public class Uncategorized {...public void run（）{String val = db.get（getRandomInt（），getRandomString（））;...}}publicstatic void main（String[] args）{IDatString db = new DatabaseImpl（）;db.setLogger（new LoggerImpl（））;int findDuplicate（）;new EnvThread（）.start（）; new EnvThread（db）.start（）;...return（）;}在本例中，两个控制线程使模型检查器能够搜索对于并发错误，将创建。也采用随机选择参数值以检查所有控制流路径（getRandom...146P. Parizek，F.Plasil/Electronic Notes in Theoretical Computer Science 176（2007）143电话）。显然，即使在简单的情况下，手工创建环境也是一项艰巨而繁琐的工作。这个问题的一个直接解决方案是从比代码提供的更高级别的抽象自动在第3节和第4节中，我们提出了基于这一想法的两种解决方案。3Bandera中的环境生成器3.1班德拉Bandera [6]是一个为完整Java程序的模型检查而设计的工具集即以主方法为特征的那些。它由模型提取器、模型翻译器、环境生成器和模型检查器几个模块组成。模型提取器从Java源代码中提取（有限的）内部模型，模型翻译器将内部模型翻译成目标模型检查器的输入语言。在这里，Bandera工具集最初支持Spin和Java Path模型检查器，但目前它主要用于Bandera特定的模型检查器（Bogor [11]）。3.2Bandera环境生成器Bandera Environment Generator（BEG）[12]是一个为Java类自动生成环境的工具给定一个完整的Java程序，BEG工具的用户必须将程序分解为两个部分-测试单元，即要测试的类及其环境。 由于环境部分对于模型检查来说通常太复杂，因此有必要创建一个抽象环境。这个抽象的环境可以从一个创建的• 根据用户提供的假设，或者• 从环境类的代码分析结果（如果可用）。例如，模型可以指定某个方法应该连续调用五次，或者它应该与另一个特定的方法并行执行由于在软件组件的情况下通常不存在环境类，我们将进一步考虑第一个选项-即抽象环境是从用户指定的假设中生成的为此，BEG工具提供了两种正式的符号- LTL和正则表达式。实际的规范（第2节中介绍的DatabaseImpl类的环境规范，用BEG工具的输入语言编写，可以如下所示环境{实例化{1 LoggerImpl日志;P. Parizek，F.Plasil/Electronic Notes in Theoretical Computer Science 176（2007）143147System. out. println（）;intx = 5;}--环境行为常规假设{T0：（db.get（））|db.insert（））*T1：（db.get（x））|db.insert（5，“abcd”））*}}instantiations部分允许用户指定应该创建多少个特定类型的实例，以及可以引 用 它 们 的 名 称 在 本 例 中 ， 实 例 化 了 两 个 对 象 -LoggerImpl 类 的log实 例 和DatabaseImpl类的db正则假设部分包含描述环境相对于测试类的行为的正则表达式。每个正则表达式定义了一系列应该由单个控制线程执行的操作。在我们的示例中，定义了两个控制线程，它们都对IDatalog接口上的insert和get方法的调用序列进行请注意，整个执行的特征在于指定的线程（T0，T1）-没有因此，在这样的环境规范中，无法合理地对IDatalog接口上的start和stop方法进行建模BEG工具还允许在测试类上指定方法调用的参数值。如果一个参数的值没有被指定，就像上面的线程T0一样，那么在模型检查期间，它是从给定类型的所有可用值中（例如，在引用类型的情况下，从给定类的所有分配实例中）非确定性地选择的。作为方法调用的参数，甚至可以使用在instantiations部分定义的变量（例如上面的x由于BEG工具不是专门用于软件组件，而是对于普通的Java类，有必要手动指定实现目标组件的类的环境;另一种选择是开发一个工具，用于将组件体系结构和行为的ADL规范自动转换然而，由于最新的Bandera版本只是一个alpha版本[6]，还没有完全稳定，我们决定使用Java Path模型检查器（JPF）[13]。因此，我们面临着创建环境生成器的问题，因为没有可用的环境生成器（BEG不是为组件设计的，而且最新的Bandera版本不再允许使用Java Path作为目标模型检查器）。148P. Parizek，F.Plasil/Electronic Notes in Theoretical Computer Science 176（2007）1434Java Path我们已经建立了自己的环境生成器的模型检查组件实现的Java语言。我们的方法源于这样一个假设，即组件在设计期间是在ADL（架构描述语言）中指定的，其中特别包括它们所提供和所需接口的指定以及它们行为的指定。后者是通过行为协议完成的[9]。在本节中，我们将展示如何利用这种行为规范来生成组件模型检查所需的环境4.1行为协议行为协议是一种表达式，它描述了软件组件在组件的所提供和所需接口上的原子事件方面的行为，即在这些接口上接受和发出的方法调用请求和响应方面。Fig. 1. 数据库和日志组件，定义在节。2图1中数据库组件的协议示例1在下面：？db.start↑;！start;！db.start↓;（？db.insert||什么？db.get）*;？db.stop{！log.stop}由于该协议指定了数据库外部接口的相互作用，因此它是数据库的帧协议[9]。非正式地说，它指定了数据库功能，该功能从接受db上的start调用请求开始。作为一种反应，它调用startatlog并对db上的start调用发出响应。接下来是多次并行地在db上接收insert和get最后，它接受一个对db的stop调用请求，作为反应，它在log中调用stop，并对db上的stop调用发出响应。每个事件都有以下语法：< interface>.&方法（其中suffix是可选的;没有suffix的事件是下面解释的语法快捷方式）。Prefix？ 表示接受事件和前缀！表示发出事件。 sux ↑代表请求（即， 方法调用），而sun_x ↓代表响应（即， 从方法返回）。 一种表达！I.MISASHORTUTF O R！i.m↑;？i.m↓，一个新的xre sss ionofthef o rm？我是不是该去看医生了？i.m↑;！i.m↓ andanexxpressionofthe form？i.m{prot} isa shor tcutP. Parizek，F.Plasil/Electronic Notes in Theoretical Computer Science 176（2007）143149为了什么？i.m↑;prot;！i.m↓，当该保护是一个预处理器时。 NULL密钥表示一个空协议。上面的例子还介绍了几个操作符。 字符是序列运算符，* 是重复运算符，||是或并行运算符。行为协议还支持一个可选的operator+和一个与-并行的op-erator|. 事实上，这一过程只是一个过程，例如： 一||bs tandsfora+ b +（a|（b）。的|运算符表示与其操作数对应的所有可能的迹线交织。行为协议定义了一组可能无限的事件轨迹，每个事件轨迹都是有限的。每个组件都有一个与之相关的帧协议，复合组件也可以有一个架构协议[9]。组件的框架协议描述其外部行为，这意味着它只能包含组件外部接口上的事件。另一方面，架构协议描述了一个组件在嵌套的第一层的子组件的组成方面的行为4.2Java路径与协议栈当使用行为原型检查通过ADL指定的组件应用程序时，有必要（i）对于层次结构中的每个复合组件，检查嵌套的第一级的子组件的组成符合性，以及框架协议与架构协议的符合性（ii）并且对于每个复合组件，验证组件的实现遵守其框架协议。为了检查协议的一致性，我们使用我们研究小组开发的协议检查器[7]，为了检查原始组件是否遵守其帧协议，我们使用通过JPF与我们的协议检查器[8]合作创建的工具。该工具必须应用于由目标组件及其环境组成的程序。在数据库组件检查期间JPF和协议检查器之间的通信如图2所示。模式的左部分显示JPF遍历组件的代码（状态空间），右部分显示协议检查器的状态空间，该状态空间由组件的帧协议确定。我们开发的JPF插件跟踪执行调用和返回指令，这些指令与目标组件的所提供和所需接口的方法相关，并以原子请求和响应事件的形式通知协议检查器这些指令。协议检查器验证从接收到的事件构造的跟踪是否符合组件的帧协议。当协议检查器遇到意外事件或丢失事件时，它告诉JPF停止状态空间遍历并向用户报告错误（反例）150P. Parizek，F.Plasil/Electronic Notes in Theoretical Computer Science 176（2007）143图二. Java路径与协议栈4.3用反向帧协议对环境建模组件的环境可以通过其反向框架协议[1]有利地建模，通过将所有接受事件替换为发出事件，反之亦然，从组件框架协议构建。以这种方式构建的反向帧协议迫使环境• 在组件期望的时刻调用组件的特定提供接口的特定方法，以及• 在组件“希望”这样做的时刻接受在组件的特定所需接口上发出的特定方法调用上面介绍的Database组件的倒排帧协议是：！db.start↑;？log.start;？db.start↓;（！db.insert||！db.get）*;！db.stop{？log.stop}我们的环境生成器接受所有语法上有效的帧协议，但以下形式的协议除外：a+！B、！a*;？B.不支持格式的帧协议的原因？a+！b是环境驱动的倒置这样的协议不能确定它应该等待多长时间！b事件发生之前，它发出一个调用，对应于？一个事件，因此禁用另一个选项（即！（b）。协议的形式！a*;？b不支持的原因类似-环境无法确定何时重复！a*将被删除。建议使用以下形式的协议！a*;！B代替（只要可能），因为在这种情况下，b事件告诉环境，重复已经结束。为了最小化JPF必须遍历的状态空间的大小，我们的环境生成器在创建反向帧协议和生成环境代码之前，对目标组件的帧协议执行几次转型的主要目标是• 在协议嵌套的最外层获取尽可能多的替代运算符+的实例。这种方法的优点是，所有这些变更都可以由多个JPF实例并行检查，从而降低了P. Parizek，F.Plasil/Electronic Notes in Theoretical Computer Science 176（2007）143151目标组件模型检查的时间要求• 减少重复的次数，以及由|操作员，即使是以准确性为代价。例如，我们的生成器将• 在某个子协议上迭代到空协议和该子协议的两个副本的序列之间的替代方案（例如，该协议！a* 被转换为协议NULL +（！a;！（a）），• 包含所有可能序列之间的替代方案的一些替代方案的序列（例如，协议！a;（！b1+！b2）被转换为协议（！a;！b1）+（！a;！b2）），• 一个与并行操作符，将两个子协议（它们都是替代协议）连接到由| operator-the pairs are selected in a way ensuring that each element of thetwo alternatives is present at least in one of the pairs (e.g. the protocol (!a1+！a2）| (! b1+！b2）被转换为协议（！A1|！b1）+（！A2|！b2）），以及• 具有三个或更多个子协议的与-并行操作符到所选择的子协议对之间的替代，其中每一对由|操作者，并且随后是不属于所选对的子协议序列;以第一子协议与第二子协议配对、第二子协议与第三子协议配对等等的方式选择所述对（例如，协议a|C| d被转换为协议（（ a| b ） ; c ; d ） +（（b）|c）;|c) ;a;d）+（（c|（d）;（a）;（b））。4.4方法参数值的规范我们对方法参数的可能值的具体化的解决方案是基于这样的想法，即用户定义被认为是参数的值的集合。 从实现的角度来看，这些集合将被放入一个特殊的Java类中，作为所有值集合的容器。 某种类型的方法参数的值稍后从针对该类型和方法考虑的值集合中非确定性地选择。除了整个组件通用的值集之外，还可以定义特定于特定方法或接口的值集。下面是数据库组件的值的指定片段int []{1，2，5，10}};int []{1，3，5，12}};String[]{“abcd”，“EFGH1234”}）;第一个语句定义了一组整数值，它是IDatmap接口的insert方法所特有的。另外两个语句定义了应用于数据库组件接口的所有方法的整数和字符串这种方法的主要缺点是用户必须定义他/她的152P. Parizek，F.Plasil/Electronic Notes in Theoretical Computer Science 176（2007）143以强制模型检查器检查组件中所有控制流路径的方式拥有值集。5评价在本节中，我们比较了两种建模上述环境的方法，即BEG工具的方法和我们基于协议的方法。它们之间的主要差异是：• BEG工具允许仅在指定环境行为的正则表达式的最外层指定并行性（在行为协议的情况下没有这样的限制）。• 行为协议不支持方法参数，因此方法参数的可能值必须在一个特殊的Java类中单独指定，而BEG工具允许直接在指定环境行为的表达式中指定方法参数的值。值得一提的是，还有一个不同之处在于BEG工具针对的是具有非正式指定的提供和必需接口的普通Java类，而我们的方法针对的是具有以显式方式定义的提供和必需接口的软件组件。作为一种特性，支持直接在指定行为的表达式中指定参数值的另一个优点是，它使环境生成器能够选择重载方法的正确版本-或者生成一个代码，该代码将非确定性地调用符合规范的所有方法版本。我们已经创建了一个环境生成器的实现，它使用组件的反向帧协议作为环境行为的模型它针对使用分形组件模型[5]的组件，并期望使用分形ADL来定义组件。我们已经成功地将我们的环境生成器应用于一个基于组件的应用程序，该应用程序由20个组件组成转换的帧协议，在节中描述4.3，在更复杂的组件的情况下，将由协议确定的状态空间的大小减小约30倍，因此也降低了组件的模型检查所需的时间然而，模型检查更复杂的组件与环境产生的框架协议，没有应用转换是不可行的。尽管框架协议的转换引入了环境的抽象，但技术仍然比简单的测试更系统化。让我们再次强调，没有环境的组件的模型检查是根本不可能的，因为JPF只适用于完整的Java程序，而不是孤立的软件组件。P. Parizek，F.Plasil/Electronic Notes in Theoretical Computer Science 176（2007）1431536相关工作除了Bandera环境生成器[12]，我们不知道任何其他方法来指定和生成用于软件组件或面向对象程序部分的模型检查的环境然而，存在面向对象程序的模型检查器，它们不需要生成环境，因为这些工具通常从完整的程序（以主方法为特征）中提取有限模型，然后检查模型-这种模型检查器的一个例子是Zing[2]。还有一些工具可以解决自动生成过程程序片段的环境的问题（例如，驱动程序、库等）。这样的工具的一个例子是SLAM [4]模型检查器，它是SDV工具的一部分，用于验证Windows操作系统的设备驱动程序。给定一个程序，检查器创建程序的布尔抽象（所有值类型都近似于布尔），然后检查某些期望的时间属性是否适用于抽象。它使用细化原则来丢弃抽象中存在但原始程序中没有的错误（假否定）。设备驱动程序的环境由Windows内核提供的接口定义。SLAM工具通过训练对环境进行建模[3]。这里，基本原则是，对于要建模的某个过程P，它首先获取几个使用过程P的驱动程序，然后在这些驱动程序上运行SDV工具，从而获得过程P的几个布尔抽象，最后合并所有这些抽象，并将得到的内核过程P的布尔抽象放入库中以供将来重用。我们的环境生成工具部分基于[10]。 本文中描述的工具是为Bandera工具集设计的，也使用了反向帧协议的思想;它也专注于符合分形组件模型的组件[5]。我们决定不使用这个工具，主要是因为它生成了一个显著增加状态空间大小的环境，因为它没有使用4.3节中描述的任何转换，也没有提供任何指定方法参数值的方法-所有这些都使它在实践中几乎无法使用。7结论对孤立的软件组件进行直接的模型检查通常是不可能的，因为模型检查器只能处理完整的程序。因此，有必要为每个组件创建一个模型检查的环境本文比较了构件环境生成的两种方法，类-即第3节中的Bandera环境生成器（BEG）工具[12]，以及第4节中基于行为协议的方法[9]。这两种方法之间的主要区别在于对并行性的支持级别、对参数值的指定的支持以及BEG工具专注于普通Java类而我们的方法针对软件154P. Parizek，F.Plasil/Electronic Notes in Theoretical Computer Science 176（2007）143具有明确定义的提供和必需接口的组件至于未来的工作，一套用于方法参数的非决定性选择值的自动推导是我们目前的目标。它的动机是这样一个事实，即手动定义这样的集合需要用户仔细捕捉一种方法，让模型检查器检查目标组件中的所有控制流程路径。导出可能的参数值的可行方法是使用Java源代码（或字节代码）的静态分析致谢我们要特别感谢Jiri Adamek和Nicolas Rivierre提供的宝贵意见，以及Jan Kofron提供的关于协议检查器与JPF集成的许多提示引用[1] Adamek，J.， 和F. 组件组成错误和更新原子性：静态分析，Journal of Software Maintenance and Evolution：Research and Practice，17（2005），pp.三六三至三七七[2] 安德鲁斯，T.，S. Qadeer，S. K. Rajamani，J.谢振：一种面向并发软件的模型检测器，技术报告，微软研究院，2004年[3] 鲍尔，V. Levin和F. Xie，通过训练自动创建环境模型，TACAS 2004，93-107[4] 鲍尔，S. K. Rajamani，SLAM项目：基于静态分析的可编程系统软件，POPL 2002，ACM，1-3[5] Bruneton，E.，T. Coupaye，M. Leclercq，V. Quma，and J. B. Stefani，An Open Component Model andits Support in Java ， In Proceedings of the International Symposium on Convenient-based SoftwareEngineering（ICSE 2004 -CBSE 7），LNCS，3054（2004），May 2004[6] Corbett，J. C.，M. B. Dwyer，J. Hatterdham，S.劳巴赫角S. Pasareanu，Robby和H.卓恩、班德拉：从Java源代码中提取可执行状态模型，ICSE 2000，ACM，439-448[7] 马赫，M.，F. Plasil和J. Kofron，行为协议验证：对抗状态爆炸，International Journal of Computer and Information Science，6（2005），22-30[8] Parizek，P.，F. Plasil和J. Kofron，软件组件的模型检查：使Java PathData与行为协议协作，Tech。第2006/2号报告，Dep.查尔斯大学西南工程学院，2006年[9] Plasil，F.，和S. Visnovsky，软件组件的行为协议，IEEE软件工程学报，28（2002）[10] Potrusil，T.，“Specifying Missing Component Environment in Bandera”, Master Thesis, Department ofSoftware[11]罗比，M。Dwyer和J.Hatterygal，Bogor：一个可扩展的高度模块化的模型检查框架，在FSE 03：软件工程的基础，pp。267-276，ACM，2003年[12] 特卡丘克岛，M. B. Dwyer和C. S. Pasareanu，用于软件模型检查的自动化环境生成，第18届IEEE自动化软件工程国际会议（ASE03），第116页，2003年[13] Visser ， W. ，K. Havelund ， G.Brat ， S.Park 和F.Lerda ， Model Checking Programs ， AutomatedSoftware Engineering Journal，10（2003）