软件工程导论class5形式化说明技术

《软件工程导论class5形式化说明技术》由会员分享，可在线阅读，更多相关《软件工程导论class5形式化说明技术（43页珍藏版）》请在装配图网上搜索。

1、,,单击此处编辑母版标题样式,,单击此处编辑母版文本样式,,第二级,,第三级,,第四级,,第五级,,,,*,,,单击此处编辑母版标题样式,,单击此处编辑母版文本样式,,第二级,,第三级,,第四级,,第五级,,,,*,软件工程导论第,5,课,第,4,章 形式化说明技术,第,4,章 形式化说明技术,软件工程方法分类,,非形式化,,自然语言,,半形式化,,数据流图,,实体,-,联系图建立模型,,形式化,,有穷状态机,,,Petri,网,,,Z,语言,,形式化方法,:,描述系统性质的基于数学的技术,,4.1,概述,4.1.1,非形式化方法的缺点,,矛盾,：指一组相互冲突的陈述,,二义性,：读者可

2、以用不同方式理解的陈述,,含糊性,：系统规格说明书是很庞大的文档,,,难以杜绝含糊性措辞,,不完整性,：对实体的描述不全面,,抽象层次混乱,：在非常抽象的陈述中混进了一些关于细节的低层次陈述,,,,4.1.2,形式化方法的优点,理想的建模工具,,数学最有用的一个性质是，它能够简洁准确地描述物理现象、对象或动作的结果。特别适于表示状态。,,在理想情况下，分析员可以写出系统的数学规格说明， 它准确到几乎没有二义性，而且可以用数学方法来验 证，以发现存在的矛盾和不完整性，在这样的规格说明 中完全没有含糊性,4.1.2,形式化方法的优点,可以在不同的软件工程活动之间平滑地过渡,不仅功能规格说明，而且系

3、统设计也可以用数学表达,,提供了高层确认的手段,可以使用数学方法证明，设计符合规格说明，程序代码 正确地实现了设计结果,,,,4.1.3,应用形式化方法的准则,形式化方法有争议，要一分为二,,应用形式化方法的准则如下：,,(1),应该选用适当的表示方法,。一种规格说明技术只能用自然的方式说明某一类概念，适用于一定范围,,(2),应该形式化，但不要过分形式化,。目前的形式化技术还不适于描述系统的每个方面。,,,主要,用形式化方法仔细说明系统中易出错的或关键的部分,,,4.1.3,应用形式化方法的准则,(3),应该估算成本,,为了使用形式化方法，通常需要事先进行大量的培训,,(4),应该有形式化方

4、法顾问随时提供咨询,,绝大多数软件工程师对形式化方法中使用的数学和逻辑 并不很熟悉，而且没受过使用形式化方法的专业训练,,需要专家指导和培训,,,4.1.3,应用形式化方法的准则,(5),不应该放弃传统的开发方法,,形式化方法和结构化方法或面向对象方法集成起来可能 取长补短,,(6),应该建立详尽的文档,,使用自然语言注释形式化的规格说明书，以帮助用户和 维护人员理解系统,,,4.1.3,应用形式化方法的准则,(7),不应该放弃质量标准,,形式化方法仅仅有助于开发出高质量软件的一种手段,,,系统开发过程中仍然必须一如既往地实施其他质量保证活动,,(8),不应该盲目依赖形式化方法,,形式化方法并

5、不能保证开发出的软件绝对正确,,,，必须用其他方法,(,例如，评审、测试,),来验证软件正确性,,,4.1.3,应用形式化方法的准则,(9),应该测试、测试再测试,,形式化方法不仅不能保证软件系统绝对正确，也不能证明系统性能或其他质量指标符合需要，因此，软件测试的重要性并没有降低。,,(10),应该重用,,软件重用仍然是降低软件成本和提高软件质量的惟一合理的方法。形式化方法说明的软件构件具有清晰定义的功能和接 口，使得它们有更好的可重用性,,4.2,有穷状态机,有穷状态机可以准确地描述一个系统，是表达规格说明的一种形式化方法,。,,[,保险箱实例,],,一个保险箱上装了一个复合锁，锁有三个位置

6、，分别标记为,1,、,2,、,3,，转盘可向左,(L),或向右,(R),转动。这样，在任意时刻转盘都有,6,种可能的运动，即,1L,、,1R,、,2L,、,2R,、,3L,和,3R,。保险箱的组合密码是,1L,、,3R,、,2L,，转盘的任何其他运动都将引起报警。图,4.1,描绘了保险箱的状态转换情况。,4.2.1,概念,,4.2.1,概念,,4.2.1,概念,有穷状态机,5,部分,,状态集,J,,输入集,K,,转换函数,T:,由当前状态和当前输入确定下一个状态,(,次态,),,初始态,S,,终态集,F,,,,,4.2.1,概念,有穷状态机可以表示为一个,5,元组,(J,，,K,，,T,，,

7、S,，,F),,J,是一个有穷的非空状态集；,,K,是一个有穷的非空输入集；,,T,是一个从,(J-F)×K,到,J,的转换函数；,,S,∈,J,，是一个初始状态；,,F,∈,J,，是终态集。,,,4.2.1,概念,[,保险箱实例,],,状态集,J,：｛保险箱锁定，,A,，,B,，保险箱解锁，报警｝,,输入集,K,：｛,1L,，,1R,，,2L,，,2R,，,3L,，,3R,｝,,转换函数,T,：如表,4.1,所示,,初始态,S,：保险箱锁定,,终态集,F,：｛保险箱解锁，报警｝,,,,4.2.1,概念,有穷状态机的应用,,每个菜单驱动的用户界面,:,一个菜单的显示和一个状态相对应，键盘输入或

