（计算机软件与理论专业论文）基于模型的规格说明测试方法的研究.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 iu n i v e r s i t y 摘要 形式规格说明语言基于严密的数学和逻辑，它是精确的，无二义性的语言。 形式规格说明语言克服了非形式化语言的二义性，但是它并不能完全避免规格 说明中的人为错误。本文研究的是形式规格说明的测试方法。通过研究和比较， 测试相比其他形式规格说明的验证方法需要较少的人力、物力，却能达到很好 的检测效果。在实际的应用中，测试相比其他的验证方法有更多的工具支持。 本文所研究的是基于模型的形式规格说明的测试方法。 常见的基于模型的形式规格说明语言包括z ，o b j e c t - z 和v d m ，这些基于 模型的规格说明语言都是以谓词公式来描述系统功能的。本文提出了从两种角 度对基于模型的形式规格说明进行测试：基于谓词错误的测试方法和基于谓词 结构的测试方法。 基于谓词错误的测试方法假设形式规格说明的前置条件存在已知类型的谓 词错误。本文提出的测试方法是通过选取合适的测试用例使得假设错误的谓词 公式和假设正确的谓词公式的结果是异或的，发现前置条件的错误。基于两类 谓词错误：表达式否定错误( e x p r e s s i o nn e g a t i o nf a u l t ) 和表达式多余错误 ( e x p r e s s i o nu n w a n t e d f a u l t ) ，本文分别提出了两种不同的测试准则：e n f 测试 准则和e u f 测试准则。e n f 测试准则可以帮助测试人员构造测试用例，发现 规格说明前置条件中的e n f 错误。相对的，e u f 测试准则可以发现前置条件 中的e u f 错误。基于谓词错误的测试方法可以覆盖谓词公式中所有一类错误的 可能性，保证形式规格说明前置条件相对正确性。 基于谓词结构的测试方法是基于覆盖的测试准则。测试人员知道规格说明 的前置条件和后置条件，对规格说明进行结构性的覆盖度测试。本文提出了5 种不同的覆盖度准则。基于不同覆盖度准则的测试用例可以对形式规格说明的 谓词部分有不同的覆盖度。 在测试领域中，测试的自动化是非常重要的。测试自动化是为了节省测试 的成本以及简化测试的过程。本文基于谓词错误的测试方法，研究并开发了一 套应用于基于模型的形式规格说明的测试工具p r e d t e s t i n g 。它可以简化测试的 过程，使测试用例生成的过程自动化。p r e d t e s t i n g 是基于j a v a6 0 和s w i n g 图 形界面的图形化测试工具。该工具可以把测试用例导出为标准的x m l 文件格 式。本文详细介绍了该工具的基本架构、设计和实现。最后，本文通过一个实 例来演示工具的使用。 关键字：软件测试，形式规格说明，谓词公式，定理证明，覆盖度测试 第1 页 上海大学硕士学位论文 1 - d ep o s t ( 球a d u p ( r e1 h e s i so fs h a n g h a iu n i v e r s r i y a b s t r a c t f o r m a ls 1 ) c c i f i c a t i o nl a n g u a g e sa r ep r e c i s e ，u n a m b i g u o u s ，w h i c hb a s eo nr i g - o r o u sm a t h e m a t i c sa n d l o g i c w i t hf o r m a ls p e c i f i c a t i o nl a n g u a g e s ，t h ea m b i g u i t yo f i n f o r m a ll a n g u a g ec a nb ea v o i d e d n e v e r t h e l e s s ，h u m a ne i t o r si nf o r m a ls p e c i f i c a t i o n sc a n tb ea v o i d e d t h i sp a p e rr e s e a r c h e st h em e t h o d so ft e s t i n gs p e c i f i c a t i o n s b yc o m p a r i s o nw i t hl o t so fm e t h o d st ov a l i d a t ef o r m a ls p e c i f i c a t i o n s ，t e s t i n gi s m u c hm o r eh u m a n - s a v i n ga n dm o r er e s o u r c e s a v i n gt h a nt h eo t h e r s i np r a c t i c e ， t h e r ea r em u c hm o r et o o l s u p p o r tt ot e s t i n gt h a nt ot h eo t h e rm e t h o d s i nt h i sp a p e r , w er e s e a r c ht h em e t h o d so ft e s t i n gm o d e l b a s e df o r m a ls p e c i f i c a t i o n s z o b j e c t - za n dv d m a r em o d e l b a s e df o r m a ls p e c i f i c a t i o nl a n g u a g e s t h e s e f o r m a ls p e c i f i c a t i o nl a n g u a g e sa r ec o n s t r u c t e dw i t hp r e d i c a t ef o r m u l at od e s c r i b e t h ef u n c t i o n so fs y s t e m s t h e r e f o r ef r o mt h ed i f f e r e n tv i e w s ，t h ep a p e rg i v e st w o m e t h o d st ot e s tm o d e l b a s e df o r m a ls p e c i f i c a t i o n s ：t h et e s t i n gm e t h o db a s e do ne r r o r o fp r e d i c a t e sa n dt h et e s t i n gm e t h o db a s e d0 1 1s 觚c t u r eo f p r e d i c a t e s f o rt h et e s t i n gm e t h o db a s e do ne l r o to fp r e d i c a t e s ，g i v e nt h a tt h e r ew e r es o l n e k n o w nt y p eo fe r r o r si nt h ep r e c o n d i t i o n so ff o r m a ls p e c i f i c a t i o n s ，s e l e c tt h er e l e - v a n tt e s to a s e sw h i c hm a k et h er e s u l to ft h eh y p o t h e t i c a l l yw r o n g p r e d i c a t ea n d t h a t o ft h ef i g h to n ed i f f e r e n t t h e nt h eo w i o r sc a nb ef o u n d i nt h i sp a p e r ，f o rt h e s et w o t y p e so fp r e d i c a t ee r r o r e x p r e s s i o nn e g a t i o nf a u l t ( e n f ) a n de x p r e s s i o nu n w a n t e df a u l t ( e u f ) ，t h i sp a p e rg i v e st w oc r i t e r i ar e s p e c t i v e l y ：e n fc r i t e r i aa n d e u fc r i t e r i a e n fc r i t e r i ac a nh e l pt e s t e r sc o n s t r u c tt e s to a s e st of i n da l le n fe r r o r s i np r e c o n d i t i o n so fm o d e l - b a s e df o r m a ls p e c i f i c a t i o n s a n de u fc r i t e r i ac a nc o n - s t r u c tt e s to a s e st of m da l le u fe r r o r si np r e c o n d i t i o n so fm o d e l - b a s e df o r m a l s p e c i f i c a t i o n s t h e s ec r i t e r i ac a nc o v e ra l lp o s s i b i l i t i e so ft h ek n o w ne r r o r sa n da s - s u r et h ep r e c o n d i t i o n so ft h ef o r m a ls p e c i f i c a t i o n sa r er e l a t i v e l yf r e eo fe r r o r s t h et e s t i n gm e t h o db a s e do ns t r u c t u r eo fp r e d i c a t e si sb a s e d0 1 1c o v e r a g et r i t e - r i a t e s t e r sk n o wt h ep r e c o n d i t i o n sa n dt h ep o s t c o n d i t i o n so ff o r m a ls p e c i f i c a t i o n s ； a n dt e s t e r sd ot h ec o v e r a g et e s t i n gf o rt h ef o r m a ls p e c i f i c a t i o n s t h i sp a p e rg i v e s5 d i f f e r e n tc o v e r a g ec r i t e r i aa n de a c hh a sd i f f e r e n tc o v e r a g eo nt h ep r e d i c a t e so f m o d e l - b a s e df o r m a ls p e c i f i c a t i o n s i nt h ef i e l do fs o f t w a r et e s t i n g ，t e s t i n ga u t o m a t i o ni sv e r yi m p o r t a n t t h eg o a l o fa u t o m a t i o ni st os a v et h ec o s to ft e s t i n ga n dt os i m p l i f yt h ep r o c e s so ft e s t i n g o n et o o lh a sb e e nd e v e l o p e df o rt e s t i n ga u t o m a t i o n t h et o o lp r e d t e s t i n gi sd e - s i g n e dt os i m p l i f yt h ep r o c e s so ft e s ta n dt oc o n s t r u c tt e s tc a s e sa u t o m a t i c a l l y p r e d - 第页 上海大学硕士学位论文 t h ep o s t g ra d ii a ：r et i 匮s i so fs l 州g h a iu n i v e r s i t y t e s t i n gh a sag r a p h i c a li n t e r f a c e ，w h i c hi sb a s e d0 1 1j a v a6 0a n ds w i n gg u i u s e r s c a l le x p o r tt e s to a s e s 勰舢，f i l e s i nt h i sp a p e r , w eg i v et h ed e t a i l e di n t r o d u c t i o n a b o u tt h ea r c h i t e c t u r e ，d e s i g na n di m p l e m e n t a t i o no ft h et 0 0 1 f i n a l l y , o n es a m p l ei s g i v e nt os h o wh o w t ou s ep r e d t e s t i n g k e y w o r d s ：s o f t w a r et e s t i n g ，f o r m a ls p e c i f i c a t i o n ，p r e d i c a t ef o r m u l a , t h e o r e m p r o v i n g ，c o v e r a g et e s t i n g 第页 上海大学硕士学位论文 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 原创性声明 本人声明：所呈交的论文是本人在导师指导下进行的研究工作。 除了文中特别加以标注和致谢的地方外，论文中不包含其他人已发 表或撰写过的研究成果。参与同一工作的其他同志对本研究所做的 任何贡献均已在论文中作了明确的说明并表示了谢意。 签名：繇日期竺茎i ：型_ 本论文使用授权说明 本人完全了解上海大学有关保留、使用学位论文的规定，即： 学校有权保留论文及送交论文复印件，允许论文被查阅和借阅；学 校可以公布论文的全部或部分内容。 ( 保密的论文在解密后应遵守此规定) 签名：纽垫导师签名：骘毖日期： 泸瑶。3 。l r 上海大学硕士学位论文 t h ep o s t g r a d u j 蛆 e1 h e s i so fs h a n g h a iu n i v e r s n y 1 1 研究背景 第一章绪论 随着软件的广泛应用，特别是软件在尖端领域的应用，软件可靠性成为一 个非常重要的问题。软件的可靠取决于两个方面，一个是软件产品的测试与验 证，另一个是软件开发的方法与过程。对简单的软件开发，一般的经验是先有 用户需求，然后对软件进行设计，接着是编写程序，最后是对程序进行测试。 如果测试发现错误，则对软件进行修改，然后再测试，直至对程序满意为止。 对复杂的软件系统，总的过程基本还是这样，只是各个阶段也相应复杂一些。 比如说，用户需求可能需要从多方面进行描述，软件的设计需要从多方面考虑， 程序的编写需要分成多个单元，对于测试来讲也就有单元测试和集成测试的区 别。有些用户需求难以一开始就完全描述清楚，而更改用户需求会对软件设计 以及其他大量已经完成或正在进行的工作产生很大的影响，因此软件开发方法 和过程需要提供反复修改软件要求的便利。 形式方法帮助软件的开发者通过形式规格说明语言来描述软件需求，使软 件的需求精确的、无二义性。软件的形式规格说明详细的描述了软件“做什么”。 开发者需要实现软件的规格说明，描述软件的“怎么做”。 形式方法的应用在电路设计和协议设计上都取得了很大的成绩。但是软件 开发因为其自身的特性决定了形式方法不能从其他领域直接照搬、照抄过来。 形式方法在软件领域的应用还有很多没有解决的问题。软件的描述要比电路和 协议复杂。一个软件描述所包含的状态空间通常来讲可以是无限的，验证软件 在时间和空间上都十分复杂。 形式规格说明可以清楚地描述软件需求，在不涉及软件的实现细节的基础 上，保证了软件的需求和实现最大程度的独立。但是形式方法无法保证形式规 格说明是正确的，完整地表达软件需求。因为自身知识的局限性，书写规格说 明的人员无法保证规格说明是完整的，正确的。而不正确，不完整的规格说明 必然会使得依照规格说明而开发的软件也存在错误。而这样的错误是非常危险 的。因为规格说明是唯一的，详细的，形式化描述软件需求的正式文档。它在 整个软件开发的流程中具有非常重要的作用。很多软件测试准则都是基于规格 说明的。如果沿用错误的规格说明，会使得软件可以“安全地”通过基于规格 说明的测试。这样的软件必然使得后期的维护成本大幅度的提高，甚至于项目 的失败，代价可想而知是非常高昂的。所以，验证规格说明的正确性和完整性 是形式方法的一个重要环节。 第1 页 上海大学硕士学位论文 t h ep o s t g r a d u a r e1 t m s i so fs h a n g h a iu n e r s i t y 1 2当前国内外研究现状 随着形式方法广泛的认识和应用，如何验证规格说明，保证规格说明的正 确性和完整性已经成为软件形式化过程中的重要环节。常用的验证规格说明的 方法主要包括以下几种：定理证明，模型检查，规格说明复查和测试。 定理证明是检验规格说明最基本的方法。基于z 的规格说明是由一阶谓词 逻辑构造的。文献【l 】详细描述了如何对一个基于z 规格说明语言开发的系统进 行定理证明。定理证明的整个过程可以归纳为两个步骤：1 描述规格说明性质 的定理。2 展开定理，通过推导的方式证明该定理的正确性。定理证明的不 足之处在于推理的难度。对于稍微复杂的系统，自动化的推理就难以胜任。 模型检查是用来对有限状态的系统进行形式验证。现在模型检查的理论非 常成熟，文献【2 】介绍了如何验证基于时序逻辑公式的软件系统的正确性。模型 检测的困难首先是它所能检测的是有限状态模型。这样对于一般软件，需要有 一个从任意状态到有限状态的建模过程。并且这样的一个模型的状态空间会面 临组合爆炸的问题。所以模型检查常应用于安全领域的软件系统，要求软件系 统有较少的状态，以避免状态空间的爆炸问题。 规格说明复查是一种规格说明检测的手动方式。文献【3 】提出了一种基于 r e v i e wt a s kt r e e ( r t t ) 的规格说明复查方法。结合规格说明测试，复查规格说 明。文章通过结合测试用例来提高软件规格说明的质量，改进规格说明复查的 效率。但是规格说明的复查技术无法做到完全的自动化，需要人的参与，使得 规格说明复查的不确定性很大。 规格说明的测试相比定理证明和模型检查更加实用。在软件开发中，对于 人力和物力的要求也更低，能够更好地得到普及。但是在目前阶段，规格说明 测试的研究相对较少。 规格说明测试的最初目的是为了更好的帮助规格说明的书写者进行自我检 查，尽早的发现规格说明中的一些问题。r i o h a r d 提出规格说明测试在检测设计 缺陷的应用的思想方法【4 】。他研究了如何应用规格说明的测试来检测设计过程 中的缺陷，分别运用快速原型开发和符号执行这两种方法来运行测试用例，达 到检测设计过程中的缺陷的目的。同时相应的工具也被开发出来。r i c h a r d 把规 格说明测试作为一种规格说明的自检方式，没有应用正确的测试准则和适合规 格说明的测试用例的生成方法，只是手动的构造测试用例。 动画模拟技术是当前模拟运行规格说明的主要方式之一。它的优势在与快 速把不可执行的规格说明装化为可执行的代码。p a n k a j 提出了针对规格说明的 完整性的测试，描述了个测试规格说明系统【5 】。通过把规格说明转变为可执 行的程序，执行相应的测试用例来达到测试的目的。p a n k a j 虽然解决了测试用 第2 页 上海大学硕士学位论文 t h ep o s t g r a d u a r e 正s i so fs h a n g h a iu n i v e r s i t y 例的执行问题，但是也带来了代码的实现错误。底层的实现错误使得测试的结 果混淆，无法达到设计测试用例的初衷。 在面向对象技术十分广泛的今天，面向对象的规格说明语言也越来越多的 被应用。c h e n 提出了面向对象规格说明语言o b j e c t z 的测试方法 6 】。o b j e c t z 的类模式包含：常量定义( o o n s t a n td e f i n i t i o n ) ，状态模式( s t a t es c h e m a ) ，操 作模式( o p e r a t i o ns c h e m a ) 等。针对o b e c t - z 的面向对象特性，c h e n 提出了对 常量定义，状态模式和操作模式分别产生测试用例的方法。同时，该文献探讨 t o b j e o t - z 中继承关系中的测试问题，提出了继承关系对现有测试用例的影响 以及如何改进现有的测试用例以满足继承子类的复用。 通过对国内外在规格说明验证领域的研究状况的调研，我们发现对于规格 说明验证的研究远没有达到成熟的地步，还有很多的工作需要去做。 1 3 课题研究的内容 本课题研究形式规格说明的测试方法，研究的是基于模型的形式规格说明 的测试。本文研究目的在于从方法学上和工具上对基于模型的形式规格说明测 试的支持。形式规格说明测试的研究不仅可以使形式规格说明的正确性得到保 证，同时也可以间接地推动规格说明被广泛的接受。 形式规格说明是基于用户需求的，描述系统功能的形式规格说明。因为用 户的需求是模糊的、不精确的、由自然语言所描述，常见的用户需求是由用户 需求文档定义的。基本的测试方法要求我们对被测对象的功能定义要有清晰的 描述。而形式规格说明却不具备这样的测试条件。本文从两种角度对形式规格 说明的谓词部分进行测试：基于谓词错误的测试方法和基于谓词结构的测试方 法。 基于谓词错误的测试方法假设形式规格说明的前置条件存在已知类型的谓 词错误。本文提出的测试方法是通过选取合适的测试用例使得假设错误的谓词 公式和假设正确的谓词公式的结果是异或的，发现前置条件的错误。基于两类 谓词错误：表达式否定错误( e x p r e s s i o nn e g a t i o nf a u l t ) 和表达式多余错误 ( e x p r e s s i o nu n w a n t e df a u l t ) ，本文分别提出了两种不同的测试准则：e n f 测试 准则和e u f 测试准则。e n f 测试准则可以帮助测试人员构造测试用例，发现 规格说明前置条件中的e n f 错误。相对的，e u f 测试准则可以发现前置条件 中的e u f 错误。基于谓词错误的测试方法可以覆盖谓词公式中所有一类错误的 可能性，保证形式规格说明前置条件相对正确性。 基于谓词结构的测试方法是基于覆盖的测试准则。测试人员在不了解规格 说明描述的系统功能的基础上，对规格说明进行覆盖度测试。本文提出了5 种 第3 页 上海大学硕士学位论文 t h ep o s t g ra d u a ：r et h e s i so fs h a n g h a iu n i v e r _ s i t y 不同的覆盖度准则。基于不同覆盖度准则的测试用例可以对形式规格说明的谓 词部分有不同的覆盖度。 在测试领域中，测试的自动化是非常重要的。测试自动化是为了节省测试 的成本以及简化测试的过程。本文基于谓词错误的测试方法，研究并开发了一 套应用于基于模型的形式规格说明的测试工具p r e d t e s t i n g 。它可以简化测试的 过程，使测试用例生成的过程自动化。p r e d t e s t i n g 是基于j a v a6 0 和s w i n g 图 形界面的图形化测试工具。该工具可以把测试用例导出为标准的x m l 文件格 式。 1 4 论文组织结构 本文共分6 章，全文对基于模型的形式规格说明的测试方法进行了深入的 研究，并提出了一套测试方法和相应的辅助测试工具。 第一章介绍了规格说明测试的研究背景和当前国内外对于规格说明验证的 研究方向，另外，大概介绍了本文的研究方向及其主要的研究成果。 第二章详细介绍了形式方法和测试，并阐述了当前形式方法得不到普遍推 广的主要阻力。本章节重点分析了不同规格说明验证方法的优劣，从中发现了 规格说明的测试相比其他的验证方法具有更好的实用性和可靠性。在测试成为 工业界得到普遍认可并推广的软件验证方法的同时，它也将成为规格说明验证 的主要研究方向。 第三章提出了一种基于谓词错误的测试方法。本章节详细分析了不同谓词 错误的特性，并发现了谓词错误和相对应的检错条件之间的关联。根据这样的 关联性，我们提出了两种测试准则：d 妤测试准则和e u f 测试准则。 第四章介绍了基于谓词结构的测试方法。本文提出了5 种不同的覆盖度准 则。基于不同覆盖度准则的测试用例可以对形式规格说明的谓词部分有不同的 覆盖度。 第五章详细介绍了p r e d t e s t i n g - - 基于谓词错误的测试方法的辅助工具。该 工具是藉由标准x m l 格式的z 规格说明到测试用例的自动生成的工具。本章 节从p r e d t e s t i n g 的基本架构、设计和实现出发，对它进行了系统的介绍，同时 详细描述了e n f 测试准则和e u f 测试准则的d i i f 算法的实现。 在第六章中，我们总结了本论文的研究重点以及对未来的展望。 第4 页 上海大学硕士学位论文 1 h ep o s t g ra d u a t e1 翻旺s i so fs h a n g h a iu n i v e r s i t y 第二章形式方法和测试 软件工程是研究大规模程序设计的方法、工具和管理的工程科学。软件工 程的起源是因为6 0 年代末出现的“软件危机”。其主要表现为：软件质量差、可 靠性难以保证；软件成本增长难以控制，极少软件能在预定的成本预算内完成 的；软件开发进度难以控制，周期拖得太长；软件的维护很困难，维护人员和 费用不断增加。其中毋m 公司所开发的o s 3 6 0 就是一个典型的例子。从7 0 年代开始，越来越多的软件开发人员开始重视软件开发的过程以及软件开发方 法的研究和应用。形式规格说明语言的提出和形式方法在实际中的应用为软件 工程提出了一种新的方向。 2 1 形式方法 形式方法可以分为形式化描述和建立在形式化描述基础之上的形式化开 发。形式化描述就是用形式语言( 具有严格的语法、语义定义的语言) 作描述。 形式方法研究的目的是提供更好的理论、方法和工具，扩大形式方法的应用范 围和使用价值。 形式方法的意义在于：“它能帮助软件开发人员发现其它方法不容易发现的 系统的一致性，明确性或完整性问题，有助于增加软件开发人员对系统的理解”。 因此，形式方法是提高软件系统，特别是s a f e t y c v i t i o a l 系统的安全性与可靠性 的重要手段。最早的形式方法是逻辑与逻辑推理，它的目标是使推理机械化。 从广义上讲，这一目标受到许多挫折。主要原因包括逻辑系统的不完备性 ( i n c o m p l e t e n e s s ) 、逻辑系统的不可判定性( u n d e c i d a b i l i t y ) 和自动推理的难处理性 ( i n t r a o t a b i l i t y ) 。但是在一些实际应用上，逻辑方法和自动推理还是起着非常大 的作用。 2 1 1 软件形式化 早期形式方法在软件验证的应用是串行程序的验证，后来随着软件研究和 应用的发展，逐渐多样化。比如用逻辑和代数方法描述软件，用逻辑推理来验 证软件( 即描述软件的这些逻辑公式) 的性质。又比如用进程代数描述并发软 件，用模型检测方法验证这些软件的性质。近年来，由于认识到形式方法重视 的是严谨性，而这些方法与常用的软件方法差别很大，逐渐有许多结合图形化 软件方法、面向对象方法和形式方法的工作。以上所述几个方面( 即程序验证， 定理证明，模型检测，图形化方法和形式方法相结合) 的内容虽然不尽一样， 第5 页 上海大学硕士学位论文 1 巳p o s t g r a d u j t e1 m s i so fs h a n g h a iim t e r s i t y 但密切相关。定理证明与模型检测互为补充，各有所长。对于复杂的软件系统 的验证，最好是能够结合多种方法的使用这些方法对高可信软件开发方法的 探索和应用都极为重要。 形式方法在软件开发中能够起到的作用是多方面的。首先是对软件要求的 描述。软件要求的描述是软件开发的基础。比如说一般非形式的描述很可能导 致描述的不明确和不一致。不明确或不一致的描述会导致设计、编程的错误， 从而影响最终程序的可靠性和可使用性。而形式方法要求描述是明确的。其次 是对软件设计的描述。软件设计的描述和软件要求的描述一样重要。形式方法 的优点对于软件要求的描述同样适用于软件设计的描述。另外由于有了软件要 求的形式化描述，我们可以检验软件的设计是否满足软件的要求。对于编程来 讲，我们可以考虑自动代码生成。对于一些简单的系统，形式化描述有可能直 接转换成可执行程序，这就简化了软件开发过程，节约了资源和减少了出错的 可能性。另外，形式方法可以用于程序的验证，以保证程序的正确性。对于测 试来讲，形式方法可用于测试用例的自动生成，这可以节约许多时间和在一定 程度上保证测试用例的覆盖率。 形式方法是用数学与逻辑的方法描述和验证软件。从描述上讲，一方面是 系统或程序的描述，另一方面是性质的描述。这些可以用一种或多种语言来描 述。这些语言包括命题逻辑，一阶逻辑，高阶逻辑，代数，状态机，并发状态 机，自动机，计算树逻辑，线性时序逻辑，进程代数，演算，u 演算，特 殊的程序语言，以及程序语言的子集等。从验证来讲，主要有两类方法，一类 是以逻辑推理为基础，另一类则以穷尽搜索为基础。逻辑推理有n a t u r a ld e d u c t i o n ，s e q u e n tc a l c u l u s ，r e s o l u t i o n 以及h o a r e 1 0 9 i c 等方法。穷尽搜索方法统称 为模型检测。这类方法与系统或程序以及系统性质的表示有很大的关系，比如 说符号模型检测，其基本原理是用命题逻辑公式表示状态转换关系，用不动点 算法计算状态的可达性以及这些状态是否满足某些性质。 2 1 2 形式规格说明语言 形式规格说明语言是指具有高度的抽象性和精确性，无二义性的规格说明 语言。形式规格说明语言可以交给计算机来进行处理，进行分析、查错、验证 以及求精变换。常见的形式规格说明例如z ，o b j e c t z ，v d m , l o t o s ，o b j , l a r c h 等。 z 语言是基于一阶逻辑和集合论的形式规格说明语言。z 规格说明的基本 单元是模式。每个模式都描述了该操作了前置条件和后置条件。因为z 是基于 一阶逻辑和集合论的，所以模式分为声明部分和谓词部分。声明部分定义了该 第6 页 上海大学硕士学位论文 1 h 叵p o s t g ra 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 模式用到的所有变量和输入输出。 o b j e c t - z 是一种面向对象的形式规格说明语言，它是面向对象技术和形式 方法的统一。它对z 语言在面向对象方面进行了扩充，同时z 语言现有的语法 和语义在o b j e c t - z 中仍被保留。随着面向对象技术的广泛使用，面向对象的规 格说明语言o b j e c t z 也得到了应用。由于o b j e e t z 保留了z 的语法和语义，因 此它具有z 的特征。它使用相对简单的集合、关系、映射、序列、包和一阶谓 词逻辑等表示发来描述系统，借助于模式来表达系统结构，提供了一种能独立 于实现的、可推理的数学模型，有利于保证程序的正确性。它还利用模式和模 式演算对软件系统的结构和行为特征进行抽象描述。其中状态模式用来描述软 件系统的结构特征，操作模式则用来描述系统的行为特征。 v d m 语言是一套数学符号系统和基于形式谓词逻辑和集合论的证明规则 隅】。这是在1 9 7 3 年由i b m 维也纳实验室首先提出的一套开发大型软件系统的方 法。它以指称语义为基础，充分利用了6 0 7 0 年代发展起来的以数学为基础的 形式方法。 o b j 代数规格说明语言提供了以独立于实现的方式描述数据结构的基础， 一种光谱语言，刻画公理可描述所有抽象级上的性质：规格说明级和执行级【9 1 。 o b j 由对象网层组成，每个对象说明一个抽象数据对象。 l o t o s 语言是一种时序规格说明语言。其静态语义基于属性文件，动态语 义基于代到1 0 】。l o t o s 是可执行的、可证明的。l o t o s 是为了描述i s o 标准数 据通讯协议和服务o s i 而产生的。 2 1 3 形式方法的不足 形式方法的出发点是数学逻辑方法。其目的是开发可靠的软件产品。从软 件开发来讲，形式方法目前并非软件开发的主流。造成这种情况的主要原因在 于： 1 ) 形式规格说明难以阅读，不够直观。 因目前大多数软件开发人员习惯于非形式方法，缺少形式方法的训练。而 且数学概念简明、抽象，用他编写的形式规格说明简洁、紧凑，同时也较抽象、 难懂。对于一般的编写形式规格说明就需要相当的数学及其他理论基础，更别 说验证规格说明的正确性，或是检测规格说明。 2 ) 形式规格说明语言的正确性证明困难。 这是由正确性证明的内在困难决定的，如断言的构造等工作尚不能完全通 过计算机自动实现，正确性证明一般由手工进行或由人与计算机交互进行。 3 ) 形式方法也不能避免出错。 第7 页 上海大学硕士学位论文 t 陋p o s t g r a d iy a r et 髓s i so fs h a 缸a iu n i v e r s r r y 形式方法能够减少由误解引起的错误，但其不能保证在编写软件规格说明 时不出现语法错误、规格说明不一致，不完整等问题。目前，只有支持语法检 查、类型检查的工具，而能支持形式规格说明语义一致性。完整性检查的全自 动工具尚未出现。这就要求我们通过其他方式来保证规格说明的正确性、完整 性。 4 ) 形式方法相关支持软件的缺乏。 到目前为止，还没有一套工具可以把规格说明直接转化为代码。所以从形 式规格说明到代码的过程还需要人手动的完成。以上都是阻碍形式方法普及的 主要因素。 2 2 软件测试 随着时代的进步，科学的发展，软件不再是实验室里的实验品，不再是少 数科学家使用的工具，不再只是仅有的几台超级计算机才能够运行的稀有品。 软件随着计算机的普及而变得寻常，它存在于社会生活的每个角落。随着软件 的规模化，集成化。软件的复杂性也成几何数递增。但是却没有一个行之有效 的方式来解决软件复杂性所带来的问题。软件测试就是在这样的背景下应运而 生的。 软件测试的完整定义是：“度量软件被开发的计算机软件的质量的过程 i n 。计算机软件的质量主要包括以下几点：正确性、完整性、安全性。通常， 软件测试是指通过测试数据来验证软件系统中的错误和缺陷，以衡量软件系统 的质量。 软件测试是度量软件质量的重要手段之一，测试的目的在于提高软件的质 量。软件测试就是这样一个不断循环的过程：测试，发现错误，解决错误，再 测试。 软件测试是软件开发中的一个重要环节，它包含了三个部分：构造测试用 例、运行测试用例和评估测试结果。构造测试用例是软件测试的核心。不同的 测试准则效率各有不同。在等量测试用例的基础上，衡量测试准则的优劣可以 通过衡量两个测试准则发现错误的数量。产生软件测试的方法可以分为两类： 白盒测试和黑盒测试。白盒测试是指在了解被测软件的内部结构的基础上产生 测试用例。主要有：语句覆盖、条件覆盖、判断覆盖、判断条件覆盖等。黑 盒测试则相反，测试人员不了解被测软件的内部结构，根据被测软件的规格说 明或需求产生测试用例。黑盒测试主要包括：等价类，边界分析、因果图等。 白盒测试和黑盒测试各有优势，互有不足。在真实测试的过程中，测试人员往 往结合这两类测试方法，构造测试用例，提高测试的效率。运行测试用例是指 第8 页 上海大学硕士学位论文 t h ep o s t g ra d ua = r et h e s i so fs h a n g h a iu n w e r s n 叮 在真实的系统中运行已产生的测试用例。测试用例的运行这一环节主要研究方 向是如何提高测试用例运行的自动化。减少人的参与。最大程度的提高软件测 试的速度和效率。评估测试结果是指比较测试用例的实际运行结果和测试用例 的预期结果。测试结果的预期是根据规格说明计算得到的。在这一领域的主要 研究方向是如何自动化的产生测试用例的预期来帮助提高测试的自动化程度。 2 3形式规格说明的测试 形式方法的应用在电路设计和协议设计上都取得了很大的成绩。但是对于 软件来讲还有很多没有解决的问题。软件的描述要比电路和协议复杂。一个软 件描述所包含的状态空间通常来讲可以是无限的。因此验证的难度很大。逻辑 推理的不足之处在于推理的难度。对于稍微复杂的定理，自动化的推理就难以 胜任。人为的推理有很大的缺点，除了费时费力外，比如说一个定理推不出来， 并不能说明这个定理不成立，很可能是推理方法和策略应用不当。模型检测的 好处在于它有全自动化的检测过程，并且如果一个性质不满足，它能给出这个 性质不满足的理由。我们即可据此对我们的系统描述进行改进。模型检测的困 难首先是它所能检测的是有限状态模型。这样对于一般软件来讲，需要有一个 从任意状态到有限状态的建模过程。并且这样的一个模型的状态空间会面临组 合爆炸的问题。 形式规格说明是精确的，无歧义的，但正如前文所说形式规格说明并不一 定是正确的，能够真实反应用户的需求。规格说明的正确性证明包含两方面： 语法正确和语义正确。对于语法正确性，针对不同的规格说明语言，目前都有 相应的编辑器来辅助用户方便地编辑规格说明。英国y o r k 大学设计的z 规格说 明支持工具c a d i z 可以提供专业质量的软件规格说明文档【1 2 】。c a d 亿能够对z 规格说明进行语法检查和类型检查，并支持排版，还能够与用户进行交互以查 看z 规格说明中某些特性。美国芝加哥d cp a u l 大学计算机科学和信息系研制的 z t c 是一个比较实用的z 规格说明的类型检查工剧1 3 1 。该工具能够保证z 规格说 明的语法以及类型的正确性。i t r u 的b p 研究组在b t o o l 的基础上实现了z 规格说 明支持工具z e d bt o o l ，该工具能自动地进行模式运算【l4 1 。规格说明的编辑工具 可以自动的检测帮规格说明语法，找出规格说明的语法错误，例如类型匹配， 格式的正确性。 但是仅仅这样是不够的，要做到规格说明的语义正确性还有很多工作要做。 目前，规格说明的检测方法包含：快速原型开发、符号执行、测试、定理 证明和模型检查。测试相对于其他几种检测方法各有利弊，互有长短。 1 ) 测试v s 快速原型开发。 第9 页 上海大学硕士学位论文 1 h 叵p o s t ( 球a 【) iy a t et h e s i so fs h a n g h a iu n i v 目r s 盯y 快速原型开发是指把不可执行的规格说明转换成可执行的代码( 原型) 。通 过执行规格说明的原型演示规格说明描述的语义。通过和用户的直接交流，用 户可以清楚的了解规格说明和需求之间的关系。然后在这一过程中( 不可执行 的规格说明转换成可执行的代码) 必然会引入不必要的低层实现错误。这些实 现上的错误与原来的规格说明中的错误混淆，直接影响用户对规格说明的语义 正确性的判断。而规格说明的测试是直接针对规格说明本身进行的，避免了不 必要的底层实现错误。 2 ) 测试v s 符号执行。 符号执行需要对规格说明进行演算，通过前置条件的输入，得到后置条件 的输出。这一过程的复杂程度相比测试高，而测试只是简单的输入值，在演算 的过程中可以自动的简化原有的谓词公式，达到简化演算过程的作用。 3 ) 测试v s 定理证明。 定理证明是针对某一规格说明的特定性质，通过证明的方法来验证该规格 说明所有的模型这一性质都是成立的。定理证明是最为完美的方法来保证软件 的质量，但是同时这一方法也是最为复杂，最难以实施的。定理证明的不足之 处在于推理的难度。对于稍微复杂的系统，自动化的推理就难以胜任。人为的 推理有很大的缺点，除了费时费力外，比如说一个定理推不出来，并不能说明 这个定理不成立，很可能是推理方法和策略应用不当。 4 ) 测试v s 模型检查。 模型检测的好处在于它有全自动化的检测过程，并且如果一个性质不满足， 它能给出这个性质不满足的理由。我们即可据此对我们的系统描述进行改进。 模型检测的困难首先是它所能检测的是有限状态模型。这样对于一般软件来讲， 需要有一个从任意状态到有限状态的建模过程。并且这样的一个模型的状态空 间会面临组合爆炸的问题。所以模型检查常应用于安全领域的软件系统，要求 软件系统有较少的状态，以避免状态空间的爆炸问题。 针对不同规格说明验证方法的比较，规格说明测试相比其他的验证