第五章、软件工程中的形式化方法 本章涉及到离散数学与数据结构的知识，可见知识都是互通的。1.形式化方法基本概念分为形式规约、形式证明与验证、程序求精，形式证明与验证技术主要包括模型检测和定理证明。2.时态逻辑介绍了Kripke结构；一阶线性时态逻辑以队列及其操作与汉诺塔操作规划问题为例进行讲解。计算树逻辑一般是CTL与CTL*的统称。3.模型检测就是在软件系统的Kripke结构模型下，对以CTL*公式给出的软件性质的正确性验证。4.Z语言本节对Z语言进行详细的概述与讲解，并以停车场管理系统与图书管理系统为例详细讲解。5.Petri网任何系统都可抽象为两类元素:状态和事件。首先进行讲解，最后以信号灯的Petri网规格实例进行验证。