第4章形式化说明技术.PPT
2019/4/6,1,第4章 形式化说明技术,4.1 概述 4.2 有穷状态机 4.3 Petri网 4.4 Z语言,2,2019/4/6,形式化方法,按照形式化的程度划分软件工程使用的方法: 非形式化 半形式化 形式化 形式化方法定义: 是描述系统性质的、基于数学的技术。,3,2019/4/6,形式化方法与欠形式化方法比较,4,2019/4/6,应用形式化方法的准则,应该选用适当的表示方法 应该形式化,但不要过分形式化 应该估算成本 应该有形式化方法顾问随时提供咨询 不应该放弃传统的开发方法 应该建立详尽的文档 不应该放弃质量标准 不应该盲目依赖形式化方法 应该测试、测试再测试 应该重用,5,2019/4/6,有穷状态机(Finite State Machine),例:一个保险箱上装了一个复合锁,锁有三个位置,分别标记为1、2、3,转盘可向左(L)或向右(R)转动。这样,在任意时刻转盘都有6种可能的运动,即1L、1R、2L、2R、3L和3R。保险箱的组合密码是1L、3R、2L,转盘的任何其他运动都将引起报警。,保险箱的状态转换图,6,2019/4/6,有穷状态机的组成包括5个部分:状态集J、输入集K、由当前状态和当前输入确定下一个状态(次态)的转换函数T、初始态S和终态集F。 保险箱的有穷状态机的各部分如下: 状态集J:保险箱锁定,A,B,保险箱解锁,报警。 输入集K:1L,1R,2L,2R,3L,3R。 转换函数T:见书P68表4.1所示。 初始态S:保险箱锁定。 终态集F:保险箱解锁,报警。,7,2019/4/6,使用更形式化的术语,一个有穷状态机可以表示为一个5元组(J,K,T,S,F),其中: J是一个有穷的非空状态集; K是一个有穷的非空输入集; T是一个从(J-F)×K到J的转换函数; SJ,是一个初始状态; FJ,是终态集。,8,2019/4/6,Petri网,Petri网简称PNG (Petri Net Graph) Petri网已广泛地应用于硬件与软件系统的开发中,它适用于描述与分析相互独立、协同操作的处理系统,也就是并发执行的处理系统。,Petri网包含4种元素: 一组位置P (圆圈) :表示系统的状态 一组转换T (短直线) :表示系统中的事件 输入函数I (有向边) :表示对转换的输入 输出函数O (有向边) :表示由转换的输出,9,2019/4/6,Petri网的组成示例:,10,2019/4/6,一组位置P为P1,P2,P3,P4 一组转换T为t1,t2 两个用于转换的输入函数: I(t1)=P2,P4 I(t2)=P2 两个用于转换的输出函数: O(t1)=P1 O(t2)=P3,P3,11,2019/4/6,更形式化的Petri网结构,是一个四元组C=(P,T,I,O)。 其中, P=P1,Pn是一个有穷位置集,n0。 T=t1,tm是一个有穷转换集,m0,且T和P不相交。 I:TP为输入函数,是由转换到位置无序单位组的映射。 O:TP为输出函数,是由转换到位置无序单位组的映射。 一个无序单位组或多重组是允许一个元素有多个实例的广义集。,12,2019/4/6,带标记的Petri网:Petri网的标记是在Petri网中权标(token)的分配。,权标:或叫令牌(token),例:,2019/4/6,13,转换 t2被激发后的情况:,转换 t1被激发后的情况:,14,2019/4/6,例:处理两个进程的同步问题,15,2019/4/6,16,2019/4/6,例:,含禁止线的Petri网:当每个输入线上至少有一个权标,而禁止线上没有权标的时候,相应的转换才是允许的。,转换t1可以被激发,17,2019/4/6,Z语言,用Z语言描述的、最简单的形式化规格说明含有4个部分: 给定的集合、数据类型及常数 状态定义 初始状态 操作,18,2019/4/6,1. 给定的集合 一个Z规格说明从一系列给定的初始化集合(不需要详细定义的集合)开始。 这种集合用带方括号的形式表示。 例:对于电梯问题,给定的初始化集合称为Button,即所有按钮的集合: Button,19,2019/4/6,2. 状态定义 一个Z规格说明由若干个“格(schema)”组成,每个格含有一组变量说明和一系列限定变量取值范围的谓词。,例:,20,2019/4/6,3. 初始状态 指系统第一次开启时的状态。 例:对于电梯问题来说: Button_InitButton_Statepushed= 上式表示,当系统首次开启时pushed集为空,即所有按钮都处于关闭状态。,21,2019/4/6,4. 操作 例:如果一个原来处于关闭状态的按钮被按下,则该按钮开启,这个按钮就被添加到pushed集中。,22,2019/4/6,例:假设电梯到达了某楼层,如果相应的楼层按钮已经打开,则此时它会关闭;同样,如果相应的电梯按钮已经打开,则此时它也会关闭。,注:符号“”表示集合差运算,