|
|
|
净室软件工程（净室方法）是软件开发的一种形式化方法，它可以生成高质量的软件。它使用盒结构规约进行分析和设计建模，并且强调将正确性验证（而不是测试）作为发现和消除错误的主要机制，使用统计的测试来获取认证被交付的软件的可靠性所必需的出错率信息。
|
|
|
|
净室方法从使用盒结构表示的分析和设计模型入手，一个“盒”在某特定的抽象层次上封装系统（或系统的某些方面），通过逐步求精的过程，盒被精化为层次，其中每个盒具有引用透明性：每个盒规约的信息内容对定义其精华是足够的，不需要信赖于任何其他盒的实现。这使得分析人员能够层次地划分一个系统，从在顶层的本质表示转向在底层的实现特定的细节。净室方法主要使用三种盒类型：
|
|
|
|
（1）黑盒。这种盒刻划系统或系统的某部分的行为。通过运用由激发得到反应的一组变迁规则，系统（或部分）对特定的激发（事件）作出反应。
|
|
|
|
（2）状态盒。这种盒以类似于对象的方式封装状态数据和服务（操作）。在这个规约视图中，表示出状态盒的输入（激发）和输出（反应）。状态盒也表示黑盒“激活历史”，即，封装在状态盒中的，必须在蕴含的变迁间保留数据。
|
|
|
|
（3）清晰盒。在清晰盒中定义状态盒所蕴含的变迁功能，简单地说，清晰盒包含了对状态盒的过程设计。
|
|
|
|
一旦完成了盒结构设计，则运用正确性验证。软件构件的过程设计被划分为一系列子函数，为了证明每个子函数的正确性，要为每个函数定义出口条件并实施一组子证明。如果每个出口条件均满足，则设计一定是正确的。
|
|
|
|
一旦完成了正确性验证，便开始统计的使用测试。和传统测试不同，净室软件工程并不强调单元测试或集成测试，而是通过定义一组使用场景、确定对每个场景的使用概率及定义符合概率的随机测试来进行软件测试（这种活动称为正确性验证）。将产生的错误记录和取样、构件和认证模型相结合使得可以数学地计算软件构件的可靠性（这种活动称为基于统计的测试）。
|
|
|
|
净室方法是一种严格的软件工程方法，它是一种强调正确性的数学验证和软件可靠性的认证的软件过程模型，其目标和结果具有非常低的出错率，这是使用非形式化方法难于或不可能达到的。
|
|
|
