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