第4章-形式化说明技术--软件工程.ppt

,*,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,单击此处编辑母版标题样式,第四章 形式化说明技术,按照形式化的程度，可以把软件工程使用的方法划分成非形式化、半形式化和形式化3类,非形式化：自然语言,半形式化：数据流图,形式化：基于数学的技术。就是说，如果一种方法有坚实的数学基础，那么它就是形式化的。,4.1 概述,非形式化方法的缺点,用自然语言书写的系统规格说明书，可能存在矛盾、二义性、含糊性、不完整性及抽象层次混乱等问题。,所谓矛盾是指一组相互冲突的陈述。,二义性是指读者可以用不同方式理解的陈述。,在开发大型软件系统的过程中应用数学，能够带来下述的几个优点：,数学最有用的一个性质是，它能够简洁准确地描述物理现象、对象或动作的结果，因此是理想的建模工具。数学特别适合于表示状态，也就是表示“做什么”。,4.1.2 形式化方法的优点,事实上。,但是，实际情况并不这么简单，软件系统的复杂性是出了名的，希望用少数几个数学公式来描述它，是根本不可能的。,此外，即使应用了形式化方法，完整性也是难于保证的：由于沟通不够，可能遗漏了客户的一些需求；规格说明的撰写者可能有意省略了系统的某些特征，以便设计者在选择实现方法时有一定自由度；要设想出使用一个大型复杂系统的每一个可能的情景，通常是做不到的。,其他的优点。,不仅功能规格说明，而且系统设计也可以用数学表达,它提供了高层确认的手段。可以使用数学方法证明，设计符合规格说明，程序代码正确地实现了设计结果。,对形式化方法既不要过分夸大它的优点也不要一概排斥。为了更好地发挥这种方法的长处，下面给出应用形式化方法的几条准则，供读者在实际工作中使用。,4.1.3 应用形式化方法的准则,(7)不应该放弃质量标准。,(8)不应该盲目依赖形式化方法。,(9)应该测试、测试再测试。,(10)应该重用。即使采用了形式化方法，软件重用仍然是降低软件成本和提高软件质量的惟一合理的方法。,4.2 有穷状态机,最简单的有穷自动机,关,开,按,按,开始,两相开关，根据开关状态起作用,一个保险箱上装了一个复合锁，锁有三个位置，分别标记为1、2、3，转盘可向左(L)或向右(R)转动。这样，在任意时刻转盘都有6种可能的运动，即1L、1R、2L、2R、3L和3R。保险箱的组合密码是1L、3R、2L，转盘的任何其他运动都将引起报警。图4.1描绘了保险箱的状态转换情况。,第三个例子,包括,5,部分：状态集,J,、输入集,K,、由当前状态和当前输入确定下一个状态,(,次态,),的转换函数,T,、初始态,S,和终态集,F,。,对于保险箱的例子,:,状态集,J,：保险箱锁定，,A,，,B,，保险箱解锁，报警。,输入集,K,：,1L,，,1R,，,2L,，,2R,，,3L,，,3R,。,转换函数,T,：如表,4.1,所示。,初始态,S,：保险箱锁定。,终态集,F,：保险箱解锁，报警,例如，每个菜单驱动的用户界面都是一个有穷状态机的实现。一个菜单的显示和一个状态相对应，键盘输入或用鼠标选择一个图标是使系统进入其他状态的一个事件。状态的每个转换都具有下面的形式：,当前状态菜单+事件所选择的项下个状态。,例子：电梯系统,在一幢m层的大厦中需要一套控制n部电梯的产品，要求这n部电梯按照约束条件C1,C2和C3在楼层间移动。,C1：每部电梯内有m个按钮，每个按钮代表一个楼层，按下一个按钮时该按钮指示灯亮，同时电梯驶向相应楼层，到达指定的楼层时指示灯灭。,C2：除了大厦的最低层和最高层外，每层楼都有两个按钮分别请求电梯上行和下行。这两个按钮之一被按下时相应的指示灯亮，当电梯到达此楼层时灯熄灭，电梯向要求的方向移动。,C3：当对电梯没有请求时，它关门并挺在当前楼层。,电梯按钮的状态转换图,EBON(e,f)：电梯e内的f层按钮指示灯亮的状态,EBOFF(e,f)：电梯e内的f层按钮的指示灯熄灭的状态,EBP(e,f)：电梯按钮(e,f)被按下,EAF(e,f)：电梯e到达f层,V(e,f)：谓词，表示电梯e停在f层,EBOFF(e,f)+EBP(e,f)+not V(e,f),EBON(e,f),EBON(e,f)+EAF(e,f)EBOFF(e,f),楼层按钮的状态转换图,FBON(d,f)：楼层按钮(d,f)打开。(d,f)表示f层请求电梯向d方向运动的按钮,FBOFF(d,f)：楼层按钮(d,f)关闭,FBP(d,f)：楼层按钮(d,f)被按下的事件,EAF(1,n,f)：电梯1或,或n,到达f层,S(d,e,f)：谓词，电梯e停在f层并且移动方向由d确定为向上(d=U)或向下(d=D)或待定(d=N),FBOFF(d,f)+FBP(d,f)+not S(d,1,n,f)FBON(d,f),FBON(d,f)+EAF(1n,f)+S(d,1n,f)FBOFF(d,f),电梯的状态转换图,触发电梯状态改变的事件,DC(e,f)：电梯e在楼层f关上门,ST(e,f)：电梯e靠近f层时触发传感器，电梯控制器决定在当前楼层是否停下,RL：电梯按钮或楼层按钮被按下进入打开状态，登陆需求,电梯的状态转换规则,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.3评价,转换规则书写简单，易于验证,可以比较容易地把它转换成设计或程序代码,比数据流图更精确，而且一样易于理解,开发大系统时，三元组(状态、事件、谓词)的数量会迅速增长,和数据流图一样也没有处理定时需求。,Petri网的组成,Petri网的组成,包含种元素：一组位置、一组转换、输入函数和输出函数,位置PP1,P2,P3,P4，用圆圈表示,转换T(t1,t2)，用短直线表示,用于转换的输入函数，用由位置指向转换的箭头表示。图中的输入函数为：,I(t1)=P2,P4,I(t2)=P2,用于转换的输出函数，用由转换指向位置的箭头表示。图中的输出函数为：,O(t1)=P1,O(t2)=P3,P4,带标记的Petri网,带标记的Petri网,Petri网的标记是在Petri网中权标(token)的分配。,通常，当每个输入位置所拥有的权标数大于等于从该位置到转换的线数时，就允许转换,当转换被激发时，其所有输入状态上都会有一个权标被移出，而其输出状态上会增加一个权标,Petri网中权标的总数是不固定的。,上图中的转换t1被激发后的Petri网如下图所示,图4.6中t1转换被激发后的Petri网,图4.7中t2转换被激发后的Petri网,带禁止线的Petri网,禁止线是用一个小圆圈，而不是箭头标记的输入线。,通常，当每个输入线上至少有一个权标，而禁止线上没有权标的时候，转换才允许发生。图4.9中的转换t1可以发生。,带禁止线的Petri网,例子：用Petri网表示电梯系统,每个楼层用一个位置F,f,(1,fm),电梯用权标表示,位置F,f,上有权标，表示在楼层f上有电梯,电梯中楼层f的按钮用位置EB,f,表示(1,fm)，在位置EB,f,上有一个权标，表示电梯内楼层f的按钮被按下,楼层按钮用位置和表示，分别代表f层请求电梯上行和下行的按钮,Petri网表示的电梯按钮状态,Petri网表示的楼层按钮状态,