下载文档原格式
04章形式化说明技术形式化说明技术（Formal Specification Techniques）是一种系统性、精确地描述和定义软件系统执行行为、功能和性质的技术方法。
它通过使用数学语言和形式规约的方法，将软件系统的设计和实现过程从自然语言的模糊性和歧义性中解放出来，从而改善了软件开发和维护的效率和质量。
形式化说明技术的核心思想是将软件系统描述为一个数学模型，通过形式化的推理和证明，确保系统满足设计要求并具备所需的性质。
形式化说明技术不仅能够精确地描述系统的行为和功能，还可以检查系统的正确性、一致性、完备性、可靠性和安全性等方面的属性，提前发现和解决潜在的问题。
形式化说明技术的应用范围广泛，包括需求分析、系统设计、编码验证、软件测试、系统仿真和代码生成等方面。
下面将介绍几种常见的形式化说明技术。
1. 判定性有穷状态自动机（Deterministic Finite State Automaton，DFSA）：DFSA 是一种常用的形式化说明技术，用于描述系统的状态和状态转移。
它可以形式化地描述系统的行为，通过状态转移图来表示系统的状态变化，从而帮助开发人员更好地理解和设计系统。
2. 时序逻辑（Temporal Logic）：时序逻辑是一种扩展的命题逻辑，用于描述系统的时序性质。
通过形式化的规约、语义和推理，可以验证系统是否满足时序性质，如安全性、活性、不变性等。
时序逻辑广泛应用于软硬件系统的验证和验证。
3. Petri 网（Petri Nets）：Petri 网是一种用于建模和分析并发系统的图形化形式化说明技术。
Petri 网通过描述系统的状态、变迁和资源，揭示系统的并发行为和资源竞争情况，从而帮助开发人员理解和设计并发系统。
4. Z 规范（Z Specification）：Z 规范是一种基于集合论和一阶谓词逻辑的形式化说明技术，用于描述系统的状态、操作和约束等。
Z 规范通过形式化地定义系统的状态集合、操作集合和约束条件，帮助开发人员更好地理解和设计系统。
形式化说明技术按照形式化的程度，可以把软件工程使用的方法划分成非形式化，半形式化和形式化3类。
用自然语言描述需求规格说明，是典型的非形式化方法。
用数据流图或实体—联系图建立模型，是典型的半形式化方法。
所谓形式化方法，是描述系统性质的基于数学的技术，也就是说，如果一种方法有坚实的数学基础，那么它就是形式化的。
4.1 概述4.1.1 非形式化方法的缺点用自然语言书写的系统规格说明书，可能存在矛盾、二义性、含糊性、不完整性及抽象层次混乱等问题。
所谓矛盾是指一组相互冲突的陈述。
例如，规格说明书的某一部分可能规定系统必须监控化学反应容器中的温度，而另一部分（可能由另一位系统分析员撰写）却规定只监控在一定范围内的温度。
如果这两个相互矛盾的规定写在同一页纸上，自然很容易查出，不幸的是，它们往往出现在相距几十页甚至数百页的两页纸中。
二义性是指读者可以用不同方式理解的陈述。
例如，下面的陈述就是具有二义性：“操作员标识由操作员姓名和密码组成，密码由6位数字构成。
当操作员登录进系统时它被存放在注册文件中。
”在上面这段陈述中，“它”到底代表“密码”还是“操作员标识”，不同的人往往有不同的理解。
系统规格说明书是很庞大的文档，因此，几乎不可避免地会出现含糊性。
例如，我们可能经常在文档中看到类似下面这样的需求：“系统界面应该是对用户友好的。
”实际上，这样笼统的陈述并没有给出任何有用的信息。
不完整性可能是在系统规格说明中最常遇到的问题之一。
例如，考虑下述的系统功能需求：“系统每小时从安放在水库中的深度传感器获取一次水库深度数据，这些数值应该保留6个月。
”假设在系统规格说明书中还规定了某个命令的功能：“AVERAGE命令的功能是，在PC机上显示由某个传感器在两个日期之间获取的平均水深。
”如果在规格说明书中对这个命令的功能没有更多的描述，那么，该命令的细节是严重不完整的，例如，对该命令的描述没有告诉我们，如果用户给定的日期是在当前日期的6个月之前，那么系统应该做什么。
