11章 净室软件工程

第11章净室软件工程基本概念净室策略功能规格说明净室设计净室测试认证11.1基本本概念净室软件件工程(Cleanroomsoftwareengineering)是一种在在软件开开发过程程中强调调在软件件中建立立正确性性要求的的方法。。与传统的的分析、、设计、、编码、、测试和和调试的的周期观观点有所所不同。。净室方法法的观点点：通过在第第一次正正确地书书写代码码增量，，并在测测试前验验证它们们的正确确性来避避免成本本很高的的缺陷消消除过程程。它的的过程模模型是在在代码增增量集成成到系统统的同时时，进行行代码增增量的统统计质量量验证。。11.1基本本概念与形式化化方法技技术一样样，净室室过程强强调规格格说明和和设计上上的严格格性，并并且使用用基于数数学的正正确性证证明来对对结果设设计模型型的每个个元素进进行形式式化验证证。净室方法法不是先先制造一一个产品品，然后后再去消消除缺陷陷，而是是要求在在规格说说明和设设计中消消除错误误，然后后以“干干净”的的方式进进行制造造。净室方法法还对形形式化方方法进行行了扩展展，强调调统计质质量控制制技术，，包括基基于客户户对软件件的预期期使用的的测试。。11.1基本本概念“第一次次就将事事情做正正确”是是软件工工程最重重要的哲哲学。净室软件件工程是是这样一一个过程程：它强强调在程程序构造造开始前前进行正正确性的的数学验验证，并并且将软软件可靠靠性认证证作为软软件测试试的一部部分。其底线是是极低的的故障率率，这是是使用非非形式化化方法难难于或不不可能达达到的。。11.1基本本概念20世纪80年代，Mills、Dyer、及Linger最先建议议将净室室原理应应用于软软件工程程。虽然在软软件开发发的早期期，人们们对其抱抱以很大大的希望望，但它它并没有有得到广广泛的使使用。

11.1基本本概念Henderson提出了没没有得到到广泛使使用的三三个原因因：1.净室方法法学太理理论化、、太数学学化、太太激进，，难于在在实际的的软件开开发中使使用。2.它提倡开开发者不不需要进进行单元元测试，，而是进进行正确确性验证证和统计计质量控控制，这这些观念念与当前前大多数数软件开开发方式式有很大大的偏离离。11.1基本本概念3.软件开发发产业的的成熟度度不高。。使用净净室过程程需要在在整个生生命周期期阶段严严格按照照定义的的过程进进行。由由于大多多数软件件企业的的运作还还处于过过程成熟熟度中的的较低级级别，软软件工程程师还没没有准备备应用净净室技术术。11.1基本本概念“程序中中出现错错误的唯唯一方式式是作者者将错误误引入进进去的。。没有其其他方式式……正确实践践的目标标是：设设法避免免引入错错误，如如果引入入了错误误，通过过测试或或任何其其他运行行程序的的方式来来消除错错误。””HarlanMills11.1基本本概念11.2净室室策略净室方法法使用增增量过程程模型。。一个“软软件增量量的流水水线”由由若干小小的、独独立的软软件团队队开发。。每当一个个软件增增量通过过认证，，它就被被集成到到整体系系统中。。因此，，系统的的功能随随时间增增加。一旦将功功能分配配给系统统的软件件元素，，则可启启动净室室增量的的流水线线。需要完成成的任务务如下：：(1)增量策划划。制定一一个采用用增量策策略的项项目计划划，确定定每个增增量的功功能、预预计规模模、及净净室开发发进度。。(2)需求收集集。为每个个增量开开发更详详细的客客户级需需求描述述。

11.2净室室策略(3)盒结构规规格说明明。运用盒盒结构的的规格说说明方法法描述功功能规格格说明。。遵从操操作分析析原则，，盒结构构“在每每一个精精化级别别上使行行为、数数据及过过程的创创造性定定义独立立”。(4)形式化设设计。使用盒盒结构方方法，净净室设计计是规格格说明的的自然、、无缝扩扩展。对规格说说明(称为黑盒盒)进行迭代代求精(在一个增增量内)类似于体体系结构构设计和和构件级级设计(分别称为为“状态态盒”和和“清晰晰盒”)。

