软件工程概论
第五章 软件工程中的形式化方法
1.形式化方法基本概念
形式约束：软件规格说明是软件系统对象，对象的操作方法，以及对象行为的描述。在系统的开发及演化过程中，对象，对象的性质以及操作应作为一个整体来处理。
形式证明与验证：主要包括模型检验和定理证明。
程序求精：是将自动推理和形式化方法相结合，从抽象的形式规约推演出具体的面向计算机的程序代码的全过程。
2.时态逻辑
模态逻辑是经典命题逻辑和一阶谓词逻辑的扩展形式。
Kripke结构：三元组M=（W,R,L）称为模型逻辑的一个模型，或Kripke结构
一阶线性时态逻辑(FOLTL)：是一阶谓词逻辑的扩展。（通过队列及其操作、汉诺塔操作规划问题来介绍FOLTL）。
计算树逻辑（CTL）：是一种离散、分支时间、命题时态逻辑。
3.模型检测
◇标记算法是模型检验的一个简单算法，其基本原理在于：对于给定的CTL*公式Φ，将其写成由A◇,E◇,E○,∧,┒,nil连接的等值CTL*公式φ，对Kripke结构中φ的子式满足的状态进行标记，直到φ得到标记。
4.Z语言
Z语言为系统建立基于状态的模型。
Z语言表示抽象的要素总体分为两类：基于集合理论的集合、关系、函数、序列和包，以及z独有的模式。
Z语言实例：停车场管理系统的例，图书管理系统的例。
5.Petri网
基本定义：Petri网，前集和后集，顺序关系，并发关系，冲突关系，混惑关系。
Petri网规格实例——信号灯。