软件工程第4章(不讲)

《软件工程第4章(不讲)》由会员分享，可在线阅读，更多相关《软件工程第4章(不讲)（40页珍藏版）》请在装配图网上搜索。

1、单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,*,*,*,第,4,章 形式化说明技术,4.1,概述,4.2,有穷状态机,4.3 Petri,网,4.4 Z,语言,4.5,小结,1,形式化方法,是描述系统性质的基于,数学,的技术，有坚实的数学基础。,按照形式化的程度，划分成非形式化、半形式化和形式化,3,类。,用自然语言描述需求规格说明，是典型的非形式化方法。,用数据流图或实体,-,联系图建立模型，是典型的半形式化方法。,2,4.1.1,非形式化方法的缺点,自然语言书写的规格说明书，可能存在,矛盾,二义性,含糊性,不完整性,抽象层次混乱,3,4.1.2,形式

2、化方法的优点,简洁准确,，是理想的建模工具,验证需求，以,发现存在的矛盾和不完整性,平滑过渡，也可以用于设计,提供了高层,确认,的手段,证明设计符合规格说明,证明程序代码正确地实现了设计结果,4,4.1.3,应用形式化方法的准则,(1),应该选用适当的表示方法。,(2),应该形式化，但不要过分形式化。,(3),应该估算成本。,(4),应该有形式化方法顾问随时提供咨询。,(5),不应该放弃传统的开发方法。,(6),应该建立详尽的文档。,(7),不应该放弃质量标准。,(8),不应该盲目依赖形式化方法。,(9),应该测试、测试再测试。,(10),应该重用。,5,4.2,有穷状态机,例如,当有多个申请

3、占用,CPU,运行的进程时,有关,CPU,分配的进程的状态迁移。,6,进程的状态迁移,7,保险箱的状态转换图,例：一个保险箱上装了一个复合锁，锁有三个位置，分别标记为,1,、,2,、,3,，转盘可向左,(L),或向右,(R),转动。这样，在任意时刻转盘都有,6,种可能的运动，即,1L,、,1R,、,2L,、,2R,、,3L,和,3R,。保险箱的组合密码是,1L,、,3R,、,2L,，转盘的任何其他运动都将引起报警。,8,保险箱的状态转换图,9,有穷状态机的状态转换表,10,有穷状态机的表示,包括,5,个部分：,状态集,J,、,输入集,K,、由当前状态和当前输入确定下一个状态,(,次态,),的,

4、转换函数,T,、,初始态,S,和,终态集,F,。,保险箱的有穷状态机：,状态集,J,：保险箱锁定，,A,，,B,，保险箱解锁，报警。,输入集,K,：,1L,，,1R,，,2L,，,2R,，,3L,，,3R,。,转换函数,T,：如表,4.1,所示。,初始态,S,：保险箱锁定。,终态集,F,：保险箱解锁，报警。,11,有穷状态机5元组表示,表示为一个,5,元组,(J,，,K,，,T,，,S,，,F),，其中：,J,是一个有穷的非空状态集；,K,是一个有穷的非空输入集；,T,是一个从,(J-F)K,到,J,的转换函数；,SJ,，是一个初始状态；,FJ,，是终态集。,12,状态转换表示形式,状态的每个

5、转换都具有下面的形式：,当前状态,菜单,+,事件,所选择的项,下个状态。,加入,谓词集,P,把有穷状态机扩展为一个,6,元组，其中每个谓词都是系统全局状态,Y,的函数。转换函数,T,则是一个从,(J-F)KP,到,J,的函数。转换规则形式如下：,当前状态,菜单,+,事件,所选择的项,+,谓词,下个状态。,13,电梯系统的需求,自然语言描述的对电梯系统的需求：,在一幢,m,层的大厦中需要一套控制,n,部电梯的产品，要求这,n,部电梯按照约束条件,C1,，,C2,和,C3,在楼层间移动。,C1,：每部电梯内有,m,个按钮，每个按钮代表一个楼层。当按下一个按钮时该按钮指示灯亮，同时电梯驶向相应的楼层

