测试，证明及自动化—

测试，证明及自动化——集成化方法

西蒙•伯顿约翰•克拉克约翰•麦克德米德

约克大学，计算机科学系

约克市，黑斯灵顿

YO10 5DD，英格兰

+44 1904 432749

{burton,jac,jam}@cs.york.ac.uk

摘要

本文介绍了一篇关于测试和证明在自动化软件验证和确认过程中的互补作用的讨论。我们证明这两种方法的结合如何能进一步提高自动化水平与完整性。我们特别讨论了采用自动化反例生成来支持证明，并将自动化证明作为测试用例生成自动检查的手段。通过识别证明中的重复结构，约定规范为否则表达式中正式表示法的一个子集，开发一款携带内置约束求解器的通用定理证明工具，高水平的自动化是有可能实现的。

1引言

在过去，将测试与证明结合起来并非易事。尽管它们都有提高软件质量这一共同目标，证明被看做是软件工程行家，测试则成了软件工程的工人阶级。作者认为这种人工二分法是有害的，测试和证明可以一起使用以达到良好效果。即使没有正式细化所带来的好处，形式化规范也可以极大地提高软件产品的质量。它们为系统所需行为留出了简洁、明确和显性的规范。因此，它们是自动化测试活动的良好基础。此外，测试能为证明生成反例，可以节省大量精力，而且能为调试产生例证。

使用形式化规范本身，仍被许多人看成是正规方法在广泛工业用途中的障碍。对于V&V正规方法被充分利用到工业中的好处，在某种程度上，需要“伪装”一下形式[15]。最近的工作[5]表明，正式规范和规范验证所对应的证明义务，可以从更直观的数学基础工程符号生成。这种方法，不仅可以实现领域知识的工程师们使用他们习惯的规范符号，而且正式的规范的翻译，对使用的正规符号子集有限制作用，它将规则结构加入到一些证明中，以免除对规范中某些属性（例如完整性和确定性）的验证。这些约束，加上用于特定领域的数据类型的子集，可以为V&V活动的自动化，提供强大的、有针对性的启发方法。本文所讨论的方法，都是假设在这种方式生成的正式规范环境中进行的。

接下来的文章，我们将描述如何能利用测试、证明和规范中限制结构的结合，提高软件验证和确认过程的一些领域的完整性和自动化。测试与证明之间的这种共生关系是可行的，只要通过扩展正式规范中关于测试的早期工作，和利用一个灵活的具备集成约束求解器的定理证明工具。

本文的结构如下：章节2讨论测试在证明反例自动化生成中的作用。章节3描述如何利用证明，作为验证自动测试用例生成策略的一种方法，以及作为执行自动化本身的一种方法。我们还将说明，如何开发更有效的、以正式规范测试用例自动生成为基础的测试策略；如何利用证明作为一种测试源。章节4总结本工作的主要贡献，得出一些结论。

2测试与证明

证明推测可以出现在V&V过程的各个结点中。例如，确保某一规范满足某些“健康”标准，如完整性和确定性，或者检验某一程序是它的形式化规范的正确精致。在所有情况下，无效的推测会浪费大量证明努力。因此，在开始一段冗长而费力的手工证明之前，要重新确信对推测有的效性，有很好的置信度。用约束求解技术来生成反例，不仅节省了证明所需的开销，当出现错误时候，还能提供可使用的说明信息。用来验证规范性能的反例生成，在证明方面，是一种测试形式。有代表性的样本数据被生成，然后，测试它们是否违反了规范。如果是这样，就找到了一个反例。

约束求解通常被认为是难以控制的[13]。然而，实际情况是，人们从来不需要求解“一般性”约束，而是求解带有限制结构和特殊输入空间特性的特定子集。可以开发这些特性，使查找反例变得自动化。作者使用Z[16]型检查器和定理证明器CADiZ[19]来使查找工作自动进行。在这种意义上，使用CADiZ类似于基于Z型的Nitpick规范检查器[12]，后者使用模型检查技术生成规范断言的反例。不管怎样，CADiZ有其额外的灵活性，它可以写入通用证明策略（使用一个比较懒惰的函数记号[20]），可以交互式地调用和应用于屏幕上的任何证明义务。写入的证明策略，尝试在某些类型自动证明推测上尽最大努力（例如完整性检查）。如果证明失败或者是不确定的，这种策略会执行一些简单化操作，为集成约束求解器将推测转换成适当的形式。然后可以调用一些约束求解器尝试生成反例，这些包含一个模型检查器（SMV[3]）和一种基于启发式搜索的模拟退火法[6]。在约束求解器可以被高效地应用之前，需要简化的数量将会依赖证明义务的结构。

