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