《软件工程导论第4章形式化说明技术ppt课件》由会员分享，可在线阅读，更多相关《软件工程导论第4章形式化说明技术ppt课件（59页珍藏版）》请在金锄头文库上搜索。
1、 软件工程导论软件工程导论第第5 5版版 普通高校本科计算机专业特征教材精选张海藩 编著第第4章章 方式化阐明技术方式化阐明技术主要内容4.1 方式化阐明技术4.2 有穷形状机4.3 Petri网4.4 Z言语教学重点有穷形状机、 Petri网。4.1方式化阐明技术概述方式化阐明技术概述方式化方法的引入在传统的软件开发过程中，人们普遍采用各种非方式化的图形工具和文字符号工具，并按照一定的设计原那么和有序步骤，同时手工或辅助编写有关设计文档。软件工程的实际阐明，用户需求规格阐明的质量对于后续的软件开发过程是非常重要的。系统分析人员根据用户需求，为目的软件系统创建了需求规格阐明。设计和编程人员根据
2、这个需求规格阐明进展系统构造和模块设计及编码。软件测试及验收人员那么根据这个需求规格阐明验证目的系统。4.1 续续方式化方法的引入20世纪80年代中期以来，一种公用于需求规格阐明的方式规格阐明言语应运而生。方式规格阐明言语抑制了自然言语和程序设计言语的缺乏，运用方式化、规范化的数学实际，严厉定义软件系统“做什么的方式语义模型，并支持自动程序转换系统将需求规格阐明的语义模型转换为可执行代码。由此产生的软件方式开发方法正日益遭到各国软件界的注重。4.1 续续软件需求规格阐明方法分类非方式化方法用自然言语进展描画的方式。半方式化方法用数据流图、实体-联络图、形状转换图、IPO图等建立模型的方法。方式
3、化方法利用方式化、规范化的数学推演的方式。4.1 续续非方式化方法的缺陷矛盾一组相互冲突的陈说。二义性读者可以用不同方式了解的陈说。模糊性没有给出任何有用信息的笼统的陈说。不完好性信息的描画过程中遗留了某个方面。笼统层次混乱在非常笼统的陈说中混进了一些关于细节的低层陈说。4.1 续续方式化方法的主要思想方式化需求分析方法的主要思想，是利用方式化规格阐明言语严厉地定义用户需求，并采用数学推演的方法证明需求定义的性质。从某种意义上讲，方式化方法是抑制需求分析阶段中主要困难不准确性、不一致性和不完全性的有效途径。方式化规格阐明言语包括：严厉的语法定义、严厉的语义定义以及一系列的数学推演规那么。4.1
4、 续续方式化方法的主要思想规格阐明言语的语法普通基于集合论、数理逻辑或代数学。规格阐明言语的语义是其一切语法符号的意义的数学描画。方式化规格阐明言语的推演规那么普通与其数学根底和语义定义方法亲密相关。规那么必需在规格阐明言语的语义系统中可证。因此，可以以为规那么是派生的语义定义，它们可以直接运用于软件规格阐明的性质证明并简化推演过程。4.1 续续方式化方法的分类方式化方法是运用严厉的方式符号和数学方法定义或描画目的软件系统需求规格阐明的一种方法。根据对需求规格阐明的定义方式分类：面向模型的方式方法。又称基于形状描画的方式方法。根本思想：利用域、元组、集合、序列、映射、包等这些知特性的数学笼统概
5、念来为目的软件系统的形状特征和行为特征构造方式语义模型。语义模型就作为目的软件系统需求规格的方式阐明。主要代表：VDM方法维也纳开发方法、Z言语方法等。代数构造方式方法。目的软件系统的需求规格阐明提供一些特殊的构造机制，并以代数构造方式描画目的系统的构造、功能。4.1 续续软件方式开发方法将方式化方法运用于软件开发过程称为软件方式开发方法。首先，在需求分析阶段的信息搜集和信息分析两项任务中，采用方式化的规格阐明言语构造目的软件系统严厉的方式需求规格阐明即方式语义。然后，以该方式需求规格阐明为起点，借助相应的方式开发支持工具辅助实现目的软件系统。目前，除了在软件设计、编码阶段采用方式方法外，还在
6、开展软件系统方式化测试的研讨任务。4.1 续续方式化方法的优点对系统的需求规格阐明描画准确、定义完好。方式化的需求规格阐明有利于系统的设计与实现。软件实现的正确性可以方式验证，确保软件质量。4.1 续续方式化方法的缺陷方式化的需求规格阐明可读性差。对软件设计人员要求较高，需进展更专业化的培训。只适用于能静态定义的软件系统，它无法定义动态系统行为。方式化的规格阐明方式语义模型的正确性验证费时费力，目前还不能简化或自动化。方式方法目前还缺乏软件工程环境的支持。4.1 续续运用方式化方法的准那么应该选用适宜当前工程的方式化阐明技术。应该方式化，但不要过分方式化。应该估算本钱。应该有方式化方法顾问随时
7、提供咨询。不应该放弃传统的开发方法。应该建立详尽的文档。不应该放弃质量规范。不应该盲目依赖方式化方法。应该进展严厉的审查、验证。应该重用。4.1 续续方式化方法近年来的开展方式化方法与图形言语机制相结合。为图形言语机制赋予方式化的语法和语义，从而兼具了图形表示的直观、简约，以及方式化方法的严谨、准确等优点。用CASE工具支持方式化软件开发。CASE工具不仅可以简化需求分析和需求描画任务，而且还可以利用自动定理证明技术协助分析人员验证软件规格阐明的数学性质。实际证明，这两条技术途径对于抑制方式化方法的主要缺陷是行之有效的。因此，它们仍将在方式化方法的未来开展中发扬重要作用。4.2 有穷形状机有穷
8、形状机定义一个有穷形状机可以表示为一个5元组(J，K，T，S，F)，其中：J是一个有穷的非空形状集；K是一个有穷的非空输入集；T是一个从(J-F)K到J的转换函数；SJ，是一个初始形状；FJ，是终态集。4.2 续续例1一个保险箱上装了一个复合锁，锁有三个位置，分别标志为1、2、3，转盘可向左(L)或向右(R)转动。这样，在恣意时辰转盘都有6种能够的运动，即1L、1R、2L、2R、3L和3R。保险箱的组合密码是1L、3R、2L，转盘的任何其他运动都将引起报警。4.2 续续例1保险箱的形状转换情况4.2 续续例1保险箱的形状转换表4.14.2 续续例1保险箱例子的有穷形状机描画形状集J：保险箱锁定
9、，A，B，保险箱解锁，报警。输入集K：1L，1R，2L，2R，3L，3R。转换函数T：如表4.1所示。初始态S： 保险箱锁定。终态集F： 保险箱解锁，报警。4.2 续续扩展定义一个有穷形状机可以表示为一个5元组(J，K，T，S，F)，其中：J是一个有穷的非空形状集；K是一个有穷的非空输入集；P是一个谓词集；T是一个从(J-F)KP到J的转换函数；SJ，是一个初始形状；FJ，是终态集。4.2 续续例2一个菜单的显示和一个形状相对应，键盘输入或用鼠标选择一个图标是使系统进入其他形状的一个事件。转换规那么：当前形状菜单+事件所选择的项下个形状。当前形状菜单+事件所选择的项+谓词下个形状。4.2 续续
10、例3：电梯系统自然言语描画 在一幢m层的大厦中需求一套控制n部电梯的产品，要求这n部电梯按照约束条件C1，C2和C3在楼层间挪动。C1：每部电梯内有m个按钮，每个按钮代表一个楼层。当按下一个按钮时该按钮指示灯亮，同时电梯驶向相应的楼层，到达按钮指定的楼层时指示灯熄灭。C2：除了大厦的最低层和最高层之外，每层楼都有两个按钮分别恳求电梯上行和下行。这两个按钮之一被按下时相应的指示灯亮，当电梯到达此楼层时灯熄灭，电梯向要求的方向挪动。C3：当对电梯没有恳求时，它关门并停在当前楼层。4.2 续续例3：电梯系统电梯按钮的形状转换图转换函数：EBe，f ：按下电梯e内的按钮并恳求去f层。形状EBON(e,
11、f)：电梯按钮(e,f)翻开EBOFF(e,f)：电梯按钮(e,f)封锁4.2 续续例3：电梯系统事件EBPe，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)V(e,f)=S(U,e,f)or S(D,e,f)or S(N,e,f)4.2 续续例3：电梯系统楼层按钮的形状转换图转换函数：FBd，f ：f层恳求电梯向d方向运动的按钮。形状FBON(d,f)：楼层按钮(d,f)翻开F
12、BOFF(d,f)：楼层按钮(d,f)封锁4.2 续续例3：电梯系统事件FBPd，f ：楼层按钮 d，f 被按下EAF1n，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,1n,f)FBON(d,f)FBON(d,f)+EAF(1n,f)+S(d,1n,f)FBOFF(d,f)其中，d=UorD。4.2 续续例3：电梯系统电梯的3个形状：M(d,e,f)：电梯e正沿d方向挪动，即将到达的是第f层S(d,e,f)：电梯e停
13、在f层，将朝d方向挪动(尚未关门)W(e,f)：电梯e在f层等待(已关门)4.2 续续例3：电梯系统电梯3个事件：DC(e,f)：电梯e在楼层f关上门ST(e,f)：电梯e接近f层时触发传感器，电梯控制器决议在当前楼层电梯能否停下RL：电梯按钮或楼层按钮被按下进入翻开形状，登录需求4.2 续续例3：电梯系统电梯的形状转换规那么仅发生在关门之时：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.2 续续评价格式：当前形状+事件+谓词下个形状
14、CASE工具把一个有穷形状机描画的规格阐明直接转变为源代码。4.3 Petri网网Petri网Petri网的思想是1962年由Carl Adam Petri提出来的。最初是一种表达异步系统的控制规那么的图形表示法，如今广泛运用于硬件与软件系统的开发中。Petri网适用于描画与分析相互独立、协同操作的处置系统，即并发执行的处置系统。4.3 续续Petri网根本概念 Petri网简称PNGPetri Net Graph，是一种有向图，包含四种元素。位置P：符号为“，它用来表示系统的形状。转换T：用短竖线表示，代表系统中的事件。输入函数I：用由位置指向转换的箭头表示。输出函数O：用由转换指向位置的箭
15、头表示。4.3 续续Petri网的组成4.3 续续Petri网的组成位置P：P1，P2，P3，P4转换T：t1，t2输入函数：I(t1)=P2，P4 I(t2)=P2输出函数：O(t1)=P1 O(t2)=P3，P34.3 续续Petri网方式化定义Petri网是一个四元组C=P，T，I，O，其中，P=P1，Pn是一个有穷位置集，n0。T=t1，tm是一个有穷转换集，m0，且T和P不相交。I：TP为输入函数，是由转换到位置无序单位组(bags)的映射。O：TP为输出函数，是由转换到位置无序单位组的映射。4.3 续续带标志的Petri网Petri网的标志是在Petri网中权标的分配。标志：阐明系
16、统当前处于什么形状的标志。通常，当每个输入位置所拥有的权标数大于等于从该位置到转换的线数时，就允许转换。Petri网中权标总数不固定。Petri网具有非确定性。4.3 续续带标志的Petri网标志：(1，2，0，1)4.3 续续带标志的Petri网t1被激发。标志： (2，1，0，0)4.3 续续带标志的Petri网t1，t2 被激发。标志： (2，0，2，0)4.3 续续形状迁移当激发产生的结果有几个时，将随机地选择一个结果输出，并把作为结果的位置的形状加上权标。权标在PNG中的游动，称为“形状的迁移。4.3 续续Petri网方式化定义带有标志的Petri网成为一个五元组(P，T，I，O，M
17、)。Petri网C=(P，T，I，O)中的标志M，是由一组位置P到一组非负整数的映射：M：P0，1，2，4.3 续续含制止线的Petri网制止线：用一个小圆圈而不是用箭头标志的输入线。通常，当每个输入线上至少有一个权标，而制止线上没有权标的时候，相应的转换才是允许的。4.3 续续例1：电梯系统自然言语描画 在一幢m层的大厦中需求一套控制n部电梯的产品，要求这n部电梯按照约束条件C1，C2和C3在楼层间挪动。C1 ：每部电梯内有m个按钮，每个按钮代表一个楼层。当按下一个按钮时该按钮指示灯亮，同时电梯驶向相应的楼层，到达按钮指定的楼层时指示灯熄灭。C2 ：除了大厦的最低层和最高层之外，每层楼都有两
18、个按钮分别恳求电梯上行和下行。这两个按钮之一被按下时相应的指示灯亮，当电梯到达此楼层时灯熄灭，电梯向要求的方向挪动。C3 ：当对电梯没有恳求时，它关门并停在当前楼层。4.3 续续例1：电梯系统电梯按钮4.3 续续例1：电梯系统楼层按钮4.3 续续例2：环形铁路有一个环形铁路，在A站与B站之间是单轨，在某一个时辰只能走一列火车，但A站与B站都是双向运转的。上行和下行列车交替行驶。4.3 续续例2：环形铁路4.3 续续例3：进程同步机制设在一个多义务系统中有两个进程PR1 和PR2，它们是用了一个公共资源R。该资源在系统运转的某一个时辰只能为一个进程所占有。为理处理两个进程在运转中能够会同时恳求资
19、源的矛盾，要用原语LOCK对资源加锁和UNLOCK对资源解锁控制R的运用，保证进程间的同步。4.3 续续例3：进程同步机制4.4 Z言语言语Z言语用Z言语描画的、最简单的方式化规格阐明含有下述4个部分：给定的集合、数据类型及常数。形状定义。初始形状。操作。运用Z言语需求具备集合论、函数、数理逻辑等方面的知识。4.4 续续给定的集合一个Z规格阐明从一系列给定的初始化集合开场。初始化集合：不需求详细定义的集合。电梯系统：给定的初始化集合称为Button；Z规格阐明开场于：Button4.4 续续形状定义一个Z规格阐明由假设干个“格组成；每个格含有一组变量阐明和一系列限定变量取值范围的谓词。Z格-S
20、的格式4.4 续续形状定义电梯系统Button集合有4个子集：floor_buttons：楼层按钮的集合。elevator_buttons：电梯按钮的集合。buttons：电梯问题中一切按钮的集合。pushed：一切处于翻开形状的按钮的集合。约束条件： floor_buttons集与elevator_buttons集不相交 floor_buttons集与elevator_buttons集共同组成buttons集。4.4 续续形状定义电梯系统P：给定集的一切子集，即幂集4.4 续续初始形状笼统的初始形状是指系统第一次开启时的形状。电梯系统：Button_InitButton_Statepushed=4.4 续续操作电梯系统代表一个格被用在另一个格中代表一个格被用在另一个格中 ？代表？代表输入入变量量 ！代表！代表输出出变量量4.4 续续操作电梯系统代表一个格被用在另一个格中代表一个格被用在另一个格中 ？代表？代表输入入变量量 ！代表！代表输出出变量量 代表集合差运算代表集合差运算4.4 续续评论Z言语优点容易发现用z写的规格阐明中的错误。对于准确度的要求减少了模糊性、不一致性和脱漏的几率。在需求时可严厉地验证规格阐明的正确性。学习编写Z规格阐明不难。可降低软件开发费用。Z规格阐明转换为自然言语规格阐明，更容易保证正确性和明晰性。