当需要解决大量的相似证明推测时，使用那样的自动化证明策略达到了良好效果[5]。有一种情形，如果不手动完成将会耗费时间，导致“检查器失明”，出现错过误差的情况。我们已经发现不同的约束求解器对不同的输入域有效。比如模型校验器只对离散输入域实用，然而基于最优化的搜索技术也适合于无穷状态空间和非线性约束条件。

3证明与测试

正式规范为测试打下良好基础。它们顾及了简洁明确的需求表示，经得起证明和自动化分析的检验。基于模型的正式规范的测试生成技术[14,8,17]，如Z[16]或VDM-SL[10]，典型地以将规范分割成等价类原则为基础[9]。等价类是被假设的规范输入空间的划分，是为了测试目的，代表了规范中的相同行为。这种技术经得起自动化和工具支持检验。然而，像所有引入自动化的案例一样，尤其是高完整性系统，这种工具的完整性是极为重要的。为了使自动测试能为软件和软件规范的一致性提供可信性，测试生成策略必须是既已验证的又有效的。换言之，不仅要说明自动测试被正确地实施，而且必须说明它们在实施中擅长发现错误。

3.1自动化测试策略的检验

当检验测试分割策略已经被正确实施的时候，可以采用多种标准。例如，可以来说明测试完全覆盖原有规范的有效输入空间。如果情况并非如此，可能包含错误的实施的重要实分，也许仍未被测试。如果，作为结果的测试用同样的正式符号作为原有规范，就可以用证明来执行这些检验活动。尊重原有范式（Spec）生成的测试（T1..Tn）完整性，可以通过下面这个式子的推导得到检验：

定理1: Inputs·SpecóT1∨…∨Tn

一种实例型分割策略识别A∨B式子规范中的表达式，并将表达式分割成下面的测试用例：A∧B，﹁A∧B和A∧¬B[8]，这里A和B本身可能是复杂的判断式。应用这个推测，证明这些分割保留原有规范的有效输入状态空间，因此还可以采用下面式子：

定理2: Inputs·A∨Bó(A∧B)∨(¬A∧B)∨(A∧¬B)

可以用简单几步证明这个定理。不管A和B代表的表达式结构如何，都可以使用相同的证明步骤。通常，每一个分割策略可以导出一个证明，每次在实施这个策略时，就用这个证明来验证分割结果。通过使用CADiZ中的证明策略机制，作者已经为一些普通分割策略实现了证明的自动化。不论何时实施一个策略，可以在结果上自动调用相应的正确性证明。这样可以保证，不管用什么样的测试生成方法，结果总是会表现出有效的或者相反。可以给这个工具下达命令，在应用一种证明策略时，记录个人使用的证明步骤，这些可以通过一个表格打印出来，应对人工审查的检验。所以，倘若无法给这个工具下命令，可以开发一个严格的论证，支持证明步骤的正确性。

如果给出测试策略的一种形式定义作为其等价式（例如，上面的定理2），测试用例本身的推导，亦可采用通用的证明策略实现自动化。这一原理在运作上跟使用析取范式（DNF）相似，将一个表达式简化成联合式的分离形式，每一个分离式可以用作单独的测试用例。在对DNF转换使用简单的逻辑重写规则分配分离式的地方，以公共测试启发式为基础，可将更多的定向等价式用公式表示。

基于测试启发式正式规范的测试分割，已经通过CADiZ证明策略得到实现。一般的分割策略被指定成如定理1形式的等价式。在被划分的判断式上调用一个证明策略，来实例化带判断式操作对象的一般等价式，并简化整个范式，显示划分的分离式。每个测试用例等价于原有范式，输入空间按照一种划分而受到限制。划分策略的完整性被留作一个辅助推导，证明划分确保是有效的。这个可以通过扩展划分策略实现自动化，使用上面描述过的通用证明策略即可。下面的简单例子演示了测试划分是如何推导的。例子范式中要计算一个正整数（n?）的平方根(r!)，并用运算符≧的边界值分析，生成测试划分（以假设错误常出现在边界值上或边界值周边为依据[2]）。

范式由下面的Z模式¹给出:

┌——SquareRoot—————──┐

│n?,r!:R

├─────────

│n?≧0∧

│r!×r!=n?

