《软件工程第4章形式化说明技术ppt培训课件》由会员分享，可在线阅读，更多相关《软件工程第4章形式化说明技术ppt培训课件（44页珍藏版）》请在金锄头文库上搜索。
1、1,软 件 工 程,-第4章 形式化说明技术,2,4.1 概述 4.2 有穷状态机 4.3 Petri网 4.4 Z语言 4.5 小结 习题,第4章 形式化说明技术,3,按照形式化的程度，可以把软件工程使用的方法划分成非形式化、半形式化和形式化3类。用自然语言描述需求规格说明，是典型的非形式化方法。用数据流图或实体-联系图建立模型，是典型的半形式化方法。形式化方法，是描述系统性质的基于数学的技术，也就是说，如果一种方法有坚实的数学基础，那么它就是形式化的。,4,4.1 概述,4.1.1 非形式化方法的缺点,用自然语言书写的系统规格说明书，可能存在矛盾、二义性、含糊性、不完整性及抽象层次混乱等问
2、题。所谓矛盾是指一组相互冲突的陈述。二义性是指读者可以用不同方式理解的陈述。,5,系统规格说明书是很庞大的文档，因此，几乎不可避免地会出现含糊性。实际上，这样笼统的陈述并没有给出任何有用的信息。不完整性可能是在系统规格说明中最常遇到的问题之一。抽象层次混乱是指在非常抽象的陈述中混进了一些关于细节的低层次陈述。这样的规格说明书使得读者很难了解系统的整体功能结构。,4.1 概述,6,4.1.2 形式化方法的优点,它能够简洁准确地描述物理现象、对象或动作的结果，因此是理想的建模工具。,可以在不同的软件工程活动之间平滑地过渡。,提供了高层确认的手段。,4.1 概述,7,4.1.3 应用形式化方法的准则
3、,4.1 概述,(1) 应该选用适当的表示方法。 (2) 应该形式化，但不要过分形式化。 (3) 应该估算成本。 (4) 应该有形式化方法顾问随时提供咨询。 (5) 不应该放弃传统的开发方法。,8,(6) 应该建立详尽的文档。 (7) 不应该放弃质量标准。 (8) 不应该盲目依赖形式化方法。 (9) 应该测试、测试再测试。 (10) 应该重用。,4.1 概述,9,4.2 有穷状态机,4.2.1 概念,一个保险箱上装了一个复合锁，锁有三个位置，分别标记为1、2、3，转盘可向左(L)或向右(R)转动。这样，在任意时刻转盘都有6种可能的运动，即1L、1R、2L、2R、3L和3R。保险箱的组合密码是1
4、L、3R、2L，转盘的任何其他运动都将引起报警。图4.1描绘了保险箱的状态转换情况。,10,图4.1 保险箱的状态转换图,4.2 有穷状态机,11,一个有穷状态机包括下述5个部分：状态集J、输入集K、由当前状态和当前输入确定下一个状态(次态)的转换函数T、初始态S和终态集F。对于保险箱的例子，相应的有穷状态机的各部分如下。 状态集J：保险箱锁定，A，B，保险箱解锁，报警。 输入集K：1L，1R，2L，2R，3L，3R。,4.2 有穷状态机,12,转换函数T：如表4.1所示。 初始态S：保险箱锁定。 终态集F：保险箱解锁，报警。,一个有穷状态机可以表示为一个5元组(J，K，T，S，F)，其中：
5、J是一个有穷的非空状态集； K是一个有穷的非空输入集； T是一个从(J-F)K到J的转换函数； SJ，是一个初始状态； FJ，是终态集。,13,为了对一个系统进行规格说明，通常都需要对有穷状态机做一个很有用的扩展，即在前述的5元组中加入第6个组件谓词集P，从而把有穷状态机扩展为一个6元组，其中每个谓词都是系统全局状态Y的函数。转换函数T现在是一个从(J-F)KP到J的函数。现在的转换规则形式如下：当前状态菜单+事件所选择的项+谓词下个状态。,4.2 有穷状态机,14,在一幢m层的大厦中需要一套控制n部电梯的产品，要求这n部电梯按照约束条件C1，C2和C3在楼层间移动。C1：每部电梯内有m个按钮
6、，每个按钮代表一个楼层。当按下一个按钮时该按钮指示灯亮，同时电梯驶向相应的楼层，到达按钮指定的楼层时指示灯熄灭。,4.2 有穷状态机,15,C2：除了大厦的最低层和最高层之外，每层楼都有两个按钮分别请求电梯上行和下行。这两个按钮之一被按下时相应的指示灯亮，当电梯到达此楼层时灯熄灭，电梯向要求的方向移动。 C3：当对电梯没有请求时，它关门并停在当前楼层。,4.2 有穷状态机,16,FBP(d,f)：楼层按钮(d,f)被按下 EAF(1n,f)：电梯1或或n到达f层 其中1n表示或为1或为2或为n。为了定义与这些事件和状态相联系的状态转换规则，同样也需要一个谓词，它是S(d,e,f)，它的定义如下
7、。 S(d,e,f)：电梯e停在f层并且移动方向由d确定为向上(d=U)或向下(d=D)或待定(d=N)。,4.2 有穷状态机,17,电梯按钮的状态转换图如图4.2所示。令EB(e,f)表示按下电梯e内的按钮并请求到f层去。 EBON(e,f)：电梯按钮(e,f)打开 EBOFF(e,f)：电梯按钮(e,f)关闭如果电梯按钮(e,f)发光且电梯到达f层，该按钮将熄灭。相反如果按钮熄灭，则按下它时，按钮将发光： EBP(e,f)：电梯按钮(e,f)被按下 EAF(e,f)：电梯e到达f层,4.2 有穷状态机,18,图4.2 电梯按钮的状态转换图,图4.3楼层按钮的状态转换图,19,V(e,f)：
8、电梯e停在f层EBOFF(e,f)+EBP(e,f)+not V(e,f)EBON(e,f)EBON(e,f)+EAF(e,f)EBOFF(e,f),4.2 有穷状态机,20,接下来考虑楼层按钮。令FB(d,f)表示f层请求电梯向d方向运动的按钮，楼层按钮的状态如下： FBON(d,f)：楼层按钮(d,f)打开 FBOFF(d,f)：楼层按钮(d,f)关闭如果楼层按钮已经打开，而且一部电梯到达f层，则按钮关闭。反之，如果楼层按钮原来是关闭的，被按下后该按钮将打开。这段叙述中包含了以下两个事件。,4.2 有穷状态机,21,使用谓词S(d,e,f)，形式化转换规则为： FBOFF(d,f)+FBP
9、(d,f)+not S(d,1n,f)FBON(d,f) FBON(d,f)+EAF(1n,f)+S(d,1n,f)FBOFF(d,f) 其中，d=UorD。,4.2 有穷状态机,22,图4.4 电梯的状态转换图,23,最后，给出电梯的状态转换规则。为简单起见，这里给出的规则仅发生在关门之时。 S(U,e,f)+DC(e,f)M(U,e,f+1) S(D,e,f)+DC(e,f)M(D,e,f-1) S(N,e,f)+DC(e,f)W(e,f),4.2 有穷状态机,24,评价,25,4.3 Petri网,并发系统中遇到的一个主要问题是定时问题。,用于确定系统中隐含的定时问题的一种有效技术是Pe
10、tri网，这种技术的一个很大的优点是它也可以用于设计中。,26,Petri网是由Carl Adam Petri发明的。用Petri网可以有效地描述并发活动。Petri网包含4种元素：一组位置P、一组转换T、输入函数I以及输出函数O。,4.3 Petri网,27,图4.5 Petri网的组成,4.3 Petri网,I(t1)=P2，P4 I(t2)=P2,O(t1)=P1 O(t2)=P3，P3,28,更形式化的Petri网结构，是一个四元组C=(P,T,I,O)。其中， P=P1，Pn是一个有穷位置集，n0。 T=t1，tm是一个有穷转换集，m0，且T和P不相交。 I：TP为输入函数，是由转换
11、到位置无序单位组(bags)的映射。 O：TP为输出函数，是由转换到位置无序单位组的映射。,4.3 Petri网,29,图4.6 带标记的Petri网,Petri网的标记是在Petri网中权标(token)的分配。,当每个输入位置所拥有的权标数大于等于从该位置到转换的线数时，就允许转换。,4.3 Petri网,30,图4.7 图4.6的Petri网在转换t1被激发后的情况,4.3 Petri网,31,图4.8 图4.7的Petri网在转换t2被激发后的情况,4.3 Petri网,32,4.3 Petri网,图4.9 含禁止线的Petri网,33,例子,现在把Petri网应用于上一节讨论过的电梯
12、问题。当用Petri网表示电梯系统的规格说明时，每个楼层用一个位置Ff代表(1fm)，在Petri网中电梯是用一个权标代表的。在位置Ff上有权标，表示在楼层f上有电梯。 1. 电梯按钮在Petri网中用位置EBf表示(1fm)。在EBf上有一个权标，就表示电梯内楼层f的按钮被按下了。,34,图4.10 Petri网表示的电梯按钮,例子,35,2. 楼层按钮在第二个约束条件中描述了楼层按钮的行为。在Petri网中楼层按钮用位置FBuf和FBdf表示，分别代表f楼层请求电梯上行和下行的按钮。底层的按钮为FBu1，最高层的按钮为FBdm，中间每一层有两个按钮FBuf和FBdf (1fm)。,例子,3
13、6,图4.11 Petri网表示楼层按钮,例子,37,4.4 Z语言,用Z语言描述的、最简单的形式化规格说明含有下述4个部分：给定的集合、数据类型及常数。状态定义。初始状态。操作。,38,1. 给定的集合 一个Z规格说明从一系列给定的初始化集合开始。所谓初始化集合就是不需要详细定义的集合，这种集合用带方括号的形式表示。对于电梯问题，给定的初始化集合称为Button，即所有按钮的集合，因此，Z规格说明开始于： Button 2. 状态定义 一个Z规格说明由若干个“格(schema)”组成，每个格含有一组变量说明和一系列限定变量取值范围的谓词。例如，格S的格式如图4.12所示。,39,图4.12
14、Z格S的格式,40,在电梯问题中，Button有4个子集，即floor_buttons(楼层按钮的集合)、elevator_buttons(电梯按钮的集合)、buttons(电梯问题中所有按钮的集合)以及pushed(所有被按的按钮的集合，即所有处于打开状态的按钮的集合)。约束条件声明，floor_buttons集与elevator_buttons集不相交，而且它们共同组成buttons集,41,3. 初始状态抽象的初始状态是指系统第一次开启时的状态。 Button_InitButton_Statepushed=上式表示，当系统首次开启时pushed集为空，即所有按钮都处于关闭状态。 4. 操
15、作如果一个原来处于关闭状态的按钮被按下，则该按钮开启，这个按钮就被添加到pushed集中。,42,Z语言之所以会获得如此多的成功，主要有以下几个原因： (1) 可以比较容易地发现用Z写的规格说明的错误，特别是在自己审查规格说明，及根据形式化的规格说明来审查设计与代码时，情况更是如此。 (2) 用Z写规格说明时，要求作者十分精确地使用Z说明符。由于对精确性的要求很高，从而和非形式化规格说明相比，减少了模糊性、不一致性和遗漏。,43,(3) Z是一种形式化语言，在需要时开发者可以严格地验证规格说明的正确性。 (4) 虽然完全学会Z语言相当困难，但是，经验表明，只学过中学数学的软件开发人员仍然可以只用比较短的时间就学会编写Z规格说明，当然，这些人还没有能力证明规格说明的结果是否正确。 (5) 使用Z语言可以降低软件开发费用。虽然用Z写规格说明所需用的时间比使用非形式化技术要多，但开发过程所需要的总时间却减少了。,44,(6) 虽然用户无法理解用Z写的规格说明，但是，可以依据Z规格说明用自然语言重写规格说明。经验证明，这样得到的自然语言规格说明，比直接用自然语言写出的非形式化规格说明更清楚、更正确。使用形式化规格说明是全球的总趋势，过去，主要是欧洲习惯于使用形式化规格说明技术，现在越来越多的美国公司也开始使用形式化规格说明技术。,
