形式化规格技术：
1、定义： 对系统或者对象及其期望的特性或者行为进行的描述。规格所要描述的内容包括：功能特性（做什么）、行为特性（具体行为演化-如何做）、结构特性（系统的组成，子系统间的联系和复合）、时间特性（时间相关的系统特性）。形式化规格就是通过具有明确数学定义的文法和语义的语言实现以上描述。
2、分类：操作类、描述类、双重类。
2.1 操作类技术基于状态和迁移，因其本质上可执行，有直观和可视的特点；
2.2 描述类技术基于数学公理和概念，通过逻辑和代数给出系统的状态空间，具有高度抽象、便于通过自动工具进行验证的特点；
2.3 双重类技术兼有二者的特点，能够通过数学公理和概念高度抽象描述系统，又有状态和迁移的可执行特征。
3、操作类规格技术：
通过可执行模型描述系统，即模型本身能够采用静态分析和执行模型得到验证。
该技术侧重于系统行为的特性描述，主要包括：有限状态机和Petri网技术。
有限状态机——状态迁移图和状态迁移矩阵两种表示方式。就是一个具有有限状态的机器。
Petri网——描述能力强于FSM，可描述并发、同步、冲突等特性。
4、描述类规格技术：
以代数or逻辑为基础，具有数学上的严密性和高度抽象性，并通过做什么的方式进行系统性能规格。
4.1 基于代数的以抽象数据类型ADT概念为基础，可以对系统进行由粗到细的多层次抽象。此类方法中，系统本身视为一个ADT，规格则在于描述其文法和语义。文法定义给出ADT中算子域的描述。语义通过数学表达式给出算子的执行，这些数学表达式的形式为用编程语言书写的一组公理。复杂的ADT由简单的ADT定义，重复进行则完成整个系统的规格，这样就给后期的验证带来方便。验证可以在各个层次的规格上进行，复杂的ADT的特性可通过简单的ADT特性的验证而得到验证。Z语言 LOTOS VDM Larch
Z语言在面向对象方面进行扩展：OOZE MooZ Z++ Object-Z（集成了时态逻辑）
LOTOS language of temporal ordering specifications
4.2 基于逻辑的描述技术通过逻辑规则来规格系统的演化，与操作类技术不同的是规格所描述的系统状态空间是抽象和无限的。规则一般是一阶Horn子句或者高阶逻辑公式。时态算子。
基于时态逻辑的描述规格技术主要有计算树逻辑 CTL RTIL TCTL TPTL
原文地址：http://www.cnblogs.com/andongdong/p/4012236.html
