规格说明技术 USTC 。 描述系统对象，对象的操作方法，以及对象的行为 -非形式化方法，称“规格说明” 一形式化方法，称“形式规约” 形式规约(Formal Specification) -描述类 ·基于数学公理和概念，通过逻辑或代数，给出系统的状态空 间，采用自动工具进行验证。 -基于代数的方法：Z、VDM、Larch -基于逻辑：一阶线性时态逻辑(FOLTL)、计算树逻辑(CTL) 一操作类：操作语义 ·基于状态和迁移，通过可执行模型描述系统，采用静态分析 和模型执行进行验证。 -基于模型：图示化，直观 一基于语言：程序，一种可执行的形式规约 llxx@ustc.edu.cn 7/112规格说明技术 • 描述系统对象，对象的操作方法，以及对象的行为 – 非形式化方法，称“规格说明” – 形式化方法，称“形式规约” • 形式规约（Formal Specification） – 描述类 • 基于数学公理和概念，通过逻辑或代数，给出系统的状态空 llxx@ustc.edu.cn 7/112 • 基于数学公理和概念，通过逻辑或代数，给出系统的状态空 间，采用自动工具进行验证。 – 基于代数的方法：Z、VDM、Larch – 基于逻辑：一阶线性时态逻辑(FOLTL)、计算树逻辑(CTL) – 操作类：操作语义 • 基于状态和迁移，通过可执行模型描述系统，采用静态分析 和模型执行进行验证。 – 基于模型：图示化，直观 – 基于语言：程序，一种可执行的形式规约