软件的设计过程就是一个建立形式规约的过程。软件开发实际上就是把现实世界的需求映射成软件的模型化方法。软件规格说明是对软件系统对象，对象的操作方法，以及对象行为的描述。形式证明与验证技术主要包括模型检测和定理证明。程序求精是将自动推理和形式化方法相结合，从抽象的形式规约推演出具体的面向计算机的程序代码的全过程。模态(Modal)逻辑是经典命题逻辑和一阶谓词逻辑的扩展形式。Kripke结构。1.一阶线性时态逻辑(FOLTL)是一阶谓词逻辑的扩展。2.计算树逻辑(CTL)是一种离散、分支时间、命题时态逻辑。模型检验就是在软件系统的Kripke结构模型下，对以CTL*公式给出的软件性质的正确性验证。标记算法是模型检验的一个简单算法。Z语言为系统建立基于状态的模型。Z语言表示抽象的要素总体上可分为两类：基于集合理论的集合、关系、函数、序列和包，以及Z独有的模式。Petri网一词既指这种模型，又指以这种模型为基础发展起来的理论。有时又把Petri网称为网论。Petri网分为位置/迁移petri网和高级Petri网两类。任何系统都可抽象为两类元素：状态和事件。在Petri网中，状态用库所表示，时间用变迁表示。变迁是Petri网中的主动元素。