软件工程理论、方法与实践（第五章）

软件工程中的形式化方法

本章介绍软件工程中的形式化方法，包括时序逻辑、Z语言、Petri网等。

软件规格说明是对软件系统对象，对象的操作方法，以及对象行为的描述。在系统的开发及演化过程中，对象、对象的性质以及操作应作为一个整体来处理。软件生命周期中的不同阶段为规格说明引入和增加新的系统特征定义。当规格说明用形式化方法描述时，可称之为“形式规约”。形式证明与验证技术主要包括模型检测和定理证明。程序求精是将自动推理和形式化方法相结合，从抽象的形式规约推演出具体的面向计算机的程序代码的全过程。Z语言为系统建立基于状态的模型，模型的三个主要组成部分是输入、输出和状态。Petri网分为位置/迁移Petri网和高级Petri网两类。