第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)产生出比采用单元测试更好的代码。单元测试仅仅检查从很多可能的路径中选出的测试路径的执行效果。基于函数验证的理论，净室方法可以验证所有数据的每个可能的结果，因为虽然一个程序可能有很多可执行路径，但它只有一个函数。验证也比单