《软件工程概论》第五章 软件工程中的形式化方法

形式化方法的基本概念：

1. 形式规约
2. 形式证明与验证
3. 程序求精

一阶线性时态逻辑：

1. 队列及其操作
2. 汉诺塔操作规划问题

计算树逻辑

模型检测

Z语言概述：

Z语言为系统建立基于状态的模型。模型的三个主要组成部分是输入、输出和状态，它们均有相应的数学概念来描述。

Z语言表示：

1. 集合、关系及函数
2. 自由类型和模式

Petri网定义：

任何事物都可抽象为两类元素：状态和事件。在某种状态下，相应的事件便可发生。然后状态发生变化，于是又有一些新的事件可以发生。如此反复不已。

（1）       Petri网结构

（2）       前集合后集

（3）       顺序关系

（4）       并发关系

（5）       冲突关系

（6）       混惑关系