本章的主要内容是软件工程中的形式化方法
形式化方法基本概念
形式规约
软件规格说明是对软件系统对象，对象的操作方法，以及对象行为的描述。
当规格说明用非形式化方法描述时，可称之为“规格说明”，当规格说明用形式化方法描述时，可称之为“形式规约”。
非形式化的规格说明可用自然语言、图、表等形式来描述。因为其具有严格的语法和语义定义，从而准确的描述系统模型，排出了矛盾、二义性、含糊性等情况。
目前，已建立了多种适用于软件规格说明的形式化方法。从形式规约到目标软件系统的可实现和可执行角度，可分为操作类和描述类。操作类：有限状态机、Statecharts、Petri网等；描述类：1. 基于代数的方法：Z、VDM、Larch等；2.基于逻辑的方法：一阶线性时态逻辑（FOLTL）、计算树逻辑(CTL)等。
形势证明与验证
形势证明与验证技术主要包括模型检测和定理证明：
模型检测主要适用于有穷状态系统，优点是完全自动化并且验证速度快。模型检测离不开检验工具的支持。根据所验收规矩的特点，已有的模型检测工具有时态逻辑模型检测工具：EMC、SMV、SPIN等；行为一致性检测工具：FDR、Cospan/Formal Check等；复合检测工具：HSIS、METAFrame等。
定理证明采用逻辑公式来表示系统规约及其性质，其中的逻辑由一个具有公里和推理规则的形式化系统给出，进行定理证明的过程就是应用这些公理货推理规则来证明系统具有某些性质。定理证明同样需要定理证明器的支持。现有的定理证明器包括：用户导引自动推演工具：ACL2、LP、Eves等；证明检验器：HOL、LCF、LEGO等；复合证明器：PVS和Step将决策过程、模型检测和交互式证明组合使用。
程序求精
程序求精是将自动推理和形式化方法相结合，从抽象的形式规约推演出具体的面向计算机的程序代码的全过程。
时态逻辑
Kripke 结构 三元组 M = ( W , R , L ) 称为模态逻辑的一个模型，或者Kripke结构（模型），其中 W 是可能世界的非空集合; R ∈ W * W是可能世界W上的二元关系；L： W → 2的P次方（P是原子公式集合）是标记函数。它是对各可能世界的真值派，即对每个模态逻辑公式，指明它在每个可能世界中取真值还是假值。
一阶线性时态逻辑
一阶线性时态逻辑公式，简称 FOLTL 公式，定义如下：
①原子谓词公式是 FOLTL 公式；
②如果A、B是 FOLTL 公式，那么（非A）、（A∧B）、（A∨B）、（A→B）、（A↔B）是FOLTL公式；
③如果A是FOLTL公式，x是A中出现的变量（个体变元），则存在x • A、任意x • A 是FOLTL公式；
④如果A、B是FOLTL公式，那么（◇A）、（□A）、（○A）、（A▷B）是FOLTL公式；
⑤当且仅当有限次地使用①②③④所组成的符号串是FOLTL的应用。
计算书逻辑
计算树逻辑（CTL）是一种离散、分支时间、命题时态逻辑。
计算树逻辑公式，简称CTL公式，定义如下：
①原子命题（命题常量或变量）是CTL公式；
②如果 φ、ψ 是CTL公式，那么（非φ）、（φ∧ψ）、（φ∨ψ）、（φ→ψ）、（φ↔ψ）是CTL公式；
③如果 φ、ψ 是CTL公式，那么（A○ψ）（E○ψ）（A◇ψ）（A□ψ）（E□ψ）（A（φ▷ψ）（E（φ▷ψ）是CTL公式；
④当且仅当有限次的使用①②③所组成的符号串是 CTL 公式。
模型检验
软件的计算树逻辑规格可以通过模型检验得到验证。模型检验就是在软件系统的Kripke 结构模型下，对以 CTL*公式给出的软件性质的正确性检验。标记算法是模型检验的一个简单算法。
Z 语言）
概述
Z 语言为系统建立基于状态的模型。模型的三个主要组成部分是输入、输出和状态，他们均有相应的数学概念来描述。通常，一个Z语言形式规范文档包括以下内容：1. 给定类型的声明和全局变量及常量定义；2. 系统的抽象状态描述；3. 系统的初始化定义；4. 对正常条件下系统操作的定义；5. 计算已经定义的操作的前置条件；6. 描述完整的操作（可能的出错情况下对操作的定义）；7. 对规格说明的一些性质进行证明；8. 建立规格说明的摘要和目录。
Z 语言表示
1. 集合、关系及函数：集合、幂集、元组和笛卡尔积、关系与函数、队列和包。2. 自由类型和模式。
Z 语言实例
停车场管理系统的例：有以下几部分组成：1. 基本数据类型定义；2. 全局变量声明；3. 状态定义；4. 初始化；5. 操作定义。
Petri网
基本定义
任何系统都可以抽象为两类元素：状态和事件。
Petri 网结构：Petri网结构是一个三元组 N = （P，T，F），其中：① P = {p1,p2,......pn} 是有限库所集合；② T = {t1,t2,......tn} 是有限变迁集合（P∪T≠∅,P∩T＝∅）;③ F ≦ （ P × T ）∪ ( T × P ) 为流关系。
前集和后集 对于一个 Petri 网结构 N = （P，T，F），设 x ∈ ( P ∪ T ) ,令 ·x = {y | 存在y : ( y , x ) ∈ F} x· = {y | 存在y : ( x , y ) ∈ F} 。那么称 ·x 为 x 的前集或输入集，称 x· 为 x 的后集或输出级。
Petri网具有丰富的结构描述能力：顺序关系、并发关系、冲突关系、混惑关系。
Petri网规格实例——信号灯
交通灯Petri网表示：
信号灯可以用