1.形式化方法
(1)广义上：将离散数学的方法用于解决软件工程领域的问题。
包括:建立精确的数学模型、对模型的分析活动。
狭义上：进行形式化的规格说明、模型推理、验证。
(2)作用：解决规格说明的二义性、提高精确性、提高确认手段。
(3)根本上，软件的设计过程就是一个建立形式规约的过程。
程序---可看做一种可执行的形式规约。
(4)模型化设计的三种系统模型.
1.现实世界2.模型表示3.计算机系统
开发任务：（1）模型获取、（2）模型验证、（3）模型变换
对应活动：形式规约、形式证明与验证、程序求精。
（1）1--》转化为—》2（2）检验建立的模型（3）2—》转化为—》3
2.基本概念
(1)形式规约：即软件规格说明，是软件系统对象，对象的操作方法，以及对象行为的描述。
(2)形式验证与证明：技术包括：模型检测，定理证明。
1.模型检测：一种基于有限状态模型并检验该模型的性质的技术。（适用与有穷状态 系统）。
2．定理证明：采用逻辑公式来表示系统规约及其性质。（可处理无限状态空间问题）
(3)程序求精：将自动的推理与形式化方法结合，从抽象的形式规约推演出具体的面向计算机的程序代码的全过程。
3.三种形式化方法：
（1）时态逻辑：通过引入“可能”、“必然”两个模态词，对可能世界中的命题进行描述和演算。包括：一阶线性时态逻辑、计算树逻辑。
模型检测就是在Kripke结构模型下，对以CTL*公式给出的软件性质的正确性验证。
（2）Z语言：形式规约文档、抽象要素。
（3）Petri网：任何系统都可抽象为两类元素：状态、事件。行为是变迁。流关系。
注意：一个没有任何输入库所的变迁称为源变迁，一个源变迁的就绪是无条件的。
结构：顺序、并发、冲突、混惑。