软件工程第章13

单击此处编辑母版标题样式,单击此处编辑母版副标题样式,第,4,章 形式化说明技术,4.1,概述,4.2,有穷状态机,4.3 Petri,网,4.4 Z,语言,4.5,小结,习题,按照形式化的程度，可以把软件工程使用的方法划分成非形式化、半形式化和形式化,3,类,:,用自然语言描述需求规格说明，是典型的非形式化方法。,用数据流图或实体,-,联系图建立模型，是典型的半形式化方法。,所谓形式化方法，是描述系统性质的基于数学的技术，也就是说，如果一种方法有坚实的数学基础，那么它就是形式化的。,用自然语言书写的系统规格说明书，可能存在矛盾、二义性、含糊性、不完整性及抽象层次混乱等问题。,4.1,概述,4.1.1,非形式化方法的缺点,为了克服非形式化方法的缺点，人们把数学引入软件开发过程，创造了基于数学的形式化方法。,数学最有用的一个性质是，它能够简洁准确地描述物理现象、对象或动作的结果，因此是理想的建模工具。数学特别适合于表示状态，也就是表示“做什么”。,需求规格说明书主要描述应用系统在运行前和运行后的状态，因此，数学比自然语言更适于描述详细的需求。,4.1.2,形式化方法的优点,应该选用适当的表示方法。,(2),应该形式化，但不要过分形式化。,(3),应该估算成本。,(4),应该有形式化方法顾问随时提供咨询。,(5),不应该放弃传统的开发方法。,(6),应该建立详尽的文档。,(7),不应该放弃质量标准。,(8),不应该盲目依赖形式化方法。,(9),应该测试、测试再测试。,(10),应该重用。,4.1.3,应用形式化方法的准则,简单例子介绍有穷状态机的基本概念。,一个保险箱上装了一个复合锁，锁有三个位置，分别标记为,1,、,2,、,3,，转盘可向左,(L),或向右,(R),转动。,保险箱的组合密码是,1L,、,3R,、,2L,，转盘的任何其他运动都将引起报警。,4.2,有穷状态机,4.2.1,概念,图,4.1,保险箱的状态转换图,从上面这个简单例子可以看出，一个有穷状态机包括下述,5,个部分：,状态集,J:,保险箱锁定，,A,，,B,，保险箱解锁，报警。,输入集,K,：,1L,，,1R,，,2L,，,2R,，,3L,，,3R,。,转换函数,T,：由当前状态和当前输入确定下一个状态,(,次态,),如表,4.1,所示。,初始态,S,：保险箱锁定。,终态集,F,：保险箱解锁，报警。,如果使用更形式化的术语，一个有穷状态机可以表示为一个,5,元组,(J,，,K,，,T,，,S,，,F),，其中：,J,是一个有穷的非空状态集；,K,是一个有穷的非空输入集；,T,是一个从,(J-F)K,到,J,的转换函数；,SJ,，是一个初始状态；,FJ,，是终态集。,用自然语言,描,描述的对电,梯,梯系统的需,求,求：,在一幢,m,层的大厦中,需,需要一套控,制,制,n,部电梯的产,品,品，要求这,n,部电梯按照,约,约束条件,C1,，,C2,和,C3,在楼层间移,动,动。,C1,：每部电梯,内,内有,m,个按钮，当,按,按下一个按,钮,钮时,电梯驶向相,应,应的楼层。,C2,：每层楼都,有,有两个按钮,分,分别请求电,梯,梯上行和下,行,行。电梯向,要,要求的方向,移,移动。,C3,：当对电梯,没,没有请求时,，,，它关门并,停,停在当前楼,层,层。,例子,有穷状态机,对,对本产品进,行,行规格说明,:,这个问题中,有,有两个按钮,集,集。,n,部电梯中的,每,每一部都有,m,个按钮，一,个,个按钮对应,一,一个楼层。,因,因为这,mn,个按钮都在,电,电梯中，所,以,以称它们为,电,电梯按钮。,每层楼有两,个,个按钮，一,个,个请求向上,，,，另一个请,求,求向下，这,些,些按钮称为,楼,楼层按钮。,图,4.2,电梯按钮的,状,状态转换图,图,4.3,楼层按钮的,状,状态转换图,图,4.4,电梯的状态,转,转换图,给出电梯的,状,状态转换规,则,则,:,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,层准备向上,移,移动，且门,已,已经关闭，,则,则电梯将向,上,上一楼层移,动,动。,第二条和第,三,三条规则，,分,分别对应于,电,电梯即将下,降,降或者没有,待,待处理的请,求,求的情况。,有穷状态机,方,方法采用了,一,一种简单的,格,格式来描述,规,规格说明：,当前状态,+,事件,+,谓词下个,状,状态,这种形式的,规,规格说明易,于,于书写、易,于,于验证，而,且,且可以比较,容,容易地把它,转,转变成设计,或,或程序代码,。,。,有穷状态机,方,方法比数据,流,流图技术更,精,精确,评价,并发系统中,遇,遇到的一个,主,主要问题是,定,定时问题。,用于确定系,统,统中隐含的,定,定时问题的,一,一种有效技,术,术是,Petri,网，,Petri,网是由,CarlAdamPetri,发明的。,在性能评价,、,、操作系统,和,和软件工程,等,等领域，,Petri,网应用得都,比,比较广泛。,Petri,网包含,4,种元素：一,组,组位置,P,、一组转换,T,、输入函数,I,以及输出函,数,数,O,。,4.3Petri,网,概念,图,4.5 Petri,网的组成,图,4.6,带标记的,Petri,网,图,4.7,图,4.6,的,Petri,网在,转,转换,t1,被激,发,发后,的,的情,况,况,图,4.8,图,4.7,的,Petri,网在,转,转换,t2,被激,发,发后,的,的情,况,况,现在,把,把,Petri,网应,用,用于,电,电梯,问,问题,。,。,当用,Petri,网表,示,示电,梯,梯系,统,统的,规,规格,说,说明,时,时，,每,每个,楼,楼层,用,用一,个,个位,置,置,Ff,代表,(1,f,m),，在,Petri,网中电,梯,梯是用,一,一个权,标,标代表,的,的。,在位置,Ff,上有权,标,标，表,示,示在楼,层,层,f,上有电,梯,梯。,例子,图,4.10 Petri,网表示,的,的电梯,按,按钮,图,4.11 Petri,网表示,楼,楼层按,钮,钮,用,Z,语言描,述,述的、,最,最简单,的,的形式,化,化规格,说,说明含,有,有下述,4,个部分,：,：,给定的,集,集合、,数,数据类,型,型及常,数,数。,状态定,义,义。,初始状,态,态。,操作。,4.4Z,语言,简介,1.,给定的,集,集合,对于电,梯,梯问题,，,，给定,的,的初始,化,化集合,称,称为,Button,，即所,有,有按钮,的,的集合,，,，因此,，,，,Z,规格说,明,明开始,于,于：,Button,2.,状态定,义,义,一个,Z,规格说,明,明由若,干,干个“,格,格,(schema)”,组成，,每,每个格,含,含有变,量,量说明,和,和限定,变,变量取,值,值范围,的,的谓词,。,。例如,，,，格,S,的格式,如,如图,4.12,所示。,图,4.12Z,格,S,的格式,3.,初始状,态,态,对于电,梯,梯问题,来,来说，,抽,抽象的,初,初始状,态,态为：,Button_Init,Button_State,pushed=,上式表,示,示，当,系,系统首,次,次开启,时,时,pushed,集为空,，,，即所,有,有按钮,都,都处于,关,关闭状,态,态。,4.,操作,如果一,个,个原来,处,处于关,闭,闭状态,的,的按钮,被,被按下,，,，则该,按,按钮开,启,启，这,个,个按钮,就,就被添,加,加到,pushed,集中。,图,4.13Z,格,Button_State,图,4.14,操作,Push_Button,的,Z,规格说,明,明,图,4.15,操作,Floor_Arrival,的,Z,规格说,明,明,目前，,Z,也许是,应,应用得,最,最广泛,的,的形式,化,化语言,，,，尤其,是,是在大,型,型项目,中,中,Z,语言的,优,优势更,加,加明显,。,。,使用形,式,式化规,格,格说明,是,是全球,的,的总趋,势,势，过,去,去，主,要,要是欧,洲,洲习惯,于,于使用,形,形式化,规,规格说,明,明技术,，,，现在,越,越来越,多,多的美,国,国公司,也,也开始,使,使用形,式,式化规,格,格说明,技,技术。,评价,基于数,学,学的形,式,式化规,格,格说明,技,技术，,目,目前还,没,没有在,软,软件产,业,业界广,泛,泛应用,。,。,形式化,方,方法比,欠,欠形式,化,化方法,更,更难学,习,习，不,仅,仅在培,训,训阶段,要,要花大,量,量的投,资,资，而,且,且对某,些,些软件,工,工程师,来,来说，,它,它代表,了,了一种,“,“文化,冲,冲击”,。,。,把形式,化,化方法,和,和欠形,式,式化方,法,法有机,地,地结合,起,起来，,使,使它们,取,取长补,短,短，应,该,该能获,得,得更理,想,想的效,果,果。,4.5,小结,4-1,举例对,比,比形式,化,化方法,和,和欠形,式,式化方,法,法的优,缺,缺点。,4-2,在,在什,么,么情况,下,下应该,使,使用形,式,式化说,明,明技术?使用,形,形式化,说,说明技,术,术时应,遵,遵守哪,些,些准则?,4-3,一个浮,点,点二进,制,制数的,构,构成是,：,：一个,可,可选的,符,符号,(+,或,-),，后跟,一,一个或,多,多个二,进,进制位,，,，再跟,上,上一个,字,字符,E,，再加,上,上另一,个,个可选,符,符号,(+,或,-),及一个,或,或多个,二,二进制,位,位。例,如,如，下,列,列的字,符,符串都,是,是浮点,二,二进制,数,数：,习题,110101E-101,-100111E11101,+1E0,更形式,化,化地，,浮,浮点二,进,进制数,定,定义如,下,下：,floating,pointbinary=,sign,bitstringE,sign,bitstring,sign,=+,-,bitstring=bit,bitstring,bit=0,1,其中，,符号,=,表示定,义,义为；,符号,.,表示,可,可选项,；,；,符号,a,b,表示,a,或,b,。,假设有,这,这样一,个,个有穷,状,状态机,：,：以一,串,串字符,为,为输入,，,，判断,字,字符串,中,中是否,含,含有合,法,法的浮,点,点二进,制,制数。,试,试对这,个,个有穷,状,状态机,进,进行规,格,格说明,。,。,4-4,考虑下述,的,的自动化,图,图书馆流,通,通系统：,每,每本书都,有,有一个条,形,形码，每,个,个借阅人,都,都有一个,带,带有条形,码,码的卡片,。,。当一个,借,借阅人想,借,借一本书,时,时，图书,管,管理员扫,描,描书上的,条,条形码和,借,借阅人卡,片,片上的条,形,形码，然,后,后在计算,机,机终端上,输,输入,C,；当归还,一,一本书时,，,，图书管,理,理员将再,做,做一次扫,描,描，并输,入,入,R,。图书管,理,理员可以,把,把一些书,加,加到,(+),图书集合,中,中，也可,以,以删除,(-),它们。,借阅人可,以,以在终端,上,上查找到,某,某个作者,所,所有的书,(,输入“,A=”,和作者名,字,字,),，或具有,指,指定标题,的,的所有书,籍,籍,(,输入“,T=”,和标题,),，或属于,特,特定主题,范,范围内的,所,所有图书,(,输入“,S=”,加主题范,围,围,),。最后，,如,如果借阅,人,人想借的,书,书已被别,人,人借走，,图,图书管理,员,员将给这,本,本书设置,一,一个预约,，,，以便书,归,归还时把,书,书留给预,约,约的借阅,人,人,(,输入“,H=”,加书号,),。,试用有穷,状,状态机说,明,明上述的,图,图书流通,系,系统。,4-5,试用,Petri,网说明第,4,题所述图,书,书馆中一,本,本书的循,环,环过程。,在,在规格说,明,明中应该,包,包括操作