11.2净室室策略(5)正确性验验证。净室团团队对设设计及代代码进行行一系列列严格的的正确性性验证活活动。验证从最最高层次次的盒结结构(规格说明明)开始，然然后移向向设计细细节和代代码。正确性验验证的第第一层次次通过应应用一组组“正确确性问题题”来进进行，如如果这些些没有证证明规格格说明是是正确的的，则使使用更形形式化的的(数学的)验证方法法。11.2净室室策略(6)代码生成成、检查查和验证证。以某种种专门语语言表示示的盒结结构规格格说明被被翻译为为适当的的程序设设计语言言。然后后，使用用标准的的走查或或检查技技术来保保证代码码和盒结结构的语语义相符符性，以以及代码码的语法法正确性性。最后后，对源源代码进进行正确确性验证证。

11.2净室室策略(7)统计测试试规划。分析软软件的预预计使用用情况，，规划并并设计一一组测试试用例，，以测试试使用情情况的““概率分分布”。

11.2净室室策略(8)统计使用用测试。对计算机机软件进进行穷举举测试是是不可能能的，因因此，设设计有限限数量的的测试用用例总是是必要的的。统计使用用技术执执行由统统计样本本导出的的一系列列测试，，这里的的统计样样本是从从来自目目标人群群的所有有用户对对程序的的所有可可能执行行中抽取取的。11.2净室室策略(9)认证。一旦完完成验证证、检查查和使用用测试(并且所有有错误被被改正)，则对增增量进行行集成前前的认证证工作。。11.2净室室策略净室方法法的特异异之处明确使用用统计质质量控制制。使用基于于数学的的正确性性证明来来验证设设计规格格说明。。实现了一一些测试试技术，，这些测测试技术术最有可可能揭示示具有严严重影响响的错误误。

净室软件件工程和和传统软软件实践践的差别别在于：：它不再再强调(有些人称称取消)单元测试试和调试试的作用用，从而而大量地地减少(或取消)由软件开开发者所所承担的的测试工工作量。。在净室软软件工程程中，单单元测试试和调试试被正确确性验证证和基于于统计的的测试所所替代。。净室方法法的特异异之处11.3功能能规格说说明不管选择择哪种分分析方法法，操作作分析原原理总是是适用的的。对数数据、功功能和行行为建模模，并对对结果模模型进行行分解,提供更进进一步的的详细信信息。总体目标标是从捕捕获问题题实质的的规格说说明(模型)移向提供供重要实实现细节节的规格格说明。。净室软件件工程通通过使用用盒结构规格说明明的方法法来遵从从操作分分析原则则。一个“盒盒”在某某个细节节层次上上封装系系统(或系统的的某些方方面)。通过逐步步求精的的过程，，盒被精精化为层层次。“每个盒规规格说明明的信息息内容足足以定义义其精化化，不需需要依赖赖任何其其他盒的的实现””。这使得分分析员能能够按层层次划分分一个系系统——从顶层的的基本表表示到底底层实现现的特定定细节。。11.3功能能规格说说明有三种类类型的盒盒：黑盒，状状态盒，，清晰盒盒黑盒。黑盒刻刻画系统统行为或或系统部部件的行行为。通通过运用用由触发发映射到到反应的的一组转转换规则则，系统统(或部件)对特定的的触发(事件)做出反应应。状态盒。状态盒盒以类似似于对象象的方式式封装状状态数据据和服务务(操作)。在这种种规格说说明视图图中，表表示出状状态盒的的输入(触发)和输出(反应)。清晰盒。在清晰晰盒中定定义状态态盒所蕴蕴含的转转换功能能，简单单地说，，清晰盒盒包含了了对状态态盒的过过程设计计。11.3功能能规格说说明黑盒规格格说明黑盒规格格说明描描述一种种抽象、、触发和和反应。。函数f被应用到到输入(触发)S的序列S*，并将它们们变换为为输出(反应)R。对于简单单的软件件构件，，f可以是一一个数学学函数，，但一般般情况下下，使用用自然语语言(或形式化化规格说说明语言言)描述f。黑盒规格格说明为面向对对象系统统引入的的很多概概念也适适用于黑黑盒。黑盒封装装数据抽抽象和操操纵抽象象数据的的操作。。和类层次次一样，，黑盒规规约可以以展示使使用层次次，其中中，低层层盒从树树结构中中的高层层盒继承承属性。。黑盒规格格说明状态盒规规格说明明一个状态态是某个个可观查查到的系系统行为为的模型型。当进进行处理理时，一个系统统对事件件(触发)作出反应应，从当当前状态态转换到到某一新新的状态态。当进行行转换时时，可能能发生某某个动作作。状态盒使使用数据据抽象来来确定到到下一个个状态的的转换、、以及状状态转换换后将要要发生的的动作(反应)。状态盒同同黑盒协协作。来来自某外外部源及及一组内内部系统统状态T的触发S被输入到到黑盒中中。包含在状状态盒内内的黑盒盒的函数数g的数学描描述：g∶S*×T*→R×T这里g是和特定定状态t连接的子子函数。。当整体体地考虑虑时，状状态—子函数对对(t，g)定义了黑黑盒函数数f。状态盒规规格说明明状态盒规规格说明明清晰盒规规格说明明清晰盒规规格说明明是与过过程设计计及结构构化编程程紧密关关联的。。状态盒中中的子函函数g被实现g的结构化化编程结结构所替替代。清晰盒规规格说明明11.4净室室设计净室软件件工程中中使用的的设计方方法主要要运用结结构化程程序设计计的原理理。基本的处处理函数数(在规格说说明的早早期求精精中描述述)被精化，，其方法法是“将数学函函数逐步步扩展为为逻辑连连接词(如，if-then-else))和子函数数构成的的结构，，这种扩扩展一直直进行下下去，直直到所有有标识出出来的子子函数可可以用程程序设计计语言直直接表达达”。设计求精精与验证证每个清晰晰盒规格格说明代代表了一一个完成成状态盒盒转换所所需的过过程(子函数)的设计。。对清晰盒盒规格说说明，使使用结构构化程序序设计结结构和逐逐步求精精。一个程序序函数f被细化为为子函数数g和h的序列，，这些又又被进一一步细化化为条件件结构(if--then-else和do-while)。进一步的的求精给给出了连连续的逻逻辑细化化。在每个求求精层次次，净室室团队执执行一次次形式化化正确性性验证。。为此，，将一类类正确性性条件集集合附加加到结构构化程序序设计结结构上。。如果函数数f被扩展为为序列g和h，则f所有输入入的正确确性条件件是：执行g之后再执执行h能完成f的功能吗吗？如果一个个函数p被精化为为形为if＜c＞thenqelser的条件形形式，则则对p的所有输输入的正正确性条条件是：：只要条件件＜c＞为真，q能完成p的功能吗吗？只要条件件＜c＞为假，r能完成p的功能吗吗？