└──────────────┘

对实数边界值分析测试的启发式，约定成下面的等价式。注意，“恰好擦边”的边界用例在这里选为0.1。这个值对于不同的应用可能会变化，由基于不同应用特性的测试器选定，比如用来实现抽象类型R的具体类型的解决方案。

(x=y)∨(y<x≤y+0.1)∨(x>y+0.1)

x ,y: R·x≥ y

一个未划分的范式为模式表示成下面的存在量词：²

·n? ≥0∧r!×r!=n?

n? ,r! :R

现在引入划分原理，并用本地操作数对其实例化。划分原理作为边界条件，在测试用例被认为是有效之前，就应该得到证明。证明结果在下面定理中：

x,y: R·x≥yó(x=y)∨(y<x≤y+0.1)∨(x>y+0.1)

n?,r!:R·n?≥0∧r!×r!=n?∧((n?=0)∨(0<n?≤0+0.1)∨(n?>0+0.1))

边界条件得到了证明（比如使用预先约定的证明策略），简化后的存在变量剩下以下三条测试用例：

n?,r!: R·n?≥0∧r!×r!=n?∧n?=0

n?,r!: R·n?≥0∧r!×r!=n?∧ 0<n? ≤0.1

n?,r!: R·n?≥0∧r!×r!=n?∧n?>0.1

一旦产生测试划分，就可以使用CADiZ中的约束求解器，通过“求解”存在标量生成欲求的测试数据。上文描述的划分方法，支持由Stocks和Carrington[17,18]³所做的工作，他们为基于Z表示法的测试用例的推导和规范化，提出了一种框架（测试模板框架）。这里描述的测试用例推导的方法，通过提供一种机制补充了那个工作，这种机制自动应用测试启发式，显示测试划分，然后可以用测试模板框架将其结构化。

3.2自动化测试策略的验证

变异测试[7]是基于错误的测试技术，它故意将错误加入程序中，目的是评估测试设备检测那些错误的适当性。基于加入的错误被检测到的个数（突变分数），可以形成关于测试设备大体检错能力（变异适当性）的结论。变异测试提供一种验证前面章节讨论的测试策略的方法。测试用例的自动生成，正如上文描述的那样，能够为多种策略提供具有统计学意义的一定数量的测试用例。每一个这些策略的变异适当性可以被评估，用来比较它们检测错误的相对效力[1]。

将一个测试用例的规范，表示成一种生成测试数据的范式，也为一些额外变异增加数据的变异分数，开启了可能性。变异技术可以被应用到规范级别，来创造规范，表示实施中潜在错误的一种抽象描述（如同Budd和Gopal首先建议的那样[4]）。如果测试数据能从识别（杀死）变异的原有规范中生成，那样的数据也可能在程序级达到了一个相对高的分数。从规范中生成的数据，在某种意义上，也会“变硬”，不利实施中遇到偶然正确性的可能。

通常，能为一个正式规范表示符号，比如Z，生成突变体的数量非常大。然而，事实上，对于任何特殊的应用域，只会用到符号的一个子集。在这种情况下，可能的突变体数量会被限制。用这个子集，通过分析特殊测试策略的突变分数，可以得到变异策略采用的更多精挑细选的选择。变硬的测试数据可以从测试用例中生成，通过强化测试用例的判断式，改进生成数据中止挑选出来的一组规范突变体的可能性。在某些情况下，可以生成一组测试数据，中止一些突变体。可是，在变硬的判断式不一致的地方，需要生成几组测试数据。作为例子，下面是对一个系统的简单测试用例，求两个数的平均值：

A,B,Result:N·Result=(A+B)div2

通过给测试用例增加一个不等式，将“+”替换成“-”，测试数据可以对变异硬化。

A,B,Result:N|(A+B)≠(A-B)·Result=(A+B)div2

在这个用例中硬化的判断式是(A+B)≠(A-B)。这个表示检测变异体的一个必要条件，但是，通常不一定是充分的。依赖出现在实施过程中其他地方的变异，新的测试用例虽然不能保证产生中止突变体的数据，但是比没有硬化判断式的测试用例更能产生那样的数据。突变分析由Stocks和Carrington在他们的测试模板框架中简略提到过，作为增殖域的交错检验启发式。不论如何，作者认为仍然有研究范围，调查基于Z测试集的有效变异策略，变异分析是否可以与标准区域划分结合，提供更有效的测试集。因此，当应用测试实施时，进一步的工作将评价设计硬化判断式和他们增加突变分数的相对效力的不同标准。如果硬化判断式可以根据一组已知的规范突变体自动生成，就有可能利用传统变异测试方法（估定测试集的效力）的反馈，为特定类型的程序选择最有效的测试策略。

