标签：
形式化方法指的是将离散数学的方法用于解决软件工程领域的问题，主要是建立精确的数学模型以及对模型的分析活动。在软件开发过程中运用数学模型有很多优点，例如能够解决规格说明的二义性，提高精确性，还能使软件相关问题的本质可以在不同抽象层次被展示出来。本章介绍形式化方法主要从形式化方法基本概念、时态逻辑、模型检验、Z语言、Petri网几个方面讲述。
形式化方法基本概念主要讲了形式规范、形式证明与验证、程序求精，形式规范说明是对软件系统对象，对象的操作方法，以及对象行为的描述。形式证明与验证主要包括模型检测和定理证明。程序求精是自动推理和形式化方法相结合，从抽象的形式规约推演出具体的面向计算机的程序代码的全过程。
时态逻辑中讲到了Kripke结构，及一阶线性时态逻辑、计算树逻辑。一阶线性时态逻辑是一阶谓词逻辑的扩展，FOLTL公式在队列及其操作、汉诺塔操作规划问题中有广泛的应用。计算树逻辑是一种离散、分支时间、命题时态逻辑。CTL公式在好多的算法中也是有着很重要的应用。
模型检测是在软件系统的Kripke结构模型下，对以CTE*公式给出的软件性质的正确性验证。
Z语言是一种形式语言，它的数学基础是集合论和一阶谓词演算。在软件工程界得到最为普遍的继承和广泛的应用。本节介绍了z语言的概述、z语言表示、z语言实例。概述Z语言为系统建立基于状态的模型，模型的三个主要组成部分是输入、输出和状态。Z语言表示抽象的要素总体可分为两类:基于集合理论的集合、关系、函数、序列和包，以及Z独有的模式:自由类型和模式。Z语言实例中以停车场管理系统和图书管理系统为例讲了Z语言的应用。
Petri网主要讲了基本定义和它的规格实例信号灯，Petri网是一种系统模型，变迁和库的依赖关系的流关系表示。它是一个三元组，它有丰富的结构描述能力，有顺序、并发、冲突、混惑等关系。信号灯的实例充分说明了Petri网的应用。
标签：
原文地址：http://www.cnblogs.com/lingxi/p/4295703.html
