软件工程导论-软件工程-沈师(第4章).ppt

第4章：形式化说明技术,1.非形式化方法：自然语言描述2.半形式化方法：数据流图或实体联系图3.形式化方法：基于数学技术描述,4.1 概述,4.1.1 非形式化方法的缺点 自然语言书写的系统规格说明书可能存在：1）矛盾；2）二义性；如：“操作员标识由操作员姓名和密码组成，密码由6位数字构成，当操作员登陆系统时它被存储在注册文件中。”3）含糊性；4）不完整性；5）抽象层次混乱。,4.1.2 形式化方法的优点（1）数学是理想的建模工具，适合于表示系统状态和描述系统需求；（2）用数学表达的需求可在不同开发阶段平滑过渡。（3）数学提供了高层确认的手段,4.1.3 应用形式化方法的准则（1）选择合适的形式化方法；（2）应该形式化，但不要过分形式化；（3）应该估算成本；（4）应该有形式化方法顾问随时提供咨询；（5）不应该放弃传统的开发方法；（6）应该建立详尽的文档；（7）不应该放弃质量标准；（8）不应该盲目依赖形式化方法；（9）应该测试、测试再测试；（10）应该重用；,4.2 有穷状态机法（FSM）,4.2.1 概念,锁的三个位置：1、2、3；转盘可向左（L）或右（R）；锁密码：1L、3R、2L,一个有穷状态机包括5部分：1）状态集J：保险箱锁定，A，B，保险箱解锁，报警 2）输入集K：1L,1R,2L,2R,3L,3R 3）转换函数T，如表4.1 4）初始态S：保险箱锁定 5）终态集F：保险箱解锁，报警 更形式化的术语：一个有穷状态机可表示一个为5元组（J,K,T,S,F）,状态转换形式：当前状态【菜单】事件【所选择的项】下个状态加入谓词集P，把系统扩展成一个6元组后：当前状态【菜单】事件【所选择的项】谓词下个状态,计算机系统中每个菜单驱动的用户界面都是一个有穷状态机的实现。,定义状态：（1）M(d,e,f)：电梯e正沿d方向移动，即将到达第f层楼。（2）S(d,e,f)：电梯e停在f层楼，将朝d方向移动（未关门）。（3）W(e,f)：电梯e在f层等待（已关门）。（4）DC(e,f)：电梯e在楼层f关上门。（5）ST(e,f)：电梯e靠近f层时触发传感器，电梯控制器决定在当前楼层是否停下。（6）RL：电梯按钮或楼层按钮被按下进入打开状态,4.2.2 例子:电梯的状态转换,电梯状态转换规则：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 评价 有穷状态机描述规格说明：当前状态事件谓词=下个状态 易于书写、验证、转变成设计或程序代码。,有穷状态机方法比数据流图技术更精确，一样易于理解。但不能处理定时需求。,4.3 Petri网,4.3.1 概念,Petri网包含4种元素：一组位置P、一组转换T、输入函数I以及输出函数O。图4.5举例说明了Petri网的组成。,Petri网包含4种元素：1）一组位置P，上例 PP1,P2,P3,P4 2）一组转换T，上例 Tt1,t2 3）输入函数I，上例 I（t1）=P2,P4 I（t2）=P2 4）输出函数O，上例O（t1）=P1 O（t2）=P3,P3更形式化的Petri网结构，是一个4元组（P，T，I，O）,权标向量（1，2，0，1）,注意：当每个输入位置所拥有的权标数大于等于从该位置到转换的线数时，就允许转换。当t1被激发时，P2和P4上各有一个权标被移出，而P1上只能增加一个权标,权标向量（2，1，0，0）,权标向量（2，0，2，0）,更形式化地：标记 M：P0,1,2,Petri网成为一个5元组（P，T，I，O，M）,对Petri网的一个重要扩充是加入禁止线：,注意：当每个输入线上至少有一个权标，而禁止线上没有权标的时候，相应的转换才是允许的,4.3.2 例子1.电梯按钮,EBf 电梯中楼层 f 的按钮；Fg 楼层g；Ff 楼层 f。,2.楼层按钮,FBfu 第 f 楼层向上按钮；FBfd 第 f 楼层向下按钮；,用Z语言描述的、最简单的形式化规格说明含有下述4个部分：给定的集合、数据类型及常数。状态定义。初始状态。操作。,4.4 Z语言 4.4.1 简介,1.给定的集合一个Z规格说明从一系列给定的初始化集合开始。所谓初始化集合就是不需要详细定义的集合，这种集合用带方括号的形式表示。对于电梯问题，给定的初始化集合称为Button，即所有按钮的集合，因此，Z规格说明开始于：Button2.状态定义一个Z规格说明由若干个“格(schema)”组成，每个格含有一组变量说明和一系列限定变量取值范围的谓词。例如，格S的格式如图4.12所示。,图4.12 Z格S的格式,在电梯问题中，Button有4个子集，即floor_buttons(楼层按钮的集合)、elevator_buttons(电梯按钮的集合)、buttons(电梯问题中所有按钮的集合)以及pushed(所有被按的按钮的集合，即所有处于打开状态的按钮的集合)。,图4.13描述了格Button_State，其中，符号P表示幂集(即给定集的所有子集)。约束条件声明，floor_buttons集与elevator_buttons集不相交，而且它们共同组成buttons集(在下面的讨论中并不需要floor_buttons集和elevator_buttons集，把它们放于图4.13中只是用来说明Z格包含的内容)。,图4.13Z格Button_State,3.初始状态抽象的初始状态是指系统第一次开启时的状态。对于电梯问题来说，抽象的初始状态为：Button_Init Button_Statepushed=上式表示，当系统首次开启时pushed集为空，即所有按钮都处于关闭状态。4.操作如果一个原来处于关闭状态的按钮被按下，则该按钮开启，这个按钮就被添加到pushed集中。图4.14定义了操作Push_Button(按按钮)。,图4.14操作Push_Button的Z规格说明,操作的谓词部分，包含了一组调用操作的前置条件，以及操作完全结束后的后置条件。如果前置条件成立，则操作执行完成后可得到后置条件。但是，如果在前置条件不成立的情况下调用该操作，则不能得到指定的结果(因此结果无法预测)。假设电梯到达了某楼层，如果相应的楼层按钮已经打开，则此时它会关闭；同样，如果相应的电梯按钮已经打开，则此时它也会关闭。也就是说，如果“button?”属于pushed集，则将它移出该集合，如图4.15所示(符号“”表示集合差运算)。,图4.15操作Floor_Arrival的Z规格说明,已经在许多软件开发项目中成功地运用了Z语言，目前，Z也许是应用得最广泛的形式化语言，尤其是在大型项目中Z语言的优势更加明显。Z语言之所以会获得如此多的成功，主要有以下几个原因：(1)可以比较容易地发现用Z写的规格说明的错误，特别是在自己审查规格说明，及根据形式化的规格说明来审查设计与代码时，情况更是如此。(2)用Z写规格说明时，要求作者十分精确地使用Z说明符。由于对精确性的要求很高，从而和非形式化规格说明相比，减少了模糊性、不一致性和遗漏。,4.4.2 评价,(3)Z是一种形式化语言，在需要时开发者可以严格地验证规格说明的正确性。(4)虽然完全学会Z语言相当困难，但是，经验表明，只学过中学数学的软件开发人员仍然可以只用比较短的时间就学会编写Z规格说明，当然，这些人还没有能力证明规格说明的结果是否正确。(5)使用Z语言可以降低软件开发费用。虽然用Z写规格说明所需用的时间比使用非形式化技术要多，但开发过程所需要的总时间却减少了。,(6)虽然用户无法理解用Z写的规格说明，但是，可以依据Z规格说明用自然语言重写规格说明。经验证明，这样得到的自然语言规格说明，比直接用自然语言写出的非形式化规格说明更清楚、更正确。使用形式化规格说明是全球的总趋势，过去，主要是欧洲习惯于使用形式化规格说明技术，现在越来越多的美国公司也开始使用形式化规格说明技术。,小结 基于数学的形式化说明技术，目前还没有在软件产业界广泛应用；应该把形式化方法与传统方法有机结合。,第三、四章练习题,填空题：1、需求分析过程应该建立3种模型，它们分别是（）、（）和（）。2、按照形式化的程度，可以把软件工程使用的方法划分成（）、（）和（）等3类。3、验证软件需求应该从以下4个方面进行验证，即（）、（）、（）和（）。4、需求分析的任务包括系统综合要求、数据要求、导出逻辑模型和修正系统开发计划等。其中常见的接口需求有：用户接口需求、（）、（）和通信接口需求等等。,4、需求分析的任务包括（）、（）、（）和修正系统开发计划等。5、需求分析的任务包括系统综合要求、数据要求、导出逻辑模型和修正系统开发计划等。其中设计约束或实现约束常见的有：（）、工具和语言约束、（）、应该使用的标准和应该使用的（）等。,判断题：1、形式化方法有许多优点，因此在实际软件工作中应该依赖形式化方法来保证开发出的软件绝对正确和降低由于设计缺陷产生的维护代价。（）2、可以用形式化方法证明软件的需求和设计的正确性和合理性，因此，如果为了降低软件的测试成本和改正错误代价等，可以不用对软件进行测试，也可以保证软件的质量和降低开发成本等软件工程的目标。（）,名词解释：1、实体-联系图（ER图）2、状态转换图3、IPO图4、Petri网简答题：1、简述需求分析的原则。2、简述形式化方法的准则。3、课后题P73，第1、2题；P89，第1、2题,