（计算机软件与理论专业论文）从测试规格说明到测试用例自动生成的方法.pdf

上海大学硕士学位论文 t h ep o s t g r a d u a t et h e s i so fs h a n g h a l u n i v e r s i t y 摘要 在软件测试过程中，测试用例的生成是软件测试的关键和难点。目前，测试 用例的生成主要靠手工完成，而且要求软件测试人员具有一定的经验和较高的专 业水平，因而，测试过程往往带有很大盲目性，致使测试效率低下，软件成本居 高不下，软件质量也很难保证。为此，迫切需要改进软件测试的方法，开发一些 测试用例的自动生成工具，提高软件测试效率，降低软件成本，保证软件质量， 提高软件测试的自动化程度。 形式方法是基于数学方法来描述目标软件系统性质的软件开发方法，它为系 统的说明、开发和验证提供了一个框架。软件规格说明是用形式规格说明语言精 确描述软件需求的文档。z 语言是目前比较流行、使用较为成功而有效的语言， 它是基于模型的形式化规格语言，它以一阶谓词逻辑和集合论作为形式语言基 础，将函数、映射、关系等数学方法用于规格说明之中，具有精确、简洁、无二 义性的特点，有利于保证程序的正确性，尤其适合于无法进行现场调试的高安全 性系统的开发。 本文以z 测试规格说明作为推导测试用例的依据，探讨了从z 测试规格说明 推导出测试用例的过程、方法和技术。所谓测试规格说明，是指从规格说明中的 输入变量前置条件表达式、输入输出变量基本约束条件以及输出函数抽取得到的 以析取范式形式存在的谓词序列。使用域测试策略生成测试用例的过程如下：将 测试规格说明变换成不等式组，然后对每一个不等式组利用1 l 域测试策略生 成域测试矩阵，最终得到测试用例包。本文提出了一种应用1 1 域测试策略和 线性1 j 等式值转换器来构成一个从测试规格说明生成测试用例的方法。 针对复杂谓词和非线性谓词难以产生测试用例的难点，本文在a k o sl l a j n a t 作基础上改进了现有的域测试策略，将原来属于白盒测试范围内的路径测试策 略运用于寻找谓词的上点一离点上，较好的解决了上述难点。 本文通过给出几个实例研究( c a s es t u d y ) ，说明如何使用l l 域测试策略以 及改进的域测试策略来实现从测试规格说明到测试用例的自动生成。 关键字：形式规格说明，测试规格说明，测试策略，1 】域测试策略，域测 试矩阵，测试用例 e 海大学硕士学位论文 t h ep o s t g r a d u a t e t h e s i so f $ h a n g h a lu n i v e r s i t y a b s t r a c t d u r i n gt h ep r o c e s so fs o f t w a r et e s t i n g ，t h eg e n e r a t i o no ft e s t c a s ei sc r i t i c a la n dd i f f i c u l t p r e s e n t l y ，g e n e r a t i o no f t e s tc a s ei sp r i m a r i l yd o n em a n u a l l y , r e l y i n gh e a v i l yo nt e s t e r s e x p e r i e n c e a n d c a p a b i l i t y ，w h i c h r e s u l t s i nl o w e f f i c i e n c y o fs o f a v a r e t e s t i n g ，h i g h c o s to fs o f t w a r e d e v e l o p m e n ta n du n c e r t a i n t yo f s o f t w a r eq u a l i t y c o n s e q u e n t l y , i m p r o v i n gt h em e t h o do f s o f t w a r e t e s t i n g a n dd e v e l o p i n gt o o l st h a tc a ng e n e r a t et e s tc a s e a u t o m a t i c a l l ya r e i nu r g e n tn e e d st o i m p r o v et h ee f f i c i e n c y a n da u t o m a t i o nd e g r e eo fs o f t w a r e t e s t i n g t ol o w e rs o f t w a r ec o s ta n d a s s u r es o f t w a r eq u a l i t y f o r m a lm e t h o d sa r ek i n do fs o f t w a r ed e v e l o p m e n tm e t h o d st h a tc a r ld e s c r i b et h ec h a r a c t e r s o ft a r g e ts o f t w a r es y s t e mw i t hm a t h e m a t i c sb y p r o v i d i n g af r a m e w o r kf o rt h e s p e c i f i c a t i o n ， d e v e l o p m e n ta n dv e r i f i c a t i o no f t h es y s t e m a n df o r m a ls p e c i f i c a t i o nl a n g u a g ei su s e dt od e s c r i b e s o f t w a r er e q u i r e m e n tp r e c i s e l yz ，as u c c e s s f u la n de f f e c t i v ef o r m a ls p e c i f i c a t i o nl a n g u a g ei st h e m o s tp o p u l a ro n ea t p r e s e n t i th a sf i r s t - o r d e rl o g i ca n ds e tt h e o r ya st h eb a s i sf o ri t s f o r m a l l a n g u a g e a n d a p p l i e s m a t h e m a t i c a lm e t h o d ss u c ha s f u n c t i o n ，m a p p i n g a n dr e l a t i o n i n t o s p e c i f i c a t i o n s f o ri t sp r e c i s i o n ，c o n c i s i o na n du n a m b i g u i t y , i ti sf i tf o ra s s u r i n gc o l t e c t d e s so f s o f t w a r e ，e s p e c i a l l yi nt h ed e v e l o p m e n to fh i g hs e c a r es y s t e m sw h e r en oo n t h e s c e n ed e b u g g i n g i sa v a i l a b l e i nt h i sa r t i c l e ，g e n e r a t i o no ft e s tc a s ef r o mzt e s ts p e c i f i c a t i o ni sd i s c u s s e da n dt h e p r o c e s s m e t h o da n dt e c h n o l o g ya l s od e t a i l e dt e s ts p e c i f i c a t i o nr e f e r st op r e d i c a t e ss e q u e n c e si nt h ef o r m o fd i s j u n c t i v en o r m a lf o r m ，e x t r a c t e df r o mt h ep r e c o n d i t i o ne x p r e s s i o no f i n p u tv a r i a b l e s ，b a s i c c o n s t r a i n t sc o n d i t i o no f i n p u t ，o u t p u tv a r i a b l e sa n di n p u tf u n c t i o ni nt h es p e c i f i c a t i o nt h ep r o c e s s o fp r o d u c i n gt e s tc a s e b yd o m a i nt e s ts t r a t e g yi sd e s c r i b e da sf o l l o w s ：t e s t s p e c i f i c a t i o n i s t r a n s f o r m e di n t oi n e q u a t i o ns e t s t h e n ，1 1d o m a i nt e s ts t r a t e g yi sa p p l i e dt oe v e r yi n e q u a t i o n s e tt op r o d u c et h ed o m a i nt e s tm a t r i x ，w h i c hi nt u r np r o d u c et h et e s tc a s ep a c k a g e am e t h o dt h a tg e n e r a t e st e s tc a s ef r o mt e s ts p e c i f i c a t i o nb y1 ld o m a i nt e s t s t r a t e g ya n d l i n e a ri n e q u l i t yc o n v e r t e ri si n t r o d u c e di nt h i s a r t i c l e e x i s t i n gd o m a i nt e s ts t r a t e g yi si m p r o v e d b a s e do na k o sh a j n a l sw o r kt ot a c k l et h ed i f f i c u l t yo fg e n e r a t i n gt e s t c a s ef o rc o m p l e xa n d n o n l i n e a r p r e d i c a t e ss u c c e s s f u l l yb yu s i n gp a t h t e s t s t r a t e g yb e l o n g i n g t ow h i t e 。b o x t e s t o r i g i n a l l yt os e a r c hf o ro np o i n t sa n do f fp o i n t so f p r e d i c a t i o n s t h ew a yo fa u t o m a t i c a l l yg e n e r a t i n gt e s tc a s ef r o mt e s t s p e c i f i c a t i o nb y1 1 d o m a i nt e s t s t r a t e g ya n di m p r o 、。c dd o t n a i nt e s ts t r a t e g yi sp r e s e n t e dt h r o u g hs e v e r a lc a s es t u d i e s k e y v v o r d s ：f o r m a ls p e c i f i c a t i o n ，t e s ts p e c i f i c a t i o n ，t e s ts t r a t e g y ，1 1d o m a i n t e s ts t r a t e g y d o m a i nm a t r i x t e s tc a s e 上海大学硕士学位论文 t h ep o s t g r a d u a t et h e s i so fs h a n g h a iu n i v e r s i t y 致谢 谨以此文献给关怀和帮助过我的所有人。 感谢我的导师缪淮扣教授对我的细心指导和精心培养。缪老 师严谨的治学态度和平易近人的品质给我留下了及其深刻的印 象，他在工作上一丝不苟的作风深深地感染和鼓舞了我，使我 在不断提高学识水平的同时也加强了独立思考的能力和迎难而 上的勇气。这将成为我今后人生道路上一笔巨大的精神财富。 感谢博士生刘玲在学习上给与的热情帮助和指导，她对系统 的实现提出了宝贵的意见。 感谢同课题组的研究生羊冬昭、曹晓夏和赵梅，四个人的通 力合作使得整个课题能在一种和睦的气氛下顺利完成。感谢杨 敏、汤艳艳同学在日常生活中给予我的照顾和关心。 深深地感谢多年来一直给予我巨大关怀和鼓励的父母。 最后，感谢国家自然科学基金和上海市教委科技发展基金对 本课题的资助。 上海大学硕士学位论文 t h ep o s t g r a d u a t et h e s i so fs h a n g h a iu n i v e r s i t y 第一章软件测试介绍 1 1 软件测试概述 随着信息技术的飞速发展，计算机已广泛应用于国民经济和国防建设中的许 多重要领域，如：航空、航天、工业控制、交通、银行和军事指挥自动化系统等。 这类应用对软件提出很高的质量要求，因为即使很小的软件错误也可能导致整个 系统的崩溃，造成极大的经济损失。如：1 9 9 6 年6 月阿里亚娜火箭发射时因软 件故障导致升空失败，使欧共体蒙受了2 5 亿美元的损失。软件质量己成为制约 计算机应用的主要因素之一。 鉴于软件质量问题的重要性和迫切性，人们提出各种方法和技术来提高软件 质量，如形式方法、面向对象方法和软件测试技术等。软件测试作为保证软件质 量的关键技术之一，能够有效地发现软件中的故障。在整个软件开发过程中，软 件测试占有举足轻重的地位。根据b o e h m 的统计，软件开发总成本中，用在测试 上的开销要占3 0 到5 0 。根据1 9 8 3 年i e e e 提出的软件工程标准术语中给软件 测试下的定义，所谓软件测试，就是“使用人工或自动手段来运行或测定某个系 统的过程，其目的在于检验它是否满足规定的需求或是弄清预期结果与实际结果 之间的差别”。这就非常明确地提出了软件测试以检验是否满足需求为目标。 通俗的讲，软件测试就是选择有代表性的输入数据来驱动被测程序，观察程序的 执行结果，比较该结果与期望结果是否一致，然后做相应的纠错、调整和评价。 参看图1 1 。 程序 测 图1 1 软件测试示意图 结果l 二j测试结果 结果2 上海大学颁士学位论文 ! ! ! ! q ! ! 鱼! 1 2 1 盟! ! ! ! ! 堕q ! ! 曼! 型鱼! ! ! ! 型! ! ! ! 坚! 注：测试数据驱动被测程序，得结果1 ，此为实际结果。测试数据驱动软件 规格说明，得结果2 ，此为预期结果。两者相比较，就可知道测试是否满足了需 求的目标。 这也就意味着一个大型的程序开发完成以后，软件开发工作并未结束，因为 后面几乎还有相当一部分工作要做，也就是说，还要进行程序的测试。软件测试 是保证软件质量的重要手段。 1 2 软件测试方法分类 1 2 1 静态方法和动态方法 原则上讲，可以把软件测试方法分为两大类，即静态方法和动态方法。静态 方法又叫静态分析，其主要特征是不利用计算机运行被测试的程序，而是直接分 析软件的形式和结构。静态分析主要是对被测程序进行特性分析，它工作起来象 一个编译器，也要随着语法分析的进行做特定的工作。利用静态分析可以对程序 作结构图、分析程序的控制流、度量软件的静态质量等。 常用的一些静态分析方法有如下几种： 收集一些程序信息，以利于查找程序中的各种欠缺和可疑的程序结构； 从程序中提出语义的或结构要点，供进一步分析： 以符号代替数值求得程序的结果，便于对程序进行运算规律的检验； 对程序进行一些处理，为进一步动态分析做准备； 动态方法也叫动态分析，它与静态分析相反，在测试时要运行被测程序，然 后根据运行结果来检验程序的性质。比如，测定软件的覆盖率、检查内存使用有 街渗漏和违例、跟踪程序的异常终止等等。实现动态分析的关键技术是程序插装。 程序插装是借助于插入到源程序中的监控语句来收集执行信息以达到揭示程序 内部行为和特性的目的。它是用来查找静态分析不能找到或不易找的错误的主要 动态分析工具。程序插装的工作分为三个阶段： 预处理阶段。这一阶段的主要操作是向源程序中插入特定的语句。这个 阶段的工作可以与静态分析同时进行，在语法分析到特定位置时插入特 定代码。 编洋执行阶段。对插装后的程序进行编译和执行。 后处理阶段。把程序执行过程中统b t 的数据与源程序匹配，作出报告图 表，包括覆盖报告。 动态分析的关键在于如何得到测试数据和期望的正确输出，黑盒测试方法平“ 上海大学硕士学位论文 t h ep o s t g r a d u a t et h e s i so fs h a n g h a lu n i v e r s i t y 白盒测试方法是两种通用的动态方法。 1 2 2 黑盒测试和自盒测试 黑盒测试与白盒测试是广泛使用的两类测试方法。 黑盒测试( b l a c k b o xt e s t i n g ) 又称功能测试、数据驱动测试或基于规格 说明的测试( s p e c i f i c a t i o n b a s e dt e s t i n g ) 。用这种测试方法进行测试时，被 测程序被当作打不开的黑盒，因而无法了解其内部构造。在完全不考虑程序内部 结构和内部特性的情况下，测试者只知道程序输入和输出之间的关系，或是程序 的功能。他必须依靠能够反映这一关系和程序功能的需求规格说明书确定测试用 例，并推断测试结果的正确性。即所依据的只能是程序的外部特性。因此，黑盒 测试是从用户观点出发的测试。 白盒测试( w h i t e b o xt e s t i n g ) 又称结构测试、逻辑驱动测试或基于程序 的测试( p r o g r a m b a s e dt e s t i n g ) 。采用这一测试方法，测试者可以看到被测的 源程序，他可以分析程序的内部构造，并且根据其内部构造设计测试用例。这时 测试者可以完全不顾程序的功能。 这两类测试方法是从完全不同的起点出发，反映了事物的两个方面。两类方 法各有侧重，在测试的实践中都是有效和适用的。在进行单元测试时大都采用白 盒测试，而在确认测试或系统测试中大都采用黑盒测试。 1 3 软件测试研究的相关工作 7 0 年代以来，软件工作者对测试工作越来越重视，到了7 0 年代中期，软件 测试技术的研究达到高潮。j b g o o d e n o u g h 和s lg e r h a r t 首先提出了软件 测试的理论，从而把软件测试这一实践性很强的学科提高到理论的高度，被认为 是测试技术发展过程中具有开甜陛的t 作。此后4 ：久，著名测试专家w e h o w d e n 指出了上述理论的缺陷，并进行了新的开创性工作。以后，又有w e y u k e r 和 o s t r a n d ，g e l l e r ，以及g e r h a r t 进一步总结原有的测试理论并进一步加咀完善， 使软件测试成为有理沦指导的实践性学科。 在软件测试的理沦迅速发展的同时，各种高级的软件测试方法也将软件测试 技术提高到了初期的原始方法无法比较的高度。j gh u a n g 提出了程序插装 ( p r o g r a mi n s t u m e n t a t i o n ) 的概念，使被测程序在保持原有逻辑完整性的基底 上，插入“探测仪”，以便获取程序的控制流和数据流信息，并可得到测试的覆 盖率。wb h o w d e n 对测试路径进行了深入的分析，提出了系统功能测试及代数 测试等概念。w e h o w d e n 、i ，a c l a r k e 和j a d a r r i n g e r 等人把符号执行的 上海大学硕士学位论文 t h ep o s t g r a d u a t et h e s i so fs h a n g h a iu n i v e r s i t y 概念引入到软件测试中，提出了符号测试方法，并且建立了d i s s e t 等符号测试 系统。w o o d w a r d 和h e d l e y 等人分析了路径测试中的藕联效应假设，并以此为基 础发展出基于程序变异( p r o g r a mm u t a t i o n ) 的测试方法，使传统的测试技术领 域增加了新的成员一错误驱动测试。1 9 7 7 年l o s t e r w e i l 和lof o s d i c k 等 人首先引入了数据流测试方法，该方法通过对数据流的静态测试找出程序中潜藏 的错误。o s t e e r w e i l 还把这一方面推广到并发程序的数据流分析。1 9 8 3 年日本 学者r y e i e h ih o s o y a 等在数据流测试方法中加入了变量值域分析，使数据流方 法检测的错误类型更多。 如何确定测试数据，选取测试点，仍然是实施测试，提高测试效率和查错命 中率的关键问题。l w h i t e 和e c o h e n 提出了一种新的计算机程序测试策略， 这就是域测试方法( d o m a i nt e s t i n gs t r a t e g y ) 。输入域分析是把程序的输入按 谓词划分，进一步以此划分为依据，给出各个域的测试点。e j f f e y u k e r 和t j o s t r a n d 接着发展了他们的方法。1 9 8 5 年d j r i c h a r d s a n 和l ac l a r k e 在此 基础上又提出了划分分析的概念，将形式规格说明和程序本身的输入变量的取值 范围都划分为域，找出共同的域，通过在这些共同域上的测试找出规格说明和 程序之间的不一致性。l a c l a r k e 还深入讨论并改进了w h i t e 和c o h e n 提出 的域测试方法。此外，s r e d w i n ej r 总结了一套工程化测试方法。 在面向对象的软件测试方面，也出现了不少新的测试方法和技术。其中不少 研究人员在基于规格说明的测试方面做了大量的研究工作，包括从单个操作来生 成测试用例，有限状态机的生成，预测的生成等等。b o s m a n 和s c h m i d t 使用有 限状态机来测试类，该方法首先从面向对象分析和设计时所用的状态图生成状态 机，然后将被测类模型化为此状态机。d o o n g 和f r a n k 在测试类时所采用的方 法则是从类的代数规格说明来半自动化的生成测试用例并且从类接口的规格说 明中自动生成测试驱动器。t u r n e r 和r o b s o n 的基于状态的测试技术同样使用了 有限状态机来生成测试用例，有限状态机用来模型化一个类的内部表示。也有许 多类测试的框架并不使用形式规格说明，例如d k u n g 等提出的面向对象的测试 和维护环境( o b j e c t - o r i e n t e dt e s t i n ga n dm a i n t e n a n c e ，o o t m ) 。o o t m 使用 了一个数学定义的测试模型，这个测试模型是从源代码生成的。o o t m 的f i 足之 处是仅仅支持基于程序的测试。 近年来，尽管软件测试技术有了长足的进步，但总的来说，仍然和软件开发 实践提出的要求有相当大的距离。测试手段的进展睦i 远远没有达到令人满意的程 度。 上海大学硕士学位论文 t h ep o s t g r a d u a t et h e s i so fs h a n g h a fu n i v e r s i t y 1 4 软件测试常用工具 为了提高软件测试的效率，加快软件开发过程，一些测试工具相应问世。有 些测试工具用以检查规格说明书的一致性和完整性，有的用以检查编码的静态特 征，也有些则支持已提出的测试方法。r e f a i r l e y 曾经系统地论述了软件工 具的作用，重点介绍了a d a 支持环境。lg s t u c k i 所设计的程序评估和测试器 p e t 能够自动进行f o r t r a n 程序的测试，并能给出测试覆盖信息。r x v p 原是用于 检查f o r t r a n 程序静态错误的，扩充咀后的r x v p8 0 能兼顾f o r t r a n 和c o b o l 的程序测试。类似工具还有c v r a m a m o o t h y 教授指导开发的f a c e s 和l t o s t e r w e i l 等人开发的d a v e 系统。h k a o 和t c h e n 开发了支持c o b o l 数据流 分析的工具。 有关动态测试的工具的开发更为普遍，其中的一部分工作力图自动产生测试 数据，比如s m o t l 测试编译程序的工具，以及一些支持符号测试的工具s e l e c t ， d i s s e c t ，a t t e s t 和$ a d a t 等。e h 于模块测试时需要用到驱动模块和桩模块，一 些模拟测试环境的工具出现了，如r g ，h a m l e t 设计的t e s t m a s t e r 系统和n ， p a u z l 设计的a u t 。 不久前，c w i l s o n 和l j o s t e r w e i l 提出了支持c 程序数据流分析工具 o m e g a ，主要解决了c 程序中指针引用的测试问题。e f m l l e r 设计了交互式 测试环境i t b 。接着出现的有m a h e n n e l 和d h e d l e y 开发用于p f o r t 语言程 序的l o r a 软件测试环境以及bm o n t e l 等人设汁测试p e t r i 网的软件包o v i d e 。 在面向对象的测试方面，m u r p h y 等开发了工具a c e 来对c + + 类和簇进行测试。 由d o o n g 和f r a n k 开发的a s t o o t 系统，也提供了一系列的工具来支持从类接口 规格说明中自动的产生测试驱动器和从代数的类规格说明中半自动的产生测试 用例。 上海大学硕士学位论文 t h ep o s t g r a d u a t et h e s i so fs h a n g h a lu n i v e r s i t y 第二章基于规格说明的软件测试 2 1 规格说明的种类 测试中最重要的因素是实际测试本身，规格说明由于清楚地描述了系统的功 能，显然可以作为黑盒测试的来源。规格说明可以分为非形式规格说明和形式规 格说明两种。下面首先考虑利用非形式规格说明进行的测试。 在软件测试中，这两种规格说明中的任一种都是有用的，目前来说，大部分 规格说明是非形式的规格说明。这些非形式规格说明主要由自然语言语句和些 用于增强说明性的图形图表构成，因而，在测试中使用这样的规格说明时必须要 作一些辅助工作，这些工作的主要目的是找出规格说明中的关键元素。另外，考 虑从非形式规格说明来推导测试时，还要注意到规格说明的大小和不精确性以及 规格说明中各元素之间的较弱的联系。所以工具支持是考虑的主要问题。“1 中描 述了一种管理从非形式规格说明得到的测试的工具。该工具的主要功能是解释规 格说明中的各部分阻及记录规格说明中的各部分和由它们推导出的测试之间的 关系。类属分割”+ “是用于基于自然语言规格说明的测试的一种比较好的方法。 使用这种方法时先要分析规格说明来决定各个功能单元，对每个功能单元找出相 关的参数和环境变量，并且根据类属进行划分。然后，测试者根据经验找出每一 类的有代表性的输入构成测试数据。这种方法的优点在于定义了测试规格说明语 言t s l ，可以用它来自动构造测试序列和执行测试。 很显然，使用这种方法时的主要工作是从非形式规格说明中抽取有用的信 息，这一点对于形式规格说明来说是非常容易的。我们的研究重点是基于形式规 格说明的测试。下面先简单介绍形式方法以及形式规格说明。 2 2 采用形式规格说明的原因 2 2 1 形式方法 2 2 1 1 形式方法简介 形式方法是在“软件危机”出现以后所出现的种软件开发方法，它的基奉 思想是对系统建立个数学模型，研究和提供一种基于数学的和形式语义学的软 上海大学硕士学位论文 t h ep o s t g r a d u a t et h e s i so fs h a n g h a lu n v e r s i t y 件规格说明语言，用这种语言严格地描述所开发软件的功能，然后将它转换成可 以执行的代码，最后证明实现的代码是否符合其规格说明。 用形式方法开发软件可提高软件系统的正确性和可靠性，并可提高软件开发 的效率。该方法日益受到计算机界和工业界的高度重视，并得到越来越广泛的应 用。著名的欧洲e s p r i t 项目的l a r g ec o r r e c ts y s t e m 、美国h p 公司的a n a l y s i s i n f o r m a t i o nl i b r a r y 、德克萨斯的c o m p u t a t i o n a ll o g i ci n c 开发的v i p e r ( v e r i f i a b l ei n t e g r a t e dp r o c e s s o rf o re n h a n c e dr e l i a b i l i t y ) 等都使用了 形式方法。 因此，形式方法在测试中最杰出的用途是用来产生黑盒测试集。 2 2 1 2 形式方法的主要优点 形式方法的优越之处在于其严格的数学基础与描述性。在软件开发过程中应 用形式方法具有如下优点“】： i 形式规格说明是无歧义的。 2 由误解引起的错误减少。 3 形式规格说明易于系统实现。 4 能够对形式规格说明进行正确性证明。 基于以上分析，我们可以明白为什么形式方法受到日益的重视和应用。尽管 就目前而言，大部分规格说明仍使用非形式的方法来书写，但随着人们认识的不 断提高以及软件工程的全面实施，形式规格说明终将代替非形式规格说明。 2 2 2 形式规格说明语言z 已有的形式方法采用的是形式规格说明语言。在用某种程序设计语言具体实 现日标软件系统之前先准备一个严格的形式规格说明。规格说明指明目标软件系 统“做什么”，而不考虑“怎么做”。规格说明语言有许多，例如z ”1 、v d m ”j 、o b j ”1 、 l a r c i i “等。1 i 同的规格说明语言在表达能力、术语以及支持形式处理的能力方 面有所不同，每种语言的侧重点也1 i 同，均针对所产生的背景而设计其特制性。 语言的设计范围也很广，从通用的到专用的，从具有较高表达能力的到有某些限 制的，从多态的到不可变类型的。 我们的研究工作是针对z 语言的。z 语言是7 0 年代末至8 0 年代初由英国 o x f o rd 大学程序设汁研究组p r g ( p r o g r a n n i n gr e s e a r c hg r o u p ) 的j e a nr a y m o n d a b r i a l 、b e r n a r ds u f r i n 等人设计的。在它的早期发展阶段，就得到了应用， 尤其i b m h u r s e y 子公司用z 来对他们的客户信息控制系统( c i c s ) 进行了规格 上海太学硕十学位论文 t h ep o s t g r a d u a t t h e s i so fs h a n g h a iu n i v e r s i t y 说明的重写，降低了软件开发费用。这对z 语言的发展产生了较大的影响。在 9 0 年代初，人们已经定义出了z 的标准文本。 z 语言是基于一阶谓词逻辑和集合论的形式规格说明语言，用于软件系统功 能的描述。称z 为形式语言是由于它采用了严格的数学理论。这样可以产生简明、 精确、无歧义且可证明的规格说明。同其它规格说明语言相比，z 一个主要的特 点是可以对z 规格说明进行推理和证明，这种特点使得软件开发人员或用户能够 很快找出规格说明的不一致、不完整之处，使他们提高对软件的信心。 z 语言最主要的结构是模式，每个模式由变量说明和谓词两部分组成。模式 可分为状态模式和操作模式。 以镪缓疑是对系统的状态空间及其约束特性的描述，是系统最基本的模式， 它定义了一个系统的本质特征。如一个用来汜录单位内部电话情况的小型数据库 系统( 简称小型电话系统) 可用图2 一l 的模式来描述这个系统的状态。模式上 方为声明部分，p e r s o n 是人的集合，p h o n e 是电话号码的集合，变量t e l e p h o n e s 是一个从p e r s o n 到p h o n e 的关系。模式下方为谓词部分，状态模式的谓词给出 了状态不变式，它决定了这个系统的约束是d o mt e l e p h o n e m e m b e r s ，即在这 个小型电话系统中拥有电话的人必须是这个单位的职员。 p e r s o n ，p h o n e 圈2i 小型电话系统的状态模式 嫠詹镆：靛义了系统在状态空问上的操作。它描述了该操作所要满足的条件 以及前系统状态和操作后的系统状态之间的关系。如查询电话号码的操作模式见 图2 - 2 。 囝2 - 2 盘酗i 也 号码的操作模式 在模式声明部分，兰p h o n e d b 表明系统状态不发生改变。n a m e ? 为输入变量 上海夫学硕士学位论文 ! ! ! ! q 盟! 坠! 型竺! ! ! ! ! ! ! 殳! ! ! ! 型鱼! 皇! ! 型! ! ! ! ! ! ! n l b e r ! 为输出变量，谓词部分的前一个式子是表示输入变量的前置条件。即进 行一个操作时输入变量要满足的条件。后一个式子反映了输入、输出之间的约束 关系。关于z 语言的细节可参阅文献 5 。 2 3 1 分类 2 3 基于形式规格说明的测试 本节中将介绍形式规格说明。形式规格说明有过程代数规格说明、代数规格 说明和基于模型的规格说明等。不同的形式规格说明支持不同的测试推导方法， 这些方法互为补充。 1 过程代数规格说明 从现有的资料来看，关于从过程代数规格说明推导测试主要考虑的是协议的 测试。利用过程代数推导测试中的关键是路径分析。过程代数助记符定义了有标 记的转换系统，该系统用来显示一个系统是怎样从一个状态变到另一个状态，而 不考虑这些状态的细节。因而，可以非常高效地产生大量的测试集。 2 代数规格说明 代数规格说明的好处在于容易构造测试数据。规格说明的构造性显示了怎样 建立已经定义的数据类型的实例并略含了测试序列化信息，利用这种规格说明可 以自动产生测试用例。目前，关于利用代数规格说明推导测试的研究已经比较深 入。 3 基于模型的规格说明 与过程代数相反，关于从基于模型的规格说明推导测试数据的文章较少。基 于模型的规格说明在测试推导方面的优点在于有关的数据和它们之间的关系有 清楚的定义。数据对操作的影响通常是明显的，这有助于说明怎样进一步划分输 入输出空间。基于模型的规格说明的测试的研究要比基于代数规格说明的测试 迟，目前还没有受到很多人的注意。对这一问题的解释是基于模型的规格说明是 不能执行的并且也1 i 一定具有构造性，从而限制了从规格说明自动产生测试用例 的能力。尽管如此，从基于模型的觌格说明进行测试仍然可以得到一些非常有益 的结果。 上海大学硕士学位论文 t h ep o s t g r a d u a t et h e s i s0 fs h a n g h a iu n i v e r s i t y 2 3 2基于形式规格说明的测试的构成 基于规格说明的测试和一般的测试一样也包括驱动测试和支持测试两个方 面。驱动测试是与推导测试用例有关的工作，测试中的驱动行为就是那些与决定 测试和测试结果有关的行为。而支持测试是与评估软件有关，用来改善和判断测 试组的总体质量的工作。没有充分的支持工作，测试的价值总是令人怀疑的。 2 3 3 基于规格说明的测试策略 常用的测试策略 常用的测试策略有随机测试、等价划分、定义域测试、基于错误的测试、变 异测试等等。 随机测试 随机测试中_ i 对输入定义域进行进一步的划分，直接从输入空间随机产生测 试数据。是一种比较简单的测试方法”。1 。 等价划分 软件测试中有很多等价类划分的方法”“，这些方法的一个共同点就是 将输入定义域划分成一些子定义域，使得这些子定义域中的每个元素有同样的检 查错误的能力。不同的是每种方法采用的指导划分的原则不同。一个常用的划分 方法是因果测试，这种方法根据不同的输出情况( 结果) 来决定不同的输入情况 ( 原因) 从而形成输入定义域的划分。 定义域测试 定义域测试对于测试具有线性输入空间的系统来说是一种非常成功的技术 “。利用这种方法进行测试时，首先要分析程序的控制流，然后根据线性定义域 的边界将输入空间划分成子定义域，出现程序控制流中的错误将会导致这些边界 偏离正确的位置。根据定义域测试，可以选取最少的点来保证检测到边界的偏移。 基于错误的测试 基于错误的测试”“4 i 是一个单独的测试策略而是一个广泛的测试策略集。 基于错误的测试的共同点就是显示程序中不存在某些众所周知的错误。这些众所 周知的错误包括不正确地使用关系操作符( 例如，在应该用“ = 、 ， = ，( ，f 0 f ft b o u n d a r y + d e l t a 。t b o u n d a r y o f ff b o u n d a r y d e l t a ( 2 t ；b o u n d 鞋。o o f ff 的n n 姆y + d e 醚8 二 t b o u n d a r y 0 f ffb o u n d a r y + d e l t a o f ff b o u n d a r y d e l t a 注：( 1 ) d e l t a 为人为指定的值，根据不同的数据类型其值也不同。当变量为整 型时，d e l t a = l ，当变量为浮点型时，d e l t a = o 0 0 0 0 0 1 。 ( 2 ) 如果边界值为实数，变量为整型，就会发生边界类型与变量类型不匹配， 例如，x 4 3 ，x 是整型。所以根据上表取得上点一离点后还需要进行处理。对( 、 = ) ，取得的值需要向下取整；对( = ) ，取得值需要f f 取整：对( 、 = ) ，取得值需要向上取整。 对( = ) ，报错! ( 小数点后均为0 除外) 当变量是非标量类型时，就叫i 可以利用表中公式产生上点离点以及内点了。 根据域测试标准，当变量是串类型，若b o u n d a r y 为s t r i n g ，则o n 与o f f 中必 有一个为s t r i n g ，另一个与它只有一字之差；若变量为布尔类型，则o n 与o f f 上海大学硕士学位论文 t h ep o s t g r a d u a t et h e s i so fs h a n g h a iu n i v e r s i t y 分别是t r u e 和f a l s e ；若变量为枚举类型，例如e n u m f a b ，c ，则o n 与o f f 必 有一个落在这三个字母之外，一个等于三个字母中任意一个。 2 复杂边界情况 肖一个边界条件使用两个或两个以上的变量，那么可以通过解相关等式找到 上点一离点。一般地，假如有k 个独立变量( 在右边的变量) ，就有k 个上点。插 入任意独立变量的组合，它使该断言( 边界等式) 为真，而不使其它的边界条件 为假。一般通过取独立变量的中点值，按该值解方程，然后保持独立变量的值不 变，最小可能地改变解的值使条件为假得到一个离点。 例如：y 1 4 o - x ，x ： 0 ，1 0 i n t e g e r 类型，y ： 1 0 ，1 0 0 f l o a t 类型。 边界条件中有两个变量，为求出y 的上点和离点，需要插入独立变量x 的值，使 该条件为真，而不使其它的条件为假。 当x 取4 到1 0 之间的任意整数时，满足上述要求。因此将x 的中间点7 代 入y 2 1 4 o - x ，可得y = 7 。因为 o ) ( y = 1 4 0 - x ) 八( x = l ，0 ) 八( y o ，显然是不能解y 、 = ， ，b 就称为内边界；如果运算符号卵属于 )