《形式化语言》PPT课件

单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,*,SOFTWARE ENGINEERING,*,第4章 形式化说明技术,SOFTWARE ENGINEERING,形式化方法,所谓形式化方法：是描述系统性质的，是基于数学的技术，也就是说，如果一种方法有坚实的数学基础，那么它就是形式化的。,SOFTWARE ENGINEERING,4.1概述,非形式化方法的缺点,用自然语言书写的系统规格说明书，可能存在矛盾、二义性、含糊性、不完整性及抽象层次混乱等问题。,形式化方法的优点,简洁准确描述物理现象、对象或动作的结果,适合于表示状态，表示“做什么”,数学规格说明 可以用数学方法验证,SOFTWARE ENGINEERING,应用形式化方法的准则,1 应该选用适当的表示方法（每种形式化语言都有各自的特点）,2 应该形式化，但不要过分形式化,3 应该估算成本,4 应该有形式化方法顾问随时提供咨询,5 不应该放弃传统的开发方法,6 应该建立详尽的文档,7 不应该放弃质量标准,8 不应该盲目依赖形式化方法,9 应该测试、测试再测试,10 应该重用,SOFTWARE ENGINEERING,4.2有穷状态机,概念,一个有穷状态机包括5部分：,J是一个有穷的非空状态集；,K是一个有穷的非空输入集,T是一个从（J-F）K到J的转换函数,SJ，是一个初始状态,FJ，是终态集,SOFTWARE ENGINEERING,图4.1保险箱的状态转换图,SOFTWARE ENGINEERING,SOFTWARE ENGINEERING,保险箱的有穷状态机,状态集J：保险箱锁定，A,B，保险箱解锁，报警,输入集K：1L,1R,2L,2R,3L,3R,转换函数T：如表4.1,初始态S：保险箱锁定,终态集F：保险箱解锁，报警,SOFTWARE ENGINEERING,例子,在一幢M层楼的大厦里，用电梯内的和每个楼层的按钮来控制N部电梯的运动。当按下电梯按钮请求电梯在指定楼层停下时，按钮指示灯亮；当电梯到达指定楼层时，指示灯灭。除了大厦的最底层和最高层外，每层楼都有两个按钮分别指示电梯上行和下行。当这两个按钮之一被按下时相应的指示灯亮，当电梯到达此楼层时灯熄灭，电梯向要求的方向移动。当电梯无升降动作时，关门并停在当前楼层。,SOFTWARE ENGINEERING,电梯按钮的状态转换图,EB（e,f）：表示按下电梯e内的按钮，并请求到f层去。有两个状态：,-EBON（e,f）：电梯按钮（e,f）打开,-EBOFF（e,f）：电梯按钮（e,f）关闭,两个事件：,-EBP（e,f）：电梯按钮（e,f）被按下,-EAF（e,f）：电梯e到达f层,SOFTWARE ENGINEERING,形式化转换规则,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）,SOFTWARE ENGINEERING,楼层按钮的状态转换图,FB（d,f）：表示f层请求电梯向d方向运动的按钮。有两个状态：,-FBON（d,f）：楼层按钮（d,f）打开,-FBOFF（d,f）：楼层按钮（d,f）关闭,两个事件：,-FBP（d,f）：楼层按钮（d,f）被按下,-EAF（1n,f）：电梯1或或n到达f层,SOFTWARE ENGINEERING,形式化转换规则,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,SOFTWARE ENGINEERING,电梯的状态转换,电梯的3个状态：,M（d，e，f）：电梯e沿着d方向移动，即将到达的是第f层,S（d，e，f）：电梯e停在f层，将朝d方向移动（尚未关门）,W（e，f）：电梯e在f层等待（已关门）,电梯的3个事件：,DC（e，f）：电梯e在楼层f关上门,ST（e，f）：电梯e靠近f层时触发传感器，电梯控制器决定在当前楼层电梯是否停下,RL：电梯按钮或楼层按钮被按下进入打开状态,SOFTWARE ENGINEERING,图4.4电梯的状态转换图,SOFTWARE ENGINEERING,形式化转换规则,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）,SOFTWARE ENGINEERING,4.3 Petri网,概念（描述并发活动、处理定时需求）,四元组C=（P,T,I,O）,P=P,1,P,n,是一个有穷位置集，n0,T=t,1,t,m,是一个有穷转换集，m0,I：T,P,为输入函数，是由转换到位置无序单位组的映射,O：T,P,为输出函数，是由转换到位置无序单位组的映射,一个无序单位组或多重组是允许一个元素有多个实例的广义集,SOFTWARE ENGINEERING,图4.5 Petri网的组成,图4.6带标记的Petri网,SOFTWARE ENGINEERING,图4.7图4.6的Petri网在转换t1被激发后的情况,图4.8图4.7的Petri网在转换t2被激发后的情况,SOFTWARE ENGINEERING,图4.10 Petri网表示的电梯按钮,SOFTWARE ENGINEERING,例子,1.电梯按钮,图4.10 Petri网表示的电梯按钮,SOFTWARE ENGINEERING,图4.11Petri网表示楼层按钮,2.楼层按钮,SOFTWARE ENGINEERING,4.4 Z语言,简介,1.给定的集合,2.状态定义,图4.12Z格S的格式,SOFTWARE ENGINEERING,图4.13Z格Button_State,SOFTWARE ENGINEERING,3.初始状态4.操作,图4.14操作Push_Button的Z规格说明,SOFTWARE ENGINEERING,图4.15操作Floor_Arrival的Z规格说明,SOFTWARE ENGINEERING,将事物的状态和行为用,数学符号,形式化表达的,语言,，为编写,计算机程序,和验证计算机程序的正确性提供依据，是,软件工程,中,编码,之前的规格说明语言。,Z语言是一种以一阶谓词演算为主要理论基础的规约语言,是一种功能性语言。形式化描述语言Z指的是著名数学家Zermelo，它是目前使用最广泛的一种形式化描述语言，在软件产业的一些大型项目中已经获得成功的应用，Z以带等词的一阶谓词逻辑ZF（Zermelo-Fraenkel，蔡梅罗-弗兰科尔）公理集合论为主要数学基础。在Z中有两种语言：数学语言和模式（Schema）语言。数学语言用来描述系统的各种特征：对象及其之间的关系。模式语言是一种半图形化的语言，它用来构造、组织形式化说明的描述、整理、封装信息块并对其命名以便可以重用这些信息块。通常，形式化说明的可读性都不太好，但由于Z采用半图形化的模式语言，能用一种比较直观、有条理的方式来表达形式化说明，这就改善了可读性。,Z语言是由牛津大学程序设计研究小组开发的一种形式语言，之后该小组与IBM的Hursley实验室合作，将Z语言用于IBM客户信息控制系统(Customer Information and Control System,CICS)的开发，使得最终的产品质量得到了全面的提高，所监测出的错误数量大大减少，并且整体开发费用降低了9%。在ISO指导下的国际标准化Z工作与2002年完成。,SOFTWARE ENGINEERING,