3.3证明作为测试源

从正式规范中生成的测试数据，和测试实施所需要的那样，典型不在同一抽象级别。一些精致需要用测试输入练习实施。对于不保持原有规范结构的实施来说，这个精致可能会困难。另外，一些规范可能是非决定论的，消除了预计期望的测试结果的可能性。

将规范有结构地分解成测试用例和预期结果二选一的方法，正如上面讨论的那样，是用一种“生成与测试”方法。通过任何方法（如随机法）选取测试输入，然后检验将输入应用到实施的结果与规范的一致性。这个方法也可以用在基于划分的连合测试。可以从每个测试划分中选择具有统计意义数量的样本，增加用于生成测试用例的等价类假设的置信度。在任一情形中，检验违反规范的测试输入输出，需要一个测试“源”。如果已知足够的精致信息，将系统的具体输入输出转换成它们在抽象规范中的等价形式，可以利用正式规范和自动化证明策略形成一个自动化的源。规范被用输入和输出实例化，证明策略被用来简化表达式成真（测试通过）或假（测试失败）。那样的简化理想地适合于自动化定理证明，因为它典型地涉及应用很多“单级”简化，直到将表达式简化为真或假。

4结论

在本文中，我们说明了怎样巧妙使用测试与证明的互相支持，为软件V&V处理带来有意义的好处，增加自动化和完整性。使用反例生成可以节省许多白白浪费的证明努力，用证明来支持测试用例设计，可以用来示范测试划分技术的正确性，本身也提供一种自动化方法。

高水平的自动化是有可能成功的，因为通过组合，限制正式规范所用的子集，预测所需证明结构的能力（多次复用证明策略的能力）和使用有集成约束求解能力的强大的定理证明工具。依据作者在航空应用程序的经验，这些限制不需要人为操作，而是作为域属性和各种类型被执行的证明自然地发生。

这里描述的一些技术（比如反例生成，自动化测试用例和数据生成）已经被应用到一个大型工业案例的研究[5]。其它技术（比如作为测试源的自动化证明和变异测试思想的应用）需要更多的研究以充分探索它们的潜能。尤其使用变异测试技术，在编码和规范级别都出现一个有希望的方法，为特定应用域的基于Z测试，自动生成有效的和有效率的测试标准。这是一个研究领域，通过本文描述的自动框架变为可能，并将成为未来工作的焦点。

5致谢

本工作资金由高完整性系统与软件中心，劳斯莱斯公共有限公司提供。

参考文献

[1]S.P.Allen,M.R.Woodward.基于规范的测试质量评估.Sandro Bologna,Giacomo Bucci,编辑,第三届国际会议关于实现软件质量的会议记录，341-354页.Chapman，Hall，1996

[2]Boris Beizer.软件测试技术.汤姆森计算机出版社,1990

[3]Sergey Berezin.SMV网站.http://www.cs.cmu.edu/~modelcheck/smv.html/,1999.可从此网站下载最新版本的SMV和相关文档

[4]Timothy A.Budd,Ajei S.Gopal.通过规范变异的程序测试.计算机语言,10(1):63-73,1985

[5]Simon Burton,John Clark,Andy Galloway,John McDermid.高完整性系统的自动化V&V,一个定向的正式方法.第5届NASA兰里市正式方法研讨会会议记录,2000年7月

[6]John Clark,Nigel Tracey.求解轻型反坦克武器LAW中的约束条件.LAW/D5.1.1(E),欧洲委员会-国防指南DG第三产业,1997.遗产评定工作-替补可行性评估

[7]Richard A.DeMillo,Richard J.Lipton,Frederick G.Sayward.选取测试数据的暗示：帮助练习程序员.IEEE计算机,34-41页,1978年四月

[8]J Dick,A Faivre.基于模型规范的测试用例自动生成与排序.FME’93:工业力量形式方法,欧洲.LCNS670,268-284页,1993年四月

[9]John B Goodenough,Susan L Gerhart.测试数据选取原理.关于软件工程IEEE汇报,1(2):156-173,1975年六月

[10]VDM-SDL工具组.IFAD VDM-SL语言.计算机科学应用协会,1994年九月

[11]PAV Hall.关于正式规范的测试.软件工程第二次IEE/BCS会议,159-163页,1998

