《形式化说明技术》由会员分享，可在线阅读，更多相关《形式化说明技术（22页珍藏版）》请在金锄头文库上搜索。
1、tjm第第4章章 形式化说明技术形式化说明技术4.1 概述概述4.2 有穷状态机有穷状态机4.3 Petri网网4.4 Z语言语言8/27/20241tjm形式化方法形式化方法w按照形式化的程度划分软件工程使用的方法：按照形式化的程度划分软件工程使用的方法：n非形式化非形式化n半形式化半形式化n形式化形式化w形式化方法定义：形式化方法定义： 是描述系统性质的、基于数学的技术。是描述系统性质的、基于数学的技术。8/27/20242tjm形式化方法与欠形式化方法比较形式化方法与欠形式化方法比较优点优点缺点缺点形式形式化方化方法法形式化的规格说明可以用数学方形式化的规格说明可以用数学方法研究、验证。
2、法研究、验证。消除了二义性，鼓励在软件工程消除了二义性，鼓励在软件工程过程的早期阶段使用更严格的方过程的早期阶段使用更严格的方法，从而可以减少差错。法，从而可以减少差错。主要关注于系统的主要关注于系统的功能和数据，而问功能和数据，而问题的时序、控制和题的时序、控制和行为等方面的需求行为等方面的需求却更难于表示。却更难于表示。复杂难学习。复杂难学习。欠形欠形式化式化方法方法简单易学。简单易学。可能存在矛盾、二可能存在矛盾、二义性、含糊性、不义性、含糊性、不完整性及等问题。完整性及等问题。8/27/20243tjm应用形式化方法的准则应用形式化方法的准则w应该选用适当的表示方法应该选用适当的表示方
3、法w应该形式化，但不要过分形式化应该形式化，但不要过分形式化w应该估算成本应该估算成本w应该有形式化方法顾问随时提供咨询应该有形式化方法顾问随时提供咨询w不应该放弃传统的开发方法不应该放弃传统的开发方法w应该建立详尽的文档应该建立详尽的文档w不应该放弃质量标准不应该放弃质量标准w不应该盲目依赖形式化方法不应该盲目依赖形式化方法w应该测试、测试再测试应该测试、测试再测试w应该重用应该重用8/27/20244tjm有穷状态机（有穷状态机（Finite State Machine） 例：一个保险箱上装了一个复合锁，锁有三个位置，分别标记例：一个保险箱上装了一个复合锁，锁有三个位置，分别标记为为1、2
4、、3，转盘可向左，转盘可向左(L)或向右或向右(R)转动。这样，在任意转动。这样，在任意时刻转盘都有时刻转盘都有6种可能的运动，即种可能的运动，即1L、1R、2L、2R、3L和和3R。保险箱的组合密码是。保险箱的组合密码是1L、3R、2L，转盘的任何其，转盘的任何其他运动都将引起报警。他运动都将引起报警。保险箱的状态转换图保险箱的状态转换图8/27/20245tjm 有穷状态机的组成包括有穷状态机的组成包括5个部分：状态集个部分：状态集J、输入集、输入集K、由当前状态和当前输入确定下一个状态、由当前状态和当前输入确定下一个状态(次态次态)的转换函数的转换函数T、初始态、初始态S和终态集和终态集
5、F。保险箱的有穷状态机的各部分如下：保险箱的有穷状态机的各部分如下：状态集状态集J：保险箱锁定，：保险箱锁定，A，B，保险箱解锁，报，保险箱解锁，报警。警。输入集输入集K：1L，1R，2L，2R，3L，3R。转换函数转换函数T：见书：见书P68表表4.1所示。所示。初始态初始态S：保险箱锁定。：保险箱锁定。终态集终态集F：保险箱解锁，报警。：保险箱解锁，报警。8/27/20246tjm使用更形式化的术语，一个有穷状态机可以表示使用更形式化的术语，一个有穷状态机可以表示为一个为一个5元组元组(J，K，T，S，F)，其中：，其中：J是一个有穷的非空状态集；是一个有穷的非空状态集；K是一个有穷的非空
6、输入集；是一个有穷的非空输入集；T是一个从是一个从(J-F)K到到J的转换函数；的转换函数；SJ，是一个初始状态；，是一个初始状态；FJ，是终态集。，是终态集。8/27/20247tjmPetri网网 Petri网简称网简称PNG (Petri Net Graph) Petri网已广泛地应用于硬件与软件系统的开发中，网已广泛地应用于硬件与软件系统的开发中，它适用于描述与分析相互独立、协同操作的处理它适用于描述与分析相互独立、协同操作的处理系统，也就是并发执行的处理系统。系统，也就是并发执行的处理系统。 Petri网包含网包含4种元素：种元素：n一组位置一组位置P （圆圈）（圆圈） ：表示系统的
7、状态：表示系统的状态n一组转换一组转换T （短直线）（短直线） ：表示系统中的事件：表示系统中的事件n输入函数输入函数I （有向边）（有向边） ：表示对转换的输入：表示对转换的输入n输出函数输出函数O （有向边）（有向边） ：表示由转换的输出：表示由转换的输出8/27/20248tjmPetri网的组成示例：网的组成示例：8/27/20249tjm一组位置一组位置P为为P1，P2，P3，P4一组转换一组转换T为为t1，t2两个用于转换的输入函数：两个用于转换的输入函数：I(t1)=P2，P4I(t2)=P2两个用于转换的输出函数：两个用于转换的输出函数：O(t1)=P1O(t2)=P3，P38
8、/27/202410tjm更形式化的更形式化的Petri网结构，是一个四元组网结构，是一个四元组C=(P,T,I,O)。其中，其中，P=P1，Pn是一个有穷位置集，是一个有穷位置集，n0。T=t1，tm是一个有穷转换集，是一个有穷转换集，m0，且，且T和和P不相交。不相交。I：TP为输入函数，是由转换到位置无序单位为输入函数，是由转换到位置无序单位组的映射。组的映射。O：TP为输出函数，是由转换到位置无序单位为输出函数，是由转换到位置无序单位组的映射。组的映射。一个无序单位组或多重组是允许一个元素有多个实一个无序单位组或多重组是允许一个元素有多个实例的广义集。例的广义集。8/27/202411
9、tjm带标记的带标记的Petri网：网：Petri网的标记是在网的标记是在Petri网中权网中权标标(token)的分配。的分配。权标：或叫令牌权标：或叫令牌(token)w例：例：8/27/202412tjm转换转换 t2被激发后的情况：被激发后的情况：转换转换 t1被激发后的情况：被激发后的情况：8/27/202413tjm例：处理两个进程的同步问题例：处理两个进程的同步问题8/27/202414tjm8/27/202415tjmw例：例：含禁止线的含禁止线的Petri网：当每个输入线上至少有一个网：当每个输入线上至少有一个权标，而禁止线上没有权标的时候，相应的转换权标，而禁止线上没有权标
10、的时候，相应的转换才是允许的。才是允许的。转换转换t1可以被激发可以被激发8/27/202416tjmZ语言语言 用用Z语言描述的、最简单的形式化规格说明含有语言描述的、最简单的形式化规格说明含有4个部分：个部分：n给定的集合、数据类型及常数给定的集合、数据类型及常数n状态定义状态定义n初始状态初始状态n操作操作8/27/202417tjm 1. 给定的集合给定的集合 一个一个Z规格说明从一系列给定的初始化集合（不需规格说明从一系列给定的初始化集合（不需要详细定义的集合）开始。要详细定义的集合）开始。 这种集合用带方括号的形式表示。这种集合用带方括号的形式表示。 例：对于电梯问题，给定的初始化
11、集合称为例：对于电梯问题，给定的初始化集合称为Button，即所有按钮的集合：，即所有按钮的集合： Button 8/27/202418tjm 2. 状态定义状态定义 一个一个Z规格说明由若干个规格说明由若干个“格格(schema)”组成，组成，每个格含有一组变量说明和一系列限定变量取值每个格含有一组变量说明和一系列限定变量取值范围的谓词。范围的谓词。 例：例：8/27/202419tjm3. 初始状态初始状态指系统第一次开启时的状态。指系统第一次开启时的状态。例：对于电梯问题来说：例：对于电梯问题来说：Button_InitButton_Statepushed=上式表示，当系统首次开启时上式
12、表示，当系统首次开启时pushed集为空，即集为空，即所有按钮都处于关闭状态。所有按钮都处于关闭状态。8/27/202420tjm4. 操作操作例：如果一个原来处于关闭状态的按钮被按下，则例：如果一个原来处于关闭状态的按钮被按下，则该按钮开启，这个按钮就被添加到该按钮开启，这个按钮就被添加到pushed集中。集中。8/27/202421tjm例：假设电梯到达了某楼层，如果相应的楼层按钮例：假设电梯到达了某楼层，如果相应的楼层按钮已经打开，则此时它会关闭；同样，如果相应的电已经打开，则此时它会关闭；同样，如果相应的电梯按钮已经打开，则此时它也会关闭。梯按钮已经打开，则此时它也会关闭。注：符号注：符号“”表示集合差运算表示集合差运算8/27/202422