6、，到达按钮指定的楼层时指示灯熄灭。,C2,：除了大厦的最低层和最高层之外，每层楼都有两个按钮分别请求电梯上行和下行。这两个按钮之一被按下时相应的指示灯亮，当电梯到达此楼层时灯熄灭，电梯向要求的方向移动。,C3,：当对电梯没有请求时，它关门并停在当前楼层。,14,电梯系统的需求,使用一个扩展的有穷状态机对本产品进行规格说明,:,这个问题中有两个按钮集。,n,部电梯中的每一部都有,m,个按钮，一个按钮对应一个楼层。因为这,mn,个按钮都在电梯中，所以称它们为,电梯按钮,。,每层楼有两个按钮，一个请求向上，另一个请求向下，这些按钮称为,楼层按钮,。,15,电梯系统的需求,电梯按钮的状态转换图如图,4

7、.2,所示。令,EB(e,f),表示按下电梯,e,内的按钮并请求到,f,层去。,EB(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,层,16,电梯按钮的状态转换图,17,电梯按钮的规则描述,定义一个谓

8、词,V(e,f),，它的含义如下：,V(e,f),：电梯,e,停在,f,层,如果电梯按钮,(e,f),处于关闭状态,当前状态,，而且电梯按钮,(e,f),被按下,事件,，而且电梯,e,不在,f,层,谓词,，则该电梯按钮打开发光,下个状态,。,该状态转换规则的形式化描述如下：,EBOFF(e,f)+EBP(e,f)+not V(e,f)EBON(e,f),反之，如果电梯到达,f,层，而且电梯按钮是打开的，于是它就会熄灭。,该转换规则可以形式化地表示为：,EBON(e,f)+EAF(e,f)EBOFF(e,f),18,楼层按钮的状态描述,令楼层按钮,FB(d,f),表示,f,层请求电梯向,d,方向

9、运动的按钮,楼层按钮的状态,如下：,FBON(d,f),：楼层按钮,(d,f),打开,FBOFF(d,f),：楼层按钮,(d,f),关闭,19,楼层按钮的规则描述,如果楼层按钮已经打开，而且一部电梯到达,f,层，则按钮关闭。反之，如果楼层按钮原来是关闭的，被按下后该按钮将打开。,该规则包含了以下,两个事件,：,FBP(d,f),：楼层按钮,(d,f),被按下,EAF(1n,f),：电梯,1,或,或,n,到达,f,层,其中,1n,表示或为,1,或为,2,或为,n,。,20,楼层按钮状态转换图,21,楼层按钮的规则描述,定义一个谓词（是一个状态）：,谓词,S(d,e,f),：电梯,e,停在,f,层

10、并且移动方向由,d,确定为向上,(d=U),或向下,(d=D),或待定,(d=N),。,使用谓词,S(d,e,f),，形式化转换规则为：,FBOFF(d,f)+FBP(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,22,楼层按钮的规则描述,如果在,f,层请求电梯向,d,方向运动的楼层按钮处于关闭状态，现在该按钮被按下，并且当时没有正停在,f,层准备向,d,方向移动的电梯，则该楼层按钮打开。反之，如果楼层按钮已经打开，且至少有一部电梯到达,f,层，该部电梯将朝,d,方向运动，则按钮将关

11、闭。,电梯按钮状态转换规则时定义的谓词,V(e,f),，可以用谓词,S(d,e,f),重新定义：,V(e,f)=S(U,e,f)or S(D,e,f)or S(N,e,f),23,电梯的状态,定义电梯的,3,个状态：,M(d,e,f),：电梯,e,正沿,d,方向移动，即将到达的是第,f,层,S(d,e,f),：电梯,e,停在,f,层，将朝,d,方向移动,(,尚未关门,),W(e,f),：电梯,e,在,f,层等待,(,已关门,),3,个可触发状态发生改变的事件：,DC(e,f),：电梯,e,在楼层,f,关上门,ST(e,f),：电梯,e,靠近,f,层时触发传感器，电梯控制器决定在当前楼层电梯是否

12、停下,RL,：电梯按钮或楼层按钮被按下进入打开状态，登录需求,24,电梯的状态转换图,图,4.4,电梯的状态转换图,25,电梯系统的需求,电梯的状态转换规则,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),第一条规则表明，如果电梯,e,停在,f,层准备向上移动，且门已经关闭，则电梯将向上一楼层移动。第二条和第三条规则，分别对应于电梯即将下降或者没有待处理的请求的情况。,26,4.2.3,评价,规格说明描述格式简单：,当前状态,+,事件,+,谓词 下个状态,易于书写、验证，易于转变成设计或代

13、码,维护可以通过修改规格说明来实现,比数据流图技术更精确,三元组,(,即状态、事件、谓词,),的数量随规模迅速增长,没有处理定时需求,27,4.3 Petri,网,用于确定并发系统中隐含的定时问题,Petri,网包含,4,种元素，四元组,C=(P,T,I,O),一组位置,P,P1,，,P2,，,P3,，,P4,一组转换,T,t1,，,t2,输入函数,I,：,I(t1)=,P2,，,P4,、,I(t2)=,P2,输出函数,O,：,O(t1)=,P1,、,O(t2)=,P3,，,P3,28,Petri网的权标,在,Petri,网中权标,(token),的分配,权标可以用向量,(1,，,2,，,0,

14、，,1),表示,当每个输入位置所,拥有的权标数大于等于从该位置到转换的线数,时，就允许转换,Petri,网中权标总数,不是固定,的,带有标记的,Petri,网成为一个五元组,(P,，,T,，,I,，,O,，,M),29,Petri,网的转换,30,31,32,处理两个进程的同步问题,33,34,含禁止线的Petri网,禁止线是用一个小圆圈而不是用箭头标记的输入线。,通常，当每个输入线上至少有一个权标，而禁止线上没有权标的时候，相应的转换才是允许的。,35,Petri,网表示的电梯系统规格说明,每个楼层用一个位置,F,f,代表,(1fm),电梯用一个权标代表,在位置,F,f,上有权标，表示在楼层

15、,f,上有电梯,1.,电梯按钮,的行为,第一条约束,C1,：每部电梯有,m,个按钮，每层对应一个按钮。当按下一个按钮时该按钮指示灯亮，指示电梯移往相应的楼层。当电梯到达指定的楼层时，按钮将熄灭。,36,Petri,网表示的,电梯按钮,用位置,EB,f,表示楼层,f,的电梯按钮,(1fm),若电梯内楼层,f,的按钮被按下，则在,EB,f,上有一个权标,电梯按钮只有在第一次被按下时才会由暗变亮，以后再按它则只会被忽略。,37,Petri,网表示的,电梯按钮,假设电梯由,g,层驶向,f,层，位置,F,g,上有一个权标,由于每条输入线上各有一个权标，转换“电梯在运行”被激发，从而,EB,f,和,F,g

16、,上的权标被移走，按钮,EB,f,被关闭，在位置,F,f,上出现一个新权标，即转换的激发使电梯由,g,层驶到,f,层。,38,Petri,网表示的,楼层按钮,2.,楼层按钮,的行为,第二条约束,C2,：除了第一层与顶层之外，每个楼层都有两个按钮，一个要求电梯上行，另一个要求电梯下行。这些按钮在按下时发亮，当电梯到达该层并将向指定方向移动时，相应的按钮才会熄灭。,用位置,FB,f,u,和,FB,f,d,表示楼层按钮，分别代表,f,楼层请求电梯上行和下行的按钮。,底层的按钮为,FB,1,u,，最高层的按钮为,FB,m,d,，中间每一层有两个按钮,FB,f,u,和,FB,f,d,(1,f,m),。,39,Petri网表示楼层按钮,电梯由,g,层驶向,f,层,如果两个按钮都亮了，则只有一个按钮熄灭,第三条约束,C3,：当电梯没有收到请求时，它将停留在当前楼层并关门。,(FBf,u,和,FBf,d,上无权标）,40,