第五章：软件工程中的形式化方法
形式化方法是指将离散数学的方法用于解决软件工程领域的问题，主要包括建立精确的数学模型以及对模型的分析活动。软件的设计过程就是一个建立形式规约的过程。实际上就是把现实世界的需求映射成软件的模型化过程即在现实世界、模型表示和计算机系统之间进行描述和转化的过程。开发过程中的任务包括：模型获取、模型验证、模型变化。包括时态逻辑、一阶线性时态逻辑（队列及其操作、汉诺塔操作规划问题）、计算树逻辑等模型及模型检验。
Z语言为系统建立基于状态的模型。模型的三个主要组成部分是输入、输出和状态。数据抽象和过程抽象是软件规格说明过程中的两类重要抽象。Z语言表示：集合、关系及函数（幂集、元组合笛卡尔积、关系与函数、队列和包）、自由类型和模式。
Petri网具有顺序、并发、冲突、混惑等结构描述能力。任何系统都可抽象为状态和事件两类元素。变迁是Petri网种的主动元素。