8、用鼠标选择一个图标是使系统进入其他状态 的一个事件,,状态的每个转换都具有下面的形式：,,当前状态,〔,菜单,〕,+,事件,〔,所选择的项,〕 →,下个状态。,,当前状态,〔,菜单,〕,+,事件,〔,所选择的项,〕+,谓词→ 下个状态,,增加一个谓词集,P,，把有穷状态机扩展为一个,6元组,,(J,，,K,，,T,，,S,，,F，P),,,,,,4.2.2,例子,用自然语言描述的电梯系统需求,,4.2.2,例子,用有穷状态机描述的电梯系统需求,,4.2.2,例子,用有穷状态机描述的电梯系统需求,,4.2.2,例子,用有穷状态机描述的电梯系统需求,,4.2.2,例子,用有穷状态机描述的电梯系统需

9、求,,4.2.2,例子,用有穷状态机描述的电梯系统需求,,4.2.2,例子,用有穷状态机描述的电梯系统需求,,4.2.2,例子,用有穷状态机描述的电梯系统需求,,,4.2.3,评价,有穷状态机用简单的格式来描述规格说明,,4.3 Petri,网,Petri,网,(Carl Adam Petri,发明,),用于确定系统中隐含的定时问题的一种有效技术,,,用于解决如同步问题、竞争条件以及死锁问题等问题,,应用领域,,自动化,,性能评价,,操作系统,,软件工程 有效地描述,并发活动,,,,4.3.1,概念,Petri4,元素,,一组位置,P,,一组转换,T,,输入函数,I,,输出函数,O,,P

10、,为｛,P1,，,P2,，,P3,，,P4,｝，圆圈,,T,为｛,t1,，,t2,｝，短直线,,I(t1)=,｛,P2,，,P4,｝,I(t2)=,｛,P2,｝,,,位置指向转换的箭头,,O(t1)=,｛,P1,｝,O(t2)=,｛,P3,，,P3,｝,,,4.3.1,概念,形式化的,Petri,网结构四元组,, C=(P,T,I,O),。,,P=,｛,P1,，,…,，,Pn,｝是一个有穷位置集，,n,≥,0,。,,T=,｛,t1,，,…,，,tm,｝是一个有穷转换集，,m,≥,0,，且,T,和,P,不相交。,,I,：,T,→,P,∞为输入函数，是由转换到位置无序单位组,(bags),的映射。

11、,,O,：,T,→,P,∞为输出函数，是由转换到位置无序单位组的映射。,,无序单位组或多重组是允许一个元素有多个实例的广义集,,,4.3.1,概念,Petri,网的权标,·，,,见图4.6,,P,1,中1个小黑点，P,2,中2个，P,4,中1 个,,可用向量表示,(1，2，0，1),,当一个位置拥有的,权标数大于等于,从它到转换的,线数,时，就允许转换,,当,t,1,被激发，,P,2,和P,4,各有一个权标被移走，P,1,增加一个权标,,4.3.1,概念,图,4.7,上,P2有权标，,,因此t2,也被激发，,,P2移走一个权标，,,P3上新增加2个权标，如图4.8,所示,。,,形式化说，,Pe

12、tri,网是一组位置到一向量的映射,,M：P→{0,1，2，…},,带有标记的,Petri,网成为一个,5元组,,(P，T，I，O，M),4.3.1,概念,对,Petri,网的一个重要扩充是加入禁止线，禁止线用一个小圆圈标记输入线。当输入线上至少有一个权标，而禁止线上没有权标时，相应的转换才是允许的。如图,4.9,，,P,3,上有一个权标而P,2,上没有，,,因此转换t,1,可以激发。,4.3.2,例子,F,f,表示楼层，电梯用权标代表，在位置,F,f,有,权标,，表示在,楼层,f,上有电梯,。,,电梯中楼层,f的按钮，用位置EB,f,表示。在,EB,f,,上有一个,权标,，表示,电梯内楼层,

13、f,的按钮,被 按下了。,,,2,楼层按钮,,4.4 Z,语言,在形式化的规格说明语言中，,Z语言贏得了广泛的赞誉。使用Z语言需要具备集合论、函数、数理逻辑等方面的知识。,,Z语言是相当难学的，因为它除了使用集合论,和数理逻辑符号外，还使用一些特殊符号。,4.4 .1,简介,用Z语言描述的、最简单的形式化规格说明含有下述4部分,,给定的集合、数据类型及常数,,状态定义,,初始状态,,操作,1,给定的集合,给定的初始化集合，就是不需要详细定义的集合，用带方括号的形式表示。,,例如：电梯问题给定的初始化集合称为,Button,,表示：,[Button],2,状态定义,一个,Z规格说明由几个格(sc

14、hema),组成，每个格由一组变量说明和一系列限定变量取值范围的谓词，例如图,4.12,,图,4.13,是电梯例子的状态定义,3,初始状态,第一次开启时的状态,,电梯的初始状态,,,表示：当系统首次开启时,pushed,集为空，即所有的按钮都处于关闭状态。,4,操作,Z语言语法规定，当一个格被,用在另一个格中时，要在它的前面加上一个三角形符号,,电梯的例子,,△,4,操作,电梯例子，到达楼层,,△,4.4.2,评价,Z语言成功的原因：,,(1)容易发现用Z写的规格说明的错误,,(2)用Z写规格说明时，要十分精确地使用Z说明符，减少了不一致性和遗漏。,,(3)可以严格地验证说明的正确性。,,(4)学会编写Z规格说明比较容易,,(5)减少开发总时间，减少费用,,(6)可以用自然语言重写规格说明，说明更清楚，更正确。,