[12]Daniel Jackson,Craig Damon.设计风格元素:用反例检测器分析软件设计特征.关于软件工程IEEE汇报,22(7):484-495,1996七月

[13]A.K.Mackworth.关系网络中的一致性.人工智能,8:99-118,1977

[14]Thomas J Ostrand,Marc J Balcer.指定和生成功能测试的分类划分法.ACM通信,31(6):676-686,1988年六月

[15]Martyn Ould.测试—— 一个对方法和工具开发者的挑战.软件工程杂志,39:59-64,March 1991

[16]J.M.Spivey.Z表示法:参考手册,第二版.普伦蒂斯·霍尔(出版社),1992

[17]Phil Stocks,David Carrington.测试模板框架:基于规范的案例研究.软件测试与分析国际座谈会（ISSTA’93）会议记录,11-18页,1993

[18]Phil Stocks,David Carrington.基于规范的测试框架.软件工程IEEE汇报,22(11):777-793,1996年十一月

[19]I.Toyn.用CADiZ对Z表示法中的形式推论.关于定理证明系统用户界面设计的第二届国际研讨会,1996年七月

[20]Ian Toyn.关于Z规范的推理策略语言.第三届北方形式方法研讨会,克雷,英国,1998年九月

¹在Z模式中，规定 ?和 !分别代表输入和输出。

²可粗略地理解为：对n?和r! ，存在一些满足范式的值，所以可以被用作适当的测试数据。

³也依赖比如[11,14,8]领域中的其它重要工作。

测试，证明及自动化——集成化方法相关推荐

谷歌YouTube算法团队：视频质量评价的集成池化方法
点击我爱计算机视觉标星,更快获取CVML新技术随着移动互联网的发展,视频成为信息消费越来越重要的形式(这从国内外的YouTube.抖音的发展可见一斑),而其中用户贡献内容(UGC)往往占很大比例. ...
第七章移动自动化持续化集成（下）
--------手机自动化之Appium (4)增加构建步骤,这是如何执行我们项目工程的命令,如:python src/TestSuites/OnlineTestSuite.py.构建的时候就会执行这 ...
selenium自动化测试_维持Selenium测试自动化的完美方法
selenium自动化测试毫无疑问, 自动浏览器测试已改变了软件开发的工作方式. 如果不是Selenium,我们将无法像我们一样使用各种各样的无错误的Web应用程序. 但是有时,甚至IT部门也误解了 ...
维持硒测试自动化的完美方法
毫无疑问, 自动浏览器测试已经改变了软件开发的工作方式. 如果不是Selenium,我们将无法像我们一样使用各种各样的无错误Web应用程序. 但是有时,甚至IT部门也误解了自动化一词. 大多数人认为计 ...
揭秘基于MBSE集成化的汽车电子解决方案
随着汽车销量的不断增长以及自动驾驶技术的快速发展,汽车行业对安全性.自动化等要求越来越高,加之智能化技术逐渐走进人们的生活,使得汽车电子的设计难度成倍增长. 挑战系统设计复杂汽车电子化.智能化程度 ...
【二十二】win 10 ：Jmeter 报告可视化 —— 配置 Jmeter 接口 HTML 可视化测试报告，Jenkins + Jmeter + Ant 自动化集成环境搭建
目录一.环境搭建二.文件下载三.文件配置四.本地调试五.创建.bat文件六.Jenkins配置邮件七.配置测试项目八.自动部署成功校检九.jmeter仪表盘HTML报告自动化构建一 ...
基于Armitage的MSF自动化集成攻击实践
基于Armitage的MSF自动化集成攻击实践目录 0x01 实践环境 0x02 预备知识 0x03 Armitage基础配置 0x04 Nmap:Armitage下信息搜集与漏洞扫描 0x05 A ...
简易自动电阻测试仪_开始自动测试您的网站的简单方法
简易自动电阻测试仪 by Adam Kelly 通过亚当凯利开始自动测试您的网站的简单方法 (The easy way to start automatically testing your web ...
用于视觉识别的深度卷积网络空间金字塔池化方法
摘要现有的深卷积神经网络(CNN)需要一个固定大小的神经网络(例如224x224)的输入图像.这种要求是"人为的",可能会降低对任意大小/尺度的图像或子图像的识别精度.在这项工作 ...

测试，证明及自动化——集成化方法

测试，证明及自动化——集成化方法相关推荐

最新文章

热门文章