（计算机软件与理论专业论文）基于模型检测的类测试自动生成技术研究.pdf

基于模型检测的类测试自动生成技术研究 摘要 高可信软件技术是软件理论研究和工程实践领域关注的焦点之一。近年 来，越来越多的形式化方法被应用于提高软件质量的研究上。软件测试是 保证软件产品可靠性和正确性的有效手段之一，而模型检测是一种确保设 计规范正确性的形式化自动验证技术。研究发现，模型检测中生成的反例 可有效应用于测试用例的生成，显著减少测试代价，提高软件质量。本文 主要研究基于模型检测的类测试自动生成技术。 本文分别采用数据流测试和变异测试的方法，并结合模型检测器j a v a p a t h f i n d e r ( 胂) ，将测试生成问题简化成模型检测中寻找反例的问题，提 出了两种面向对象软件测试用例自动生成的方法。 首先采用数据流测试的方法，通过设置陷阱性质，用时序逻辑公式表示 数据流测试的覆盖准则，提出一种自动生成测试用例的方法，并在j p f 上 实现。该方法满足数据流覆盖准则，适用于j a v a 类内方法问调用序列的测 试。算法分析与实验结果表明，通过设置适当的搜索深度，本文提出的算 法使得类数据流测试的覆盖率提高了8 ，并能发现隐藏在程序当中的错 误；通过本文提出的方法调用选择原则，可显著减少生成调用序列的长度； 与j p f 的d f s 算法相比，本文提出的算法减少了搜索过程中产生的冗余状 态，并及时进行了回退，在内存消耗基本相同的情况下本文算法生成的新 状态数减少了6 5 ，回退次数减少了9 0 ，处理的状态数减少了8 8 ，算 法的执行时间也减少了2 8 ，有效减少了测试生成的代价。 此外，基于变异测试的思想，采用类复制的方法，应用j p f 来保证软件 执行过程中产生的错误在输出结果中可见，自动生成满足变异覆盖准则的 测试用例，适用于类之间方法调用的测试，从而实现了j a v a 类之间的测试 用例自动生成。算法分析与实验结果表明，针对t r e e m a p 类的测试用例生 成实验，本文提出的方法覆盖了其中主要的面向对象特性，且生成的变异 数多达2 1 1 个，而反例数仅2 6 个就覆盖了1 0 0 的有效变异，显著减少了 测试生成的代价；与v i s s e r 提出的模型检测器j p f 上的符号执行方法相比， 在对t r e e m a p 类中的d e l e t e e n t r y 、f i x a f i e r d e l e t i o n 和f i x a f l e r i n s e r t i o n 三个 方法进行测试用例生成的实验中，本文提出的方法有效覆盖率达到了 1 0 0 ，覆盖率提高了约1 5 ，且本文提出的方法不依赖于程序结构的设计， 并能保证程序执行过程中出现的错误在输出结果中表现出来，以发现隐藏 的错误。 关键词：面向对象软件测试，模型检测，类内测试，类间测试，数据流方 法，变异方法 s t u d yo n t h ea u t o m 噙t i cc l a s st e s tg e n e r a t i o n t e c h n i q u e sw i t hm o d e l c h e c k a b s t r a c t t h eh i g h l yr e l i a b l es o f t w a r et e c h n i q u e 缸o n eo ft h ef o c u s e si nt h es o f t w a r et h e o r y s t u d ya n dt h es o f t w a r ee n g i n e e r i n gp r a c t i c e r e c e n t l y , m o r ea n dm o r ef o r m a lm e t h o d s h a v eb e e ne x p l o i t e df o rs o f t w a r eq u a f i t ys t u d y t h es o f t w a r et e s t i n gi so n eo ft h e e f f e c t i v em e t h o d sf o ra s s u r i n gs o f t w a r er e l i a b i l i t ya n da c c u r a c y , a n dt h em o d e lc h e c ki s m na u t o m a t i cf o r m a lv e r i f i c a t i o nm e t h o de n s u k a gt h ec o r r e c t n e s so fs p e e i f i c a t l o n sa n d c o d e s r e s e a r c h e ss h o wt h _ tt h ee o u n t e r e x a m p l ei nt h em o d e lc h e e ki sn ue f f e c ta p p l y i n g f o rg e n e r a t i n gt h et a tc _ s e 矗a n di tc a nr e d u e on o t a b l yt h et e s t i n ge o s ka n dh e i g h t e nt h e s o f t w a r eq u a l i t y t h 缸p a p e rm a i n l ys t u d i e st h et e c h n i q u e sf o ra u t o m a t i cg e n e r a t i n g c l a ut e s t e sb a s e dm o d e lc h e c k t h i sp a p e ri n t r o d u c e st h ed a t a - f l o wt e s t i n ga n dm u t a t i o nt e s t i n gi n t ot h em o d e l c h e e k e rj a v ap a t h f i n d e r ( j p f ) t r a n s f o r m st h ep r o b l e mo ft e s tg e n e r a t i o ni n t ot h eo n eo f f i n d i n gt h ee o u n t e r e x a m p l ei nm o d e lc h e e k , a n dd e s i g nt w om e t h o d st og e n e r a t e o r i e n t e d - o b j e e ts o f t w a r et e s t i n ga u t o m a t i c a l l y f i r s t ，b ya p p l i e dt r a pp r o p e r t i e sa n dt h et e m p o r a ll o g i cr e l a t i o n s h i p ，w ed e s i g nn s e a r c h i n ga l g o r i t h mt og e n e r a t et h e t e s ts e q u e n c e sa u t o m a t i c a l l y , a n di m p l e m e n ti tw i t h j p f t h ea l g o r i t h ms a t i s f i e st h ec r i t e r i o no fd a t a f l o we o v e r a g ea n dg e n e r a t e st e s t e sf o r m e t h o dc a l l i n gi nnj a v ac k i s t h ee x p e r i m e n t a lr e s u l t ss h o wt h a tt h ep r e s e n t e d a l g o r i t h me n h a n c e s8 e o v e r a g eb yt h er i g h ts e a r c hd e p t h , a n dc a uf i n dt h eh i d d e n f a u l t si nt h ep r o g r a m ，s h o r t e nt h ec a l l i n gs e q u e n c e sl e n g t hb yt h es e l e c t i o np r i n c i p l e si n t h em e t h o d sc a l l i n g c o m p a r e dw i t ht h ed f sa l g o r i t h mi nj p kt h ep r e s e n t e da l g o r i t h m d r o p st h ee x c e s ss t a t e sy i e l d e di nt h es e a r c hp r o c e s s a n db a c k t r a c k si nt i m e , i nt h ec _ 5 e o ft h eu m em e m o r y , t h en u m b e ro fn o ws t a t e sd e c r e a s e6 5 ，b a c k t r a c k sn u m b e r r e d u c e 帅，t h ep r o c e s s e ds t a t e sd r o pb y8 8 ，a n dr u nt i m e ss u b t r a c t2 8 t h e p r e s e n t e da l g o r i t h mr e d u c e sr e m a r k a b l yt h et e s tg e n e r a t i o n c o s t s e c o n d , b a s e do nt h em u t a t i o nt e s tt h e o r ya n dc l a s s - d u p f i c a t i o nm e t h o d , a n a u t o m a t i cg e n e r a t i o na p p r o a c ho ft h et e s tf o ri n t e r - c l a s si sp r e s e n t e da n di m p l e m e n t e d b ya p p l y i n gt h ej p ft om a k et h ep r o p a g a t i o no ff a u l t sb et h ev i s i b l eo u t p u t s t h e a l g o r i t h ma n a l y s i sa n de x p e r i m e n t a lr e s u l t ss h o wt h a tt h ep r e s e n t e da p p r o a c ho v e r l a y j i i t h em i no b j e e t - o r l e n t e df e a t u r ea n dy i e l d2 1 1m u t i n t sf o rt r e e m a pt h u s ，w eg o v e r a l l t h ev a f i dm u t a n t sb y2 1e o u n t e r e x a m p l e s , r e d u c et h et e s tg e n e r a t i o ne o s tr e m a r k a b l y ，c o m p a r ew i t ht h es y m b o l i ce x e c u t i o n m e t h o di nj p f p r e s e n t e db y v m s e r , t h ep r e s e n t e d 卸p m a e hr a i s e t h ec o v e r a g ea b o u t1 5 f o rd e l e t e e n t r y , f i x a f t e r d e l e t i o n a n d 6 x a n e d n s e r t i o nm e i h o d si nt r e e m a pe i n u ，t h ev a l i dc o v e g a g er e a c h1 0 0 f u r t h e r , o u r - p p m a c hd o e sn o td e p e n d o nt h ed e s i g no fp r o g r a ms t r u c t u r e , a n dm a k em 0 p r o p a 叠蛐o no f f a u l t sb et h ev i s i b l eo u t p u t s t of i n d i n gt h eh i d d e ne r g o l t l k e yw o r d s ：o b j e c t - o r i e n t e ds o f t w a r et e s t , m o d e lc h e c k , i n t e r - c l a s st e s t , i n t r a - c l a s st e s t , d a t a f l o wt e s t , m u t a t i o n t e s t ，1 盯大孽啊曩士掌位翟 文| l 于奢型检测的鼻涸试自动生l | 鼻术研究 1 1 软件测试与模型检测 第一章引言 随着软件在信息社会中发挥日益重要的作用，人们对软件可靠性、可靠安全性和保 密安全性等可信性质的要求也越来越高，如何在软件开发和运行中保证软件具有高可信 性质成为软件理论和技术的重要研究方向【l 】。 软件测试是软件工程理论中非常重要的一个方面，是提高软件产品质量和可靠性的 关键。测试用例的选择和生成问题是测试中的关键一环，测试用例的数量和质量决定了 软件测试的成本和有效性。随着现代软件的规模越来越大，其中的参数设置越来越多， 源程序代码超过百万行，参数设置上万个，而同时，因为软件的庞大，问题往往是并发 性的，每个b u g 可能导致致命灾难的几率也因此大大提高，更随着面向对象设计方法的 广泛应用，抽象，继承，重载，多态等面向对象程序的特性也给测试生成带来了更大的 挑战。如何设计并产生高效的测试用例，特别是面向对象程序的测试用例，一直是软件 测试领域研究的重点问题之一 形式化方法以一种严格的、数学的工程方法进行软件的开发，它作为一种思想、方 法、技术渗透到软件开发的各个活动中。形式化方法的实践证明形式化方法是提高软件 质量的重要途径。在从高层规范至最终实现的过程中，选用适当的、以形式化方法为基 础的工具进行辅助设计和验证，对提高安全攸关系统的可信度有很大帮助。 模型检测( m o d e lc h e c k i n g ) t 2 ，3 】是一种确保设计规范和代码正确性的形式化自动验证 技术。主要通过显式状态搜索或隐式不动点计算来验证有穷状态并发系统的模态命题性 质，并能在系统不满足性质时提供反例路径。模型检测需要对系统模型和待验证的性质 都进行形式化的描述。系统模型一般用有限状态机表示，性质多用形式逻辑表示。验证 工具根据系统模型和性质，给出满足或不满足的判断。 模型检测与测试相结合的研究，是近年来较为活跃的高可信软件理论和技术研究领 域之一大量实验表明，模型检测中生成的反例可有效应用于测试用例的生成，将模型 检测用于软件测试生成方法的研究，可以显著减少测试代价，提高软件质量。因此，基 于模型检测的测试用例生成方法的研究越来越受到研究人员的关注。 1 2 论文的主要工作 为了提高面向对象软件测试用例自动生成的有效性和效率，保证软件质量，本文将 模型检测这一形式化验证方法引入软件测试当中，主要研究了基于模型检测的面向对象 软件测试用例自动生成的方法。本文采用数据流测试和变异测试的方法，通过将测试生 广西大尊u 翼士鼍q 立论：乞| i 于模型捆喇的套嗣自簟生成技术研究 成问题简化成模型检测中寻找反例的问题，提出了两种基于模型检测器j a v ap a t h f i n d e r ( j p f ) 的面向对象软件测试用例自动生成的方法。 在数据流测试方法中，本文通过设置陷阱性质，用时序逻辑公式表示数据流测试的 覆盖准则，在类内部自动生成满足数据流覆盖准则的类中各方法的测试调用序列，从而 实现了j a v a 类内的测试用例自动生成。 另外，本文应用变异测试的思想，采用类复制的方法，使用模型检测器j p f 来保证 软件执行过程中产生的错误在输出结果中可见，自动生成满足变异覆盖准则的测试用 例，适用于类之间方法的调用，从而实现了j a v a 类之间的测试用例自动生成。 1 3 论文的组织 论文的主要内容可划分成以下几章； 第l 章：引言。介绍软件质量的重要性及形式化方法和软件测试等保证软件质量的 方法给出本文研究工作的动机与意义以及论文的组织。 第2 章：模型检测理论基础。介绍了模型检测技术的基本概念、常用的工具以及国 内外模型检测的研究现状和水平，最后还详细介绍了本文所采用的程序模型检测器j a v a p a m f i n d e r ( j p f ) 第3 章：软件测试用例自动生成方法。介绍了目前软件测试领域常用的测试用例生 成方法，阐述了模型检测方法在软件测试领域应用的优势及目前的研究现状和水平。 第4 章：基于j p f 的类数据流测试生成方法。本章通过设置陷阱性质，利用时序逻 辑公式表示数据流测试的覆盖准则的方法，提出了一种数据流测试与模型检测方法相结 合的测试用例自动生成的方法，实现了j a v a 类内的测试用例的自动生成。 第5 章：基于类复制变异的类问测试用例自动生成方法。根据状态机复制方法提出 一种基于类复制变异的测试用例生成方法，结合面向对象变异算子的选择，实现了适用 于j a v a 类间调用的测试用例的自动生成，且保证了测试用例执行过程中产生的中间错误 能在输出结果中体现出来。 第6 章：总结与展望。总结本文的工作和展望下一步的研究。 2 | i 于模堑喇的兵稿试自动生“晓爿u 开完 2 1 基本概念 第二章模型检测理论基础 模型检测【2 一】的研究始于八十年代初，当时c l a k e 和g m e r s o n 等人提出了用于描述 并发系统性质的c t l 逻辑，设计了检测有穷状态系统是否满足给定c t l 公式的算法， 并实现了一个原型工具。这一工作为并发系统的性质进行自动验证开辟了一条新的途 径，而随后的符号模型检测技术使得这一方法向实际应用迈出了关键的一步。模型检测 已经被应用于计算机硬件，通信协议，控制系统，安全认证协议等方面的分析与验证中， 取得了令人瞩目的成功。 模型检测是一种确保设计规范正确性的形式化自动验证技术。主要通过显式状态搜 索或隐式不动点计算来验证有穷状态并发系统的模态命题性质，并能在系统不满足性质 时提供反例路径。 模型检测的基本思想是用状态迁移系统表示系统的行为，用模态，时序逻辑公式 ( d 描述系统的性质。这样“系统是否具有所期望的性质”就转化为数学问题“状态迁移 系统s 是否是公式f 的一个模型? ”，用公式表示为d 产，对有穷状态系统，这个问 题是可判定的，即可以用计算机程序在有限时间内自动确定。 可见，模型检测需要对系统模型和待验证的性质都进行形式化的描述。系统模型一 般用状态迁移系统表示，性质多用模态时序逻辑公式表示。验证工具根据系统模型和性 质，给出满足或不满足的判断。 图2 - l 模型检测框架 f i g u r e2 - i t h es 打l l c t 呲o f m o d e lc h e c k 一个模型检测系统的实现过程都可概括为三个部分；建模、性质描述及检测验证。 建模是设计正确性要求。需要将系统表示为模型检测工具能够接受的形式化描述， 通常是有穷状态迁移系统。在形式化建模的过程中，往往需要对系统进行一定程度的抽 象，去除不会影响性质正确性却会使得验证过程复杂化的信息，如在验证通信协议的时 3 ，r 大掣蝎曩士掌位能丈l 亏q 鼻型喇的奢臼目试龟，生【| 生术研究 候，我们往往关心信息的传递而不关心实际的信息内容是什么。 性质描述是待验证的设计，通过模态时序逻辑公式严格地表述系统所要验证的性 质。模型检测只能检查模型是否满足给定的公式，因此所提供的公式能正确完整地表述 出所关心的性质是得到正确检测结果的必要前提。 检测验证给出了验证的过程。狭义的验证过程是指通过对状态空间的搜索过程来判 定系统地形式化模型是否满足所给定地性质，并在不满足的情况下提供相应的诊断信息 ( 通常是从初始状态到违背给定性质状态的序列) 。这部分工作可以由机器自动完成。广 义的验证过程包括搜索( 以及可能的反例生成) ，修改系统，再搜索，再修改的过程， 其中对于错误信息的分析和对系统的修改以及重新建模的工作需要用户的参与。 模态，时序逻辑是模型检测的基础。三种最常用的模态逻辑是计算树逻辑、命题线性 时序逻辑和命题演算。 将系统的运行看成是系统状态的变化计算树逻辑( c m p u t a t i o nt r e el o g i c ) 是 一种分叉时序逻辑。将系统状态变化的可能性表示成树状结构，可以用c t l 描述状态 的前后关系和分枝情况。 系统状态变化的可能性可以看成是一种树状结构，同时它又可以看成是所有可能的 系统初始状态经历各种可能变化的集合，也就是把一颗树看成是有限或无限条路径的集 合。一条路径所代表的是系统的一次可能的运行情况。命题线性时序逻辑 ( p l t l - p r o p o s i t i o n a ll i n e a rt e m p o r a ll o g i c ) 关心的是系统的任意一次运行中的状态以及 它们之间的关系。 p l t l 和c t l 的表达能力不同，各有各的长处。p l t l 模型检测的常用方法是将所 要检测的性质即p i ，公式的补转换成b i l c h i 自动机，然后求其与表示系统的自动机的 交。如果交为空，则说明系统满足所要检测的性质；否则生成一个反例，说明不满足的 原因。 系统状态的改变总是某种动作引起的。演算关心的是系统的动作与状态之间的 关系。演算的主要缺点是公式不易读懂( 由于最小、最大不动点的交错嵌套) ，其优点 是它的表示能力非常强。c t l 和p l t l 都可以嵌入到它的真子集中，并且相应的子集具 有与c t l 和p l t l 相同的复杂度的模型检测算法。 2 2 模型检测工具 模型检测器可分为符号模型检测器和显式状态模型检测器两大类，分别以s m v 和 s p i n 为代表。 s m v p 是美国卡耐基梅隆大学开发的模型检测工具用以检测一个有限状态系统是 否满足c t l 公式。它的建模方式是以模块为单位，模块可以同步或异步( i n 1 e a v i n g ) 组 3 - r 大尊啊蔓士葺巴1 盘论：乞i 亏叫隰捌r 涮的套调试自动生j t 掣u i u 卉完 合。模块描述的基本要素包括非确定性选择，状态转换和并行赋值语句。其模型检测的 基本方法是以二叉图表示状态转换关系，以计算不动点的方法检测状态的可达性和其所 满足的性质。 s p i n 5 】是美国贝尔实验室开发的模型检测工具。用以检测一个有限状态系统是否满 足p l t l 公式及其他一些性质，包括可达性和循环。它的建模方式是以进程为单位，进 程异步组合。进程描述的基本要素包括赋值语句，条件语句，通讯语句，非确定性选择 和循环语句。其模型检测的基本方法是以自动机表示各进程和p l t l 公式，以计算这些 自动机的组合可接受的语言是否为空的方法检测进程模型是否满足给定的性质。 随着对程序进行检测的需求，出现了耐s o r 、b l a s t 、b a n d e r a 、j p f 等程序模型 检测器，从而改变了模型检测只能对形式化规约语言建模的传统，使得研究人员不需要 单独抽象出一个系统行为描述，而直接将研究重点集中到了c ，c + + 和j a v a 等主流程序语 言实现的系统描述上。 v e r i s o f l t e 是美国贝尔实验室开发的一个用于系统软件测试的工具，其核心技术就是 模型检测技术可用于c ，c h ，t c l 等语言开发的软件系统的测试，注重程序的并发交 互。v e r i s o f t 的原型于1 9 9 6 年开发完成，并在p o p l 9 7 上第一次公开其设计内容。v e r i s o f t 是第一个使用实时调度的软件模型检测器。在过去几年里，v c r i s o f l 已经成功应用到一 些朗讯科技( l u c e n t t e c h n o l o g i e s ) 开发的软件产品的分析工作中。 b l a s t l 7 】是b e r k e l e y 开发的一个用于c 语言程序的软件模型检测工具，使用反例驱 动的自动抽象精化技术来构造一个抽象模型，以实现对程序的安全性质进行模型检测， 其抽象构造过程是o n - t h e - f l y 实现的。b l a s t 最大的特点是在模型构造、模型检测、模 型求精的循环过程中采用了懒惰抽象( l a z y a b s t r a c t i o n ) 技术i s 。目前，b l a s t 作为一 个插件已集成到了e c l i p s e 集成开发环境中 b a n d e r a l 9 是一个用于模型检测并发j a v a 程序的工具集，直接从j a v a 源代码中抽取 出一个统一模型，在不同转化器的作用下，再转化成s m v ，s p i n 等模型检测器的输入 语言，且实现了对j a v a 源代码的程序切片和抽象等技术。 j a v ap a t h f i n d e r 1 0 , i t j 2 1 是美国n a s a 开发的一个程序模型检测器。用以检测可执行 的j a v a 字节码是否满足某些指定性质，包括a s s e n i o n 和不确定异常。我们将在第4 节 中对j p f 进行详细的介绍。 另外还有在l i n u x 内核上运行的模型检测器c i v i c ”1 ；微软研究院设计的用于 w i n d o w s 操作系统驱动验证的工具s l a m 1 4 】等大量的程序模型检测工具。 2 3 模型检测研究进展 模型检测基于对系统状态空间的穷举搜索。对于并发系统，其状态的数目往往随并 发分量的增加呈指数增长。因此当一个系统的并发分量较多时，直接对其状态空间进行 搜索在实际上是不可行的。这就是所谓的状态空间爆炸问题。 l 亏叫鼻越柏喇的兵翎 白重生成技术研完 为了能够有效地应用模型检测方法，大量文献研究了在模型检测器中减少和压缩状 态空间的技术，以缓解状态空间爆炸问题。这些研究大多基于s m v 和s p 玳来进行 符号模型检测( s 灿l i em o d e lc h e c k i n g ) 技术起源于1 9 8 7 年美国卡耐基梅隆大学 m c m i l i 托教授的工作。它的基本思想是用布尔逻辑公式代替传统的邻接表来表示状态间 的迁移关系。有序二叉图o b d d ( o r d e r e db i n a r yd e e i s i o nd i a g r a m s ) 是用以表示逻辑公式 的重要手段，它能较为紧凑地表示状态间的迁移关系，以降低验证时存储系统模型所需 的内存空间。o b d d 与符号模型检测的结合，使得模型检测处理状态空间的能力达到 1 0 2 叱1 0 啪甚至更大【| 】。另外，状态迁移的计算也可以以集合为单位，以提高搜索的效率。 b i e 他等人在1 9 9 9 年提出的b m c ( b o n d e dm o d e lc h o k i n g ) 作为基于b d d 技术的符 号模型检测方法的互补，解决了很多b d d 无法解决的问题【闱。实验表明，在软件系统 的检测中，符号模型检测方法只适合于2 个并发线程的检测，而显式状态模型检测方法 则较适用于多个并发线程的检测【1 6 j 。 s p 玳【5 】是基于自动机理论【l7 】的显式模型检测工具，有大量的文献对其核心算法 t a 巧趾的环路检测算法进行了改进和扩展【l k l 】l 文献【2 2 】中提出了基于一个x m l 的工具a s p n ，对s p i n 进行了抽象扩展；借鉴人工智能领域的启发式的高效搜索方法， 文献 2 3 1 提出了一个新的模型检测器h s f s p i n ，在s p 玳的基础上实现了a ，i d a * 等 启发式算法和一个改进的嵌套d f s 算法，并在文献【2 4 】中在h s f s p 烈中通过计算汉明 距离和f s m 距离来减少一个已经存在的反例的长度，进行反例优化研究。启发式方法 的引入，不仅缓减了状态爆炸问题，而且可以减少生成反例的长度，达到反例优化的目 的，而启发式搜索算法只能用于系统查错，不能用于系统验证的特性，已足够满足模型 检测在软件测试生成上的需要。文献f 2 5 】也提出了一种最小化反例的思想和算法，并在 s p 玳中实现，但他们提出的算法需要重复多次访问状态，比较耗时。 在s m v 和s p n 的基础之上，人们还采用了0 n m e n y 技术、偏序规约技术、对称 规约技术和抽象技术等有效手段来缓解状态空间爆炸问题。 o n 也e f l y 技术是由v a r d i 等人提出的，有时也称为局部模型检测技术。它的基本原 理是不需要事先生成整个搜索空间，而是根据验证性质的需要来进一步搜索，以展开系 统路径所包含的状态，这就避免预先生成系统中所包含的所有的状态网。这种方法的一 个显而易见的优点是一旦验证算法找到一个反例，算法即可终止，而不必生成剩余的状 态空间，可以很好地解决内存不足和状态爆炸等问题。v a r d i 等人首先提出了基于自动 机的“o n n l c h y ”模型检测l t l ( 1 m 谢t 锄p o r a ll o g i c ) 时态逻辑描述的规范的算法【2 7 捌， 这也是s p 玳的核心算法之一随后，j a r d 等人提出了基于替代深度优先的“o n 劬e - f l y ” 模型检测方法网，这些算法能很好地解决内存不足和状态爆炸等问题。f e m m a d e z 等人 用基于深度优先的“0 n t h e f l y ”模型检测方法验证了d r e x 协议刚。c o u w e u r 等人在 广义b n c h i 自动机上实现了0 l m e - n y 空集的检测算法，解决了基于自动机理论对l t l 检测方法的关键操作【l 叼。结合1 蠲趾算法和c o u v r e u r 的广义b n c h i 自动机的相似算法， g e l d e n h u y s 等人提出了一种新的算法来实现在系统规约描述和b n c h i 自动机的乘积中搜 6 | l 于模蓦2 ；测的摹测试由曩，生月l 技术研完 索可接受环，并在检测了所有的转化后立刻报告了一个可接受的环，且可产生一个较短 的反例，这是嵌套式深度优先搜索算法所不能实现的网。h a m m e r 等人提出一种将m 公式转化成线性弱交替自动机( 1 i n e a r w e a k a l t e r n a t i n g a u t o m a t a ) 的算法1 2 ”，在运行时间 和内存消耗上与s p 琳相比都有很大的改进。 偏序规约技术( p a r t i a lo r d e rr e d u c t i o n ) 的基本思想是利用某种序关系，以减少重复验 证本质上相同的路径【3 “3 2 1 。一个系统可以由多个进程组成，并发执行使得不同进程的动 作可以有许多不同的次序，而这些不同的执行序列可能对于要验证的性质并没有本质上 的差异。基于这一认识，偏序规约技术考虑固定某些状态的次序，从而只需验证所有可 能执行路径集合中的一个子集即可。b o s n a c k i 等人提出一种利用宽度搜索优先( b f s ) 来改进s p i n y 4 中偏序规约技术的算法，该算法是在符号模型检测方法中的局部安全性 质检测算法的基础上改进的，并可在s p i n 中实现，有效提高了s p i n 的检测效率p ”。 p a l m e r 等人提出了在并行模型检测器上实现偏序规约技术的算法，有效减少了生成的状 态数并限制了网络节点中不必要的通信刚。 对称规约技术( s y m m e t r yr e d u c t i o n ) 的基本思想是基于进程间的对称性，利用状态 的结构来确定验证过程中出现的对称性，由于存储于同一个状态的各组件( 如进程，对 象) 顺序不影响系统后继的行为，两个对称状态的后继状态也是对称的，因此类似的进 程可能产生许多相同或相似的路径，这样只须验证在对称关系下等价的一种情况既可。 人们提出了很多标准来确定在没有后继状态信息的情况下，两个状态是否对称。d a m s 等人利用进程间的顺序，通信信道和时序逻辑公式的结构来表示正确的需求【3 5 】。s i s t l a 等人实现了一个叫做s m c 的系统，提出了利用进程对称和状态对称的方法o n - t h e - f l y 实现模型检测功能，一旦发现错误就及时停止搜索，加速了模型检测的进程并减少了内 存需求1 3 6 理想情况下，约减后的状态空间将只有一个状态对应一个对称等价的类型， 但是要检测出所有的对称关系，通常需要付出非常大的计算代价，这就消减了该技术的 约减效果。因此对称规约技术在实际工程中应用较少。 抽象技术( a b s t r a c t ) 的基本思想是通过把原来模型中与待验证的性质无关的信息去 掉而获得简化模型的方式来减小模型检测时问题的规模，以降低验证过程的时空消耗。 一个有效的抽象应该满足以下特征：第一，抽象必须是保持性质的，即若简化的模型满 足性质，则原来的模型亦满足该性质；第二，所产生的抽象模型要足够的小，这样才能 有效缓解状态空间爆炸问题，使得检测进程得以快速，顺利地完成；第三，所产生的模 型不能太粗糙，否则依然保留了过多的无关信息，不能有效保证检测过程。g a l l a r d o 等 人提出了一个基于x m l 的模型检测工具n s p i n ，在s p i n 的基础上对其输入语言 p r o m e l a 模型进行了抽象扩展圈h e n z i n g e r 等人提出了一种称之为懒惰抽象( l a z y a b s t r a c t i o n ) 的方法，基于抽象验证精化的过程来实现并优化针对c 语言的模型检测， 并在b l a s t 上实现了对安全性质的检验罔。c l a r k e 等人提出了一个基于反例的谓词抽 象精化方法框架，可自动生成抽象系统 3 7 1 。袁志斌等人对软件模型检测中的抽象技术进 行了较全面的综述网。 7 ，1 ，v 学习e e 尊啦论文| 玛曩型捌r 翊由囊薯_ 试自曩，生【| 术研究 一般来讲基于减少搜索空间的方法能同时节省时间和内存空间的需求。由于内存空 间在某些情况下比时间更为重要，有些方法的目标是以时间换空间。例如在s p i n 中实 现的压缩方法伫q 和用自动机表示可达状态的方法【蚓就是这样的方法。 2 4 程序模型检测器j a v ap a t h f i n d e r 2 4 1j p f 的发展 j p f 1 4 首先由美国n a s a 提出并开始，是一个用于j a v a 字节码的显式状态的软件模 型检测器。从非形式化的角度来看，j p f 也是一个j a v a 虚拟机，称为m c - j v m ( m o d e l c h e c k b a s e dj a v a v i r t u a l m a c h i n e ) ，但它跟普通的虚拟机不同，普通虚拟机只执行程序 一次，而从理论上来说j p f 执行所有可能的次数，沿着所有可能的执行路径来检查程序 是否具有死锁、不确定异常等性质。一旦它发现了一个错误，j p f 就提供反例来报告出 导致该错误的整个执行路径，而不仅仅是普通的调试器。 j p f 在1 9 9 9 年诞生时，只是作为一个j a v a 语言到s p i n 的输入语言p r o m e l a 语言的 转化器，使得我们能够使用s p i n 直接对j a v a 源程序进行模型检测，当时的j p f 已经能 够成功地在复杂j a v a 程序中查找并发现错误，但是对于p r o m e l a 语言不支持的语言特性 则无法表述出来，如浮点数，指针，引用等；到2 0 0 0 年，为解决p m m e l a 语言的约束 性，n a s a 的开发人员就独立开发出了一个j a v a 虚拟机，直接对j a v a 字节码进行检测； 并于2 0 0 3 年设计并最终实现了其自主开发的扩展系统结构，如图2 - 2 所示，j p f 在其虚 拟机之上，采用了库文件的抽象、性质检测器和选择生成器等优化机制，通过配置搜索 策略，对j a v a 的字节码程序进行检测，并最终生成验证报告，即模型检测方法中的反例。 8 g - 冒，叫曲习【b 孽啦论，：a t 于翱型糖涮的粪测试自动生【j t 术习门乞 虚拟机监听数据调度的启发 式方法 图2 - 2j a v a p a t h f i n d e r 的系统结构图 f i g u r e2 - 2 t h es y s t e ms l n l e t t w eo f j a v ap a t h f i n d e r 2 4 2 在应用程序中使用v e r i f y 理论上，j p f 可以用于任意j a v a 应用程序的检测，但通常都是针对应用系统的j a v a 模型来进行检测。这种情况下，在j a v a 应用程序中调用j p f 的a p i 函数对系统进行检 测是很有帮助的，即可从j p f 中获取信息，又能直接用于程序的执行上。这些i p f 的 a p i 主要集中在g o v n a s a j p f j v m v e r i f y 包中，本文将使用到的主要包括以下两种类型： 9 ，1 可大掌硬士拳啦截叩乞 | i 于模翌喇的冀- 铡试盲动生成技术研完 ( 1 ) 非确定数据生成器( n o n - d e t e r m i n i s t i cd a t ac h o i c eg e n e r a t o r s ) 一这是j p f 中主要 的a p i 类型，适用于模型检测器上测试驱动的开发。其设计思路是从j p f 中取得不确定 的输入数据值，这样j p f 就能系统化地分析所有的相关取值。在j p f v 4 之前只支持布尔 类型的值和整型值，在j p f v 4 中还增加了对浮点数值的支持： p u b l i cs t a t i cb o o l e a nr a n d o m b o o lo ；c = t r u e ，f a l s e ) p u b l i cs t a t i c i n tr a n d o m ( i n t m a x ) ；c = o ，l ，m a x p u b l i cs t a t i cd o u b l eg c t d o u b l e ( d o u b l er a i n , d o u b l em a x ) ；c = o o 这些a p i 按如下方式初始化测试驱动数据： i m p o r tg o v n a s a j p f j v m v e r i f y ； v o i d t e s t ( ) i n td a t a = v e r i f y r a n d o m ( 3 ) ；j p fw i l le x e c u t ef o rv a l u e s 【0 ，1 , 2 ，3 】 ， ( 2 ) 搜索限制( s e a r c h c o n s t r a i n t s ) l 这种类型可用于控制j p f 搜索的进程。为了能 用j p f 验证一个指定的应用，这是唯一一种限制状态空间的方法。这种类型包括有两个 方法：原子操作( a t o m i c i t yc o n t r 0 1 ) 和搜索剪枝( s e a r c hp r u n i n g ) 直接的原子操作主要在自动化以及o n - t h e f l y 的偏序规约实现之前使用： v e r i f y b e g i n a t o m i c o ； ，a l lc o d ei nh e r ei se x e c u t e db yj p fi no n et r a n s i t i o n v e r i f y c n d a t o m i c o ； ， 搜索剪枝用于特定性质的高层应用，当程序对指定性质的某些具体值不感兴趣的时 候使用该方法。 c o m p u t es o m ed a t a v e r i f y i g n o r e l f ( d a t a s o m e v a l u e ) ；p r u n es e a r c hi f t r u e | | 硒s o m es t u f f w i t hd a t a 如果提供的表达式为真，j p f 不再继续执行当前路径，且回溯到前一个不确定性选 择点进行新一轮的搜索。 2 4 3j p f 中解决状态爆炸问题的机制 理论上，显式状态模型检测是一个严格的、精确的方法