1 形式化方法的基本概念
形式化规约
形式证明与验证
程序求精
2 时态逻辑
krioke结构可以表示为一个有向图
一阶线性时态逻辑是一阶谓词逻辑的扩展。
队列及其操作：队列是一种常用的数据抽象类型他服从先进先出的FIFO规则。在某一时刻队列可以为空。
1 活性 2 安全性
汉诺塔操作规划问题
计算树逻辑是一种离散，分支时间命题时态逻辑
3 z语言
概述：Z语言为系统建立基于状态的模型，模型的三个重要组成部分为输入，输出和状态。
z语言的表示 ：1集合关系及函数2自由类型和模型
4 petri网
基本定义：任何系统都可分化为两种元素：状态和事件。主要分为：顺序关系，并发关系，冲突关系，混惑关系