|
分类方法 |
具体方法 |
描述 |
|---|---|---|
|
开发风格 |
自顶向下方法 |
系统的整体结构首先被定义和设计，然后逐步细化为更具体的模块和功能 |
|
自底向上方法 |
是一种从具体模块开始逐步构建整个系统的方法 |
|
|
性质 |
形式化方法 |
形式化方法是一种具有坚实数学基础的方法 |
|
非形式化方法 |
非形式化方法则不把严格性作为其主要着眼点 |
|
|
适应范围 |
整体性方法 |
适用于软件开发全过程的方法称为整体性方法 |
|
局部性方法 |
适用于开发过程某个具体阶段的软件方法称为局部性方法 |
形式化方法
形式化方法是指在软件开发过程中，使用严格的数学模型和形式化语言来描述系统的需求、设
计和行为，并通过逻辑推理或模型检测等形式化验证手段，证明软件在所有可能的运行情况下都满
足既定规范，从而获得可证明的软件正确性。它关注的不仅是测试能否发现错误，而是从理论上保
证程序在功能、行为、安全性和活性等方面“必然正确”，常用于安全攸关或高可靠性系统的软件开
发与验证。
这里需要掌握形式化方法的特点。（1）正确性验证难且耗时，数学模型和证明困难。（2）仍
然需要和传统测试相结合。形式化方法提供理论保证，而测试则负责实际运行和发现运行时错误，
不能说有了形式化方法，软件开发就不需要测试了。
净室软件工程
净室软件工程（Cleanroom Software Engineering， CSE）首先是一种上面提到的“形式化方法”，
这一点非常关键。它不是测试方法、不是管理模型、也不是单纯的过程模型，而是强调用数学与统
计理论，在设计和规约阶段消除错误的软件工程方法。它的理论基础是函数理论和抽样理论，如下
表所示。