软件工程概论
第五章 软件工程中的形式化方法
1.形式化方法基本概念
形式约束:软件规格说明是软件系统对象,对象的操作方法,以及对象行为的描述。在系统的开发及演化过程中,对象,对象的性质以及操作应作为一个整体来处理。
形式证明与验证:主要包括模型检验和定理证明。
程序求精:是将自动推理和形式化方法相结合,从抽象的形式规约推演出具体的面向计算机的程序代码的全过程。
2.时态逻辑
模态逻辑是经典命题逻辑和一阶谓词逻辑的扩展形式。
Kripke结构:三元组M=(W,R,L)称为模型逻辑的一个模型,或Kripke结构
一阶线性时态逻辑(FOLTL):是一阶谓词逻辑的扩展。(通过队列及其操作、汉诺塔操作规划问题来介绍FOLTL)。
计算树逻辑(CTL):是一种离散、分支时间、命题时态逻辑。
3.模型检测
◇标记算法是模型检验的一个简单算法,其基本原理在于:对于给定的CTL*公式Φ,将其写成由A◇,E◇,E○,∧,┒,nil连接的等值CTL*公式φ,对Kripke结构中φ的子式满足的状态进行标记,直到φ得到标记。
4.Z语言
Z语言为系统建立基于状态的模型。
Z语言表示抽象的要素总体分为两类:基于集合理论的集合、关系、函数、序列和包,以及z独有的模式。
Z语言实例:停车场管理系统的例,图书管理系统的例。
5.Petri网
基本定义:Petri网,前集和后集,顺序关系,并发关系,冲突关系,混惑关系。
Petri网规格实例——信号灯。
时间: 2024-10-07 05:06:29