资源描述：
《《形式化语言》PPT课件》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、第4章形式化说明技术SOFTWAREENGINEERING形式化方法所谓形式化方法：是描述系统性质的，是基于数学的技术，也就是说，如果一种方法有坚实的数学基础，那么它就是形式化的。SOFTWAREENGINEERING4.1概述4.1.1非形式化方法的缺点用自然语言书写的系统规格说明书，可能存在矛盾、二义性、含糊性、不完整性及抽象层次混乱等问题。4.1.2形式化方法的优点简洁准确描述物理现象、对象或动作的结果适合于表示状态，表示“做什么”数学规格说明可以用数学方法验证SOFTWAREENGINEERING4.1.3应用形式化方法的准则1应该选用适当的表示方法（每种形式化语言都有各自
2、的特点）2应该形式化，但不要过分形式化3应该估算成本4应该有形式化方法顾问随时提供咨询5不应该放弃传统的开发方法6应该建立详尽的文档7不应该放弃质量标准8不应该盲目依赖形式化方法9应该测试、测试再测试10应该重用SOFTWAREENGINEERING4.2有穷状态机4.2.1概念一个有穷状态机包括5部分：J是一个有穷的非空状态集；K是一个有穷的非空输入集T是一个从（J-F）×K到J的转换函数S∈J，是一个初始状态F∈J，是终态集SOFTWAREENGINEERING图4.1保险箱的状态转换图SOFTWAREENGINEERINGSOFTWAREENGINEERING保险箱的有穷状态
3、机状态集J：{保险箱锁定，A,B，保险箱解锁，报警}输入集K：{1L,1R,2L,2R,3L,3R}转换函数T：如表4.1初始态S：保险箱锁定终态集F：{保险箱解锁，报警}SOFTWAREENGINEERING4.2.2例子在一幢M层楼的大厦里，用电梯内的和每个楼层的按钮来控制N部电梯的运动。当按下电梯按钮请求电梯在指定楼层停下时，按钮指示灯亮；当电梯到达指定楼层时，指示灯灭。除了大厦的最底层和最高层外，每层楼都有两个按钮分别指示电梯上行和下行。当这两个按钮之一被按下时相应的指示灯亮，当电梯到达此楼层时灯熄灭，电梯向要求的方向移动。当电梯无升降动作时，关门并停在当前楼层。SOFTW
4、AREENGINEERING电梯按钮的状态转换图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层SOFTWAREENGINEERING形式化转换规则V（e,f）：电梯e停在f层EBOFF（e,f）+EBP（e,f）+notV（e,f）→EBON（e,f）EBON（e,f）+EAF（e,f）→EBOFF（e,f）SOFTWAREENGINEERING楼层按钮的状态转换图FB（d,f
5、）：表示f层请求电梯向d方向运动的按钮。有两个状态：--FBON（d,f）：楼层按钮（d,f）打开--FBOFF（d,f）：楼层按钮（d,f）关闭两个事件：--FBP（d,f）：楼层按钮（d,f）被按下--EAF（1……n,f）：电梯1或……或n到达f层SOFTWAREENGINEERING形式化转换规则S（d，e，f）：电梯e停在f层并且移动方向由d确定为向上（d=U）或向下（d=D）或待定（d=N）。FBOFF（d,f）+FBP（d,f）+notS（d，1……n，f）→FBON（d,f）FBON（d,f）+EAF（1……n,f）+S（d，1……n，f）→FBOFF（d,f）其中
6、d=UorDSOFTWAREENGINEERING电梯的状态转换电梯的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：电梯按钮或楼层按钮被按下进入打开状态SOFTWAREENGINEERING图4.4电梯的状态转换图SOFTWAREENGINEERING形式化转换规则S（U，e，f）+DC（e，f）→M（U，e，f+1）S（D，
7、e，f）+DC（e，f）→M（D，e，f-1）S（N，e，f）+DC（e，f）→W（e，f）SOFTWAREENGINEERING4.3Petri网4.3.1概念（描述并发活动、处理定时需求）四元组C=（P,T,I,O）P={P1,……,Pn}是一个有穷位置集，n≥0T={t1,……,tm}是一个有穷转换集，m≥0I：T→P∞为输入函数，是由转换到位置无序单位组的映射O：T→P∞为输出函数，是由转换到位置无序单位组的映射一个无序单位组或多重组是允许一个元素有多个实例的
