码迷,mamicode.com
首页 > 其他好文 > 详细

软件工程概论-5软件工程中的形式化方法

时间:2015-02-10 20:15:28      阅读:158      评论:0      收藏:0      [点我收藏+]

标签:

      在软件工程实践中运用形式化方法可以保证软件的正确性。目前,从形式规约到目标软件系统的可实现和可执行角度,已建立的形式化方法分为操作类和描述类。操作类方法基于状态和转移,通过可执行模型来描述系统,而描述类方法基于数学公理和概念,通过逻辑或代数给出系统的状态空间,具有高度抽象的特点。形式证明与验证技术主要包括模型检测和定理证明。程序求精是将自动推理和形式化方法相结合,从抽象的形式规约推演出具体的面向计算机的程序代码的全过程。下面介绍较为广泛的几种形式方法:

      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网模型有顺序关系,并发关系,冲突关系和混惑关系。

软件工程概论-5软件工程中的形式化方法

标签:

原文地址:http://www.cnblogs.com/houtaoliang/p/4284750.html

(0)
(0)
   
举报
评论 一句话评论(0
登录后才能评论!
© 2014 mamicode.com 版权所有  联系我们:gaon5@hotmail.com
迷上了代码!