形式化说明技术.PPTVIP

tjmtjmtjmtjm**第4章形式化说明技术4.1概述4.2有穷状态机4.3Petri网4.4Z语言**形式化方法按照形式化的程度划分软件工程使用的方法：非形式化半形式化形式化形式化方法定义：是描述系统性质的、基于数学的技术。形式化方法与欠形式化方法比较**优点缺点形式化方法形式化的规格说明可以用数学方法研究、验证。消除了二义性，鼓励在软件工程过程的早期阶段使用更严格的方法，从而可以减少差错。主要关注于系统的功能和数据，而问题的时序、控制和行为等方面的需求却更难于表示。复杂难学习。欠形式化方法简单易学。可能存在矛盾、二义性、含糊性、不完整性及等问题。应用形式化方法的准则**应该选用适当的表示方法01应该形式化，但不要过分形式化02应该估算成本03应该有形式化方法顾问随时提供咨询04不应该放弃传统的开发方法05应该建立详尽的文档06不应该放弃质量标准07不应该盲目依赖形式化方法08应该测试、测试再测试09应该重用10有穷状态机（FiniteStateMachine）例：一个保险箱上装了一个复合锁，锁有三个位置，分别标记为1、2、3，转盘可向左(L)或向右(R)转动。这样，在任意时刻转盘都有6种可能的运动，即1L、1R、2L、2R、3L和3R。保险箱的组合密码是1L、3R、2L，转盘的任何其他运动都将引起报警。保险箱的状态转换图有穷状态机的组成包括5个部分：状态集J、输入集K、由当前状态和当前输入确定下一个状态(次态)的转换函数T、初始态S和终态集F。保险箱的有穷状态机的各部分如下：状态集J：｛保险箱锁定，A，B，保险箱解锁，报警｝。输入集K：｛1L，1R，2L，2R，3L，3R｝。转换函数T：见书P68表4.1所示。初始态S：保险箱锁定。终态集F：｛保险箱解锁，报警｝。使用更形式化的术语，一个有穷状态机可以表示为一个5元组(J，K，T，S，F)，其中：J是一个有穷的非空状态集；K是一个有穷的非空输入集；T是一个从(J-F)×K到J的转换函数；S∈J，是一个初始状态；FJ，是终态集。Petri网**Petri网简称PNG(PetriNetGraph)Petri网已广泛地应用于硬件与软件系统的开发中，它适用于描述与分析相互独立、协同操作的处理系统，也就是并发执行的处理系统。Petri网包含4种元素：一组位置P（圆圈）：表示系统的状态一组转换T（短直线）：表示系统中的事件输入函数I（有向边）：表示对转换的输入输出函数O（有向边）：表示由转换的输出Petri网的组成示例：**01一组转换T为｛t1，t2｝一组位置P为｛P1，P2，P3，P402I(t1)=｛P2，P4｝I(t2)=｛P2｝两个用于转换的输入函数：03O(t1)=｛P1｝O(t2)=｛P3，P3｝两个用于转换的输出函数：**更形式化的Petri网结构，是一个四元组C=(P,T,I,O)。其中，P=｛P1，…，Pn｝是一个有穷位置集，n≥0。T=｛t1，…，tm｝是一个有穷转换集，m≥0，且T和P不相交。I：T→P∞为输入函数，是由转换到位置无序单位组的映射。O：T→P∞为输出函数，是由转换到位置无序单位组的映射。一个无序单位组或多重组是允许一个元素有多个实例的广义集。带标记的Petri网：Petri网的标记是在Petri网中权标(token)的分配。例：权标：或叫令牌(token)转换t2被激发后的情况：转换t1被激发后的情况：例：处理两个进程的同步问题 **转换t1可以被激发例：含禁止线的Petri网：当每个输入线上至少有一个权标，而禁止线上没有权标的时候，相应的转换才是允许的。tjmtjmtjmtjm**