设计求精精与验证证如果一个个函数m被细化为为循环donwhile＜c＞则对m的所有输输入的正正确性条条件是：：能够保证证循环终终止吗？？只要＜c＞为真，，循环执执行n之后能完完成m的功能吗吗？只要＜c＞为假，，退出循循环仍能能完成m的功能吗吗？设计求精精与验证证每当一个个清晰盒盒被精化化为下一一个详细细层次时时，都应应用上面面给出的的正确性性条件。。值得注意意的是：：结构化化程序设设计结构构的使用用限制了了必须进进行的正正确性测测试的数数量。对顺序结结构只检检查单个个条件，，对if-then-else结构只测测试两个个条件，，对循环环则只验验证三个个条件。。设计求精精与验证证例：过程程设计的的正确性性验证：：设计并并验证一一个小的的程序，，该程序序对某给给定的整整数x，找出其平平方根的的整数部部分y。

yesno设计求精精与验证证定义入口口和出口口条件。。为了证明明设计的的正确性性，需要要证明图图中表示示的条件件init、loop、cont、yes和exit在所有情情形下都都是正确确的。设计求精精与验证证1.条件init要求［x≥0andy==0］。基于问题题的需求求，假定定入口条条件是正正确的。。因此，，init条件的第第一部分分x≥0是满足的的。在流流程图中中，在init条件前的的语句设设置y=0，因此，init条件的第第二部分分也是满满足的，，因此，，init为真。2.条件loop可能以两两种方式式之一出出现：(1)直接从init(此时loop条件被直直接满足足)，或(2)通过穿过过条件cont的控制流流。因为为条件cont与条件loop相同，因因此，不不管从哪哪条路径径到达它它，条件件loop都为真。。3.条件cont:只有在y值被递增增1后，才能能遇到条条件cont。另外，只只有在条条件yes也为真时时，才能能调用到到达条件件cont的控制流流路径。。因此，，如果(y+1)2≤x，则y2≤x，条件cont成立。4.条件yes在如图所所示的条条件逻辑辑中被测测试，因因此，当当控制流流沿着所所示的路路径移动动时，条条件yes一定为真真。5.条件exit首先要求求x保持不变变，对设设计进行行检查可可发现x没有出现现在赋值值操作的的左边，，没有使使用x的函数调调用，因因此，x保持不变变。因为为条件测测试(y+1)2≤x不成立时时，才可可能到达达条件exit，因此(y+1)2＞x成立。此此外，loop条件还必必须保持持为真(即，y2≤x)，因此，(y+1)2＞x和y2≤x可以组合合在一起起满足exit条件。保证循环环终止:因为y是递增的的，而x≥0，因此，最最后(y+1)2≤x不成立，，循环一一定终止止。设计求精精与验证证设计验证证的优点点对清晰盒盒设计的的每一步步求精进进行严格格的正确确性验证证有许多多显著的的优点：：(1)将验证简简化为一一个有限限的过程程。在清清晰盒中中，以嵌嵌套的、、顺序的的方式组组织控制制结构，，这就自自然地定定义了一一个层次次，该层层次显示示了必须须被验证证的正确确性条件件。(2)再怎么强强调将验验证简化化为有限限过程对对质量产产生的正正面效果果都不过过分。除除了那些些最微不不足道的的程序，，即使所所有程序序都具有有无限数数目的可可执行路路径，也也可以在在有限步步骤内对对它们进进行验证证。(3)使得净室室团队验验证设计计和代码码的每一一行。在在正确性性定理的的基础上上，团队队可以通通过小组组分析和和讨论来来执行验验证，并并且当在在生命关关键或使使命关键键的系统统中需要要额外的的信心时时，可以以生成书书面的证证明。(4)达到几乎乎零缺陷陷的水平平。在团团队的复复审过程程中，每每个控制制结构的的每个正正确性条条件被依依次验证证。每个个团队成成员必须须就每个个条件都都是正确确的达成成共识，，这样只只有团队队的每个个成员均均未能正正确地验验证某条条件时，，才有可可能出现现错误。。设计验证证的优点点(5)具有可伸伸缩性。。每个软软件系统统，不管管有多大大，均具具有顶层层的由顺顺序、选选择和循循环结构构构成的的清晰盒盒过程。。(6)产生出比比采用单单元测试试更好的的代码。。单元测测试仅仅仅检查从从很多可可能的路路径中选选出的测测试路径径的执行行效果。。基于函函数验证证的理论论，净室室方法可可以验证证所有数数据的每每个可能能的结果果，因为为虽然一一个程序序可能有有很多可可执行路路径，但但它只有有一个函函数。验验证也比比单元测测试更有有效，可可以在几几分钟之之内检查查大多数数验证条条件，但但单元测测试要花花费大量量时间去去准备、、执行和和检查。。设计验证证的优点点11.5净室室测试净室测试试的策略略在根本本上不同同于传统统测试方方法。传传统测试试方法导导出一组组测试用用例发现现设计和和编码错错误；净室测试试的目的的是：通通过证明明用例的的统计样样本的成成功运行行来确认认软件需需求。统计使用用测试计算机程程序的用用户没有有必要去去了解设设计的技技术细节节。程序的用用户可见见的行为为通常是是由用户户产生的的输入和和事件所所驱动的的。在复杂系系统中，，输入和和事件的的可能的的范围(即用例)是非常广广泛的。。什么样样的用例例子集能能够充分分验证程程序的行行为？这这是统计计使用测测试关注注的第一一个问题题。统计使用用测试““等同于于以用户户试图使使用软件件的方式式来测试试软件””。为了完成成测试工工作，净净室测试试团队（（也称为为认证团团队）必必须确定定软件的的使用概概率分布布。对软件的的每个增增量的规规格说明明(黑盒)进行分析析，并定定义一组组使软件件改变其其行为的的触发(输入或事事件)。通过与潜潜在用户户的交流流、使用用场景的的建立、、及对应应用领域域的全面面了解，，为每个个触发分分配一个个使用概概率。按照使用用概率分分布为每每个触发发集合生生成测试试用例。。统计使用用测试例，在家家庭保安安系统中中，使用用净室软软件工程程方法开开发一个个软件增增量来管管理用户户与安全全系统键键区之间间的交互互。对这这个增量量，已经经标识出出5个触发。。通过分分析，给给出每个个触发的的概率分分布百分分数。为为了更容容易地选选择测试试用例，，这些概概率被映映射到1至99的数字区区间。统计使用用测试为了生成成符合使使用概率率分布的的使用测测试用例例序列，，生成1至99之间的随随机数。。每个随随机数与与前面概概率分布布的一个个区间相相对应。。因此，，使用测测试用例例序列可可以随机机定义，，但又与与触发发发生的适适当概率率相对应应。例