第4章软件工程.ppt
《第4章软件工程.ppt》由会员分享,可在线阅读,更多相关《第4章软件工程.ppt(64页珍藏版)》请在三一文库上搜索。
1、2019/6/4,湖南科技大学 计算机学院 戴祖雄,1,第4章 形式化说明技术,教学目标及基本要求 : 1.了解形式化与非形式化的区别 2.了解应用形式化方法的准则 3.掌握有穷状态机 4.掌握Petri网 5.掌握Z语言,教学重点: 1.有穷状态机 2.Petri网,学时数:2课时,教学难点: 有穷状态机和Petri网的具体应用,2019/6/4,湖南科技大学 计算机学院 戴祖雄,2,习题 : 1 举例对比形式化方法和欠形式化方法的优缺点。 2 在什么情况下应该使用形式化说明技术?使用形式化说明技术时应遵守哪些准则? 3 考虑下述的自动化图书馆流通系统:每本书都有一个条形码,每个借阅人都有一
2、个带有条形码的卡片。当一个借阅人想借一本书时,图书管理员扫描书上的条形码和借阅人卡片上的条形码,然后在计算机终端上输入C;当归还一本书时,图书管理员将再做一次扫描,并输入R。图书管理员可以把一些书加到(+)图书集合中,也可以删除(-)它们。 借阅人可以在终端上查找到某个作者所有的书(输入“A=”和作者名字),或具有指定标题的所有书籍(输入“T=”和标题),或属于特定主题范围内的所有图书(输入“S=”加主题范围)。最后,如果借阅人想借的书已被别人借走,图书管理员将给这本书设置一个预约,以便书归还时把书留给预约的借阅人(输入“H=”加书号)。 试用有穷状态机说明上述的图书流通系统。,2019/6/
3、4,湖南科技大学 计算机学院 戴祖雄,3,教学内容 4.1 概述 4.2 有穷状态机 4.3 Petri网 4.4 Z语言 4.5 小结,2019/6/4,湖南科技大学 计算机学院 戴祖雄,4,第4章 形式化说明技术,根据形式化的程度,可以把软件工程方法划分成非形式化、半形式化和形式化三类。使用自然语言描述需求规格说明,是典型的非形式化方法。使用数据流图或实体关系图等图形符号建立模型,是典型的半形式化方法。 用于开发计算机系统的形式化方法,是描述系统性质的基于数学的技术,也就是说,如果一个方法有坚实的数学基础,那么它就是形式化的。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,5,4.1
4、 概述,4.1.1 非形式化方法的缺点 基本上使用自然语言描述的系统规格说明,可能存在矛盾、二义性、含糊性、不完整性以及抽象层次混杂等问题。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,6,4.1.2 形式化方法的优点 数学最有用的性质之一是,它能够简洁、准确地描述物理现象、对象或动作的结果,因此是理想的建模工具。 在软件开发过程中使用数学的另一个优点是,可以在软件工程活动之间平滑地过渡。不仅功能规格说明,而且系统设计也可以用数学表达,当然,程序代码也是一种数学符号。 数学作为软件开发工具的最后一个优点是,它提供了高层确认的手段。可以使用数学方法证明,设计符合规格说明,程序代码正确地反
5、映了设计结果。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,7,4.1.3 应用形式化方法的准则 应用形式化方法的几条准则: 选择适用于当前项目的符号系统。 应该形式化,但不要过分形式化。 应该进行成本/效益分析。 需要有形式化方法的顾问。 不要放弃传统的开发方法。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,8,应该建立详尽的文档。 不应该放弃质量标准。 不应该盲目依赖形式化方法。 应该测试、测试再测试。 应该重用。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,9,4.2 有穷状态机,利用有穷状态机可以准确地描述一个系统,因此是表达规格说明的一种形式化方法。 4.2.
6、1 基本概念 下面通过一个简单例子介绍有穷状态机的基本概念。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,10,一个保险箱上装了一个复合锁,锁有三个位置,分别标记为1、2、3,转盘可向左(L)或向右(R)转动。这样,在任意时刻转盘都有6种可能的运动,即1L、1R、2L、2R、3L和3R。保险箱的组合密码是1L、3R、2L,转盘的任何其他运动都将引起报警。图4.1描绘了保险箱的状态转换情况。 图4.1是一个有穷状态机的状态转换图。状态转换并不一定要用图形方式描述,表4.1的表格形式也可以表达同样的信息。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,11,图4.1 保险箱的状态转换
7、图,2019/6/4,湖南科技大学 计算机学院 戴祖雄,12,2019/6/4,湖南科技大学 计算机学院 戴祖雄,13,从上面这个简单例子可以看出,一个有穷状态机包括下述5个部分:状态集J、输入集K、由当前状态和当前输入确定下一个状态(次态)的转换函数T、初始态S和终态集F。 如果使用更形式化的术语,一个有穷状态机可以表示为一个5元组(J,R,T,S,F),其中: J是一个有穷的非空状态集; K是一个有穷的非空输入集; T是一个从(J-F)K到J的转换函数; SJ,是一个初始状态; FJ,是终态集。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,14,当前状态菜单+事件所选择的项下个状态
8、 为了对一个系统进行规格说明,通常都需要对有穷状态机做一个很有用的扩展,即在前述的5元组中加入第6个组件谓词集P,即把有穷状态机扩展为一个6元组,其中每个谓词都是系统全局状态Y的函数。转换函数T现在是一个从(J-F)KP到J的函数。现在的转换规则形式如下: 当前状态菜单+事件所选择的项+谓词下个状态,2019/6/4,湖南科技大学 计算机学院 戴祖雄,15,4.2.2 例子(电梯问题) 电梯按钮的状态转换图如图4.2所示。令EB(e,f)表示按下电梯e内的按钮并请求到f层去。EB(e,f)有两个状态,分别是按钮发光(打开)和不发光(关闭)。更精确地说,状态是: EBON(e,f):电梯按钮(e
9、,f)打开 EBOFF(e,f):电梯按钮(e,f)关闭 如果电梯按钮(e,f)发光且电梯到达f层,该按钮将熄灭。相反如果按钮熄灭,则按下它时,按钮将发光。上述描述中包含了两个事件,它们分别是:,2019/6/4,湖南科技大学 计算机学院 戴祖雄,16,图4.2 电梯按钮的状态转换图,2019/6/4,湖南科技大学 计算机学院 戴祖雄,17,EBP(e,f):电梯按钮(e,f)被按下 EAF(e,f):电梯e到达f层 为了定义与这些事件和状态相联系的状态转换规则,需要一个谓词V,(e,f),它的含义如下: V(e,f):电梯e停在f层 如果电梯按钮(e,f)处于关闭状态当前状态,而且电梯按钮(
10、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),2019/6/4,湖南科技大学 计算机学院 戴祖雄,18,接下来让我们考虑楼层按钮。令FB(d,f)表示f层的按钮请求电梯向d方向运动,楼层按钮FB(d,f)的状态转换图如图4.3所示。 楼层按钮的状态如下: FBON(d,f):楼层按钮(d,f)打开; F
11、BOFF(d,f):楼层按钮(d,f)关闭。 如果楼层按钮已经打开,而且一部电梯到达f层,则按钮关闭。反之,如果楼层按钮原来是关闭的,被按下后该按钮将打开。这段叙述中包含了以下两个事件: FBP(d,f):楼层按钮(d,f)被按下 EAF(1n,f):电梯1或或n到达f层 其中1n表示或为1或为2或为n。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,19,图4.3 楼层按钮的状态转换图,2019/6/4,湖南科技大学 计算机学院 戴祖雄,20,为了定义与这些事件和状态相联系的状态转换规则,同样也需要一个谓词,它是S(d,e,f),它的定义如下。 S(d,e,f):电梯e停在f层并且移动
12、方向由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。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,21,也就是说,如果在f层请求电梯向d方向运动的楼层按钮处于关闭状态,现在该按钮被按下,并且当时没有正停在f层准备向d方向移动的电梯,则该楼层按钮打开。反之,如果楼层按钮已经打开,且
13、至少有一部电梯到达f层,该部电梯将朝d方向运动,则按钮将关闭。 在讨论电梯按钮状态转换规则时定义的谓词V(e,f),可以用谓词S(d,e,f)重新定义如下: V(e,f)=S(U,e,f)or S(D,e,f)or S(N,e,f),2019/6/4,湖南科技大学 计算机学院 戴祖雄,22,下面定义电梯的三个状态: M(d,e,f):电梯e正沿d方向移动,即将到达的是第f层; S(d,e,f):电梯e停在f层,将朝d方向移动(尚未关门); W(e,f):电梯e在f层等待(已关门)。 其中S(d,e,f)状态已在讨论楼层按钮时定义过,但是,现在的定义更完备一些。 图4.4是电梯的状态转换图。注意
14、,三个电梯停止状态S(U,e,f)、S(N,e,f)和S(D,e,f)已被组合成一个大的状态,这样做的目的是减少状态总数以简化流图。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,23,图4.4 电梯的状态转换图,2019/6/4,湖南科技大学 计算机学院 戴祖雄,24,图4.4中包含了下述三个可触发状态发生改变的事件: DC(e,f):电梯e在楼层f关上门。 ST(e,f):电梯e靠近f层时触发传感器,电梯控制器决定在当前楼层电梯是否停下。 RL:电梯按钮或楼层按钮被按下进入打开状态,登录需求。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,25,最后,给出电梯的状态转换规则。为
15、简单起见,这里给出的规则仅发生在关门之时。 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层准备向上移动,且门已经关闭,则电梯将向上一楼层移动。第二条和第三条规则,分别对应于电梯即将下降或者没有待处理的请求的情况。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,26,4.2.3 评价 有穷状态机方法采用了一种简单的格式来描述规格说明: 当前状态+事件+谓词下个状态 这种形式的规格说明易于书写、易于验证,而且可以比较容易地把它转变成设计或程序代码。事实
16、上,可以开发一个CASE工具把一个有穷状态机规格说明直接转变为源代码。维护可以通过重新转变来实现,也就是说,如果需要一个新的状态或事件,首先修改规格说明,然后直接由新的规格说明生成新版本的产品。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,27,有穷状态机方法比数据流图技术更精确,而且和它一样易于理解。不过,它也有缺点:在开发一个大系统时三元组(即状态、事件、谓词)的数量会迅速增长。此外,和数据流图方法一样,形式化的有穷状态机方法也没有处理定时需求。下节将介绍的Petri网技术,是一种可处理定时问题的形式化方法。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,28,4.3 Pet
17、ri网,4.3.1 基本概念 Petri网包含4种元素:一组位置P、一组转换T、输入函数I以及输出函数O。图4.5举例说明了Petri网的组成。 其中: 一组位置P为P1,P2,P3,P4,在图中用圆圈代表位置。 一组转换T为t1,t2,在图中用短直线表示转换。 ,2019/6/4,湖南科技大学 计算机学院 戴祖雄,29,图4.5 Petri网的组成,2019/6/4,湖南科技大学 计算机学院 戴祖雄,30,两个用于转换的输入函数,用由位置指向转换的箭头表示,它们是: I(t1)=P2,P4 I(t2)=P2 两个用于转换的输出函数,用由转换指向位置的箭头表示,它们是: O(t1)=P1 O(
18、t2)=P3,P3 注意,输出函数O(t2)中有两个P3,是因为有两个箭头由t2指向P3。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,31,更形式化的Petri网结构,是一个四元组C=(P,T,I,O)。其中: P=P1,Pn是一个有穷位置集,n0。 T=t1,tm是一个有穷转换集,m0,且T和P不相交。 I:TP为输入函数,是由转换到位置无序单位组(bags)的映射。 O:TP为输出函数,是由转换到位置无序单位组的映射。 一个无序单位组或多重组是允许一个元素有多个实例的广义集。,2019/6/4,湖南科技大学 计算机学院 戴祖雄,32,Petri网的标记是在Petri网中令牌(to
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 软件工程
链接地址:https://www.31doc.com/p-2909672.html