标签：
在软件工程实践中运用形式化方法可以保证软件的正确性。目前，从形式规约到目标软件系统的可实现和可执行角度，已建立的形式化方法分为操作类和描述类。操作类方法基于状态和转移，通过可执行模型来描述系统，而描述类方法基于数学公理和概念，通过逻辑或代数给出系统的状态空间，具有高度抽象的特点。形式证明与验证技术主要包括模型检测和定理证明。程序求精是将自动推理和形式化方法相结合，从抽象的形式规约推演出具体的面向计算机的程序代码的全过程。下面介绍较为广泛的几种形式方法:
1.时态逻辑
Kripke结构 三元组M=(W,R,L)是模态逻辑的一个模型，它可以表示为一个有向图，在某种意义上，Kripke结构就是一个有限状态机。
一阶线性时态逻辑(FOLTL)是一阶谓词逻辑的扩展，具体应用有队列及其操作和汉诺塔操作规划问题。
计算树逻辑(CTL)是一种离散，分支时间，命题时态逻辑，后来经过对CTL文法中路径量词及其他时态算子的组合使用进行扩展，建立了CTL*，一般将CTL和CTL*统称为计算树逻辑。
2.模型检测
软件的计算树逻辑规格可以通过模型检验得到验证。模型检验就是在软件系统的Kripke结构模型下，对以CTL*公式给出的软件性质的正确性验证。
3.Z语言
Z语言为系统建立基于状态的模型。模型的三个主要组成部分是输入，输出和状态，它们均有相应的数学概念来描述，Z语言形式规约由数学语言描述和自然语言注释两部分组成。Z语言表示抽象的要素总体上可分为两类，基于集合理论的集合。关系，函数，序列和包，以及Z独有的模式，这些要素构成了Z语言的类型模型。
4.Petri网
任何系统都可抽象为两类元素:状态和事件。在某种状态下，相应的事件便可以发生。然后状态发生变化，于是又有一些新的事件发生，如此反复不已。在Petri网中，状态用库所Place表示，事件用变迁Transition表示，变迁的作用是改变状态，库所的作用是决定变迁是否能够发生，变迁和库所之间的这种依赖关系用流关系来表示。Petri网模型有顺序关系，并发关系，冲突关系和混惑关系。
标签：
原文地址：http://www.cnblogs.com/houtaoliang/p/4284750.html
