软件工程课件老师.pptxVIP

大连理工大学软件学院软件工程

2025/3/5大连理工大学软件学院2第四章形式化说明技术放弃美丽的女人让人心碎。自然语言：矛盾、二义性、含糊形式化表示：准确、清晰非形式化：自然语言半形式化：DFD、E-R图形式化：坚实的以数学为基础的表示方法

2025/3/5大连理工大学软件学院3第四章形式化说明技术4.1概述4.2有穷状态机4.3Petri网4.4Z语言

2025/3/5大连理工大学软件学院44.1概述4.1.1非形式化方法的缺点矛盾：相互冲突的陈述二义性：读者可以用不同的方式理解的陈述含糊不完整抽象层次混乱：非常抽象的陈述中混进了一些关于细节的低层次陈述。

2025/3/5大连理工大学软件学院54.1概述4.1.2形式化方法的优点把数学引入软件开发过程，形成基于数学的形式化方法。数学最有用的一个性质是，能够简洁准确地描述物理现象、对象或动作的结果，因此是理想的建模工具。在软件开发过程中使用数学，可以在不同的软件工程活动之间平滑地过渡。提供了高层确认的手段。

2025/3/5大连理工大学软件学院64.1概述4.1.3应用形式化方法的准则应该选用适当的表示方法应该形式化，但不要过分形式化应该估算成本应该有形式化方法顾问随时提供咨询不应该放弃传统的开发方法应该建立详尽的文档不应该放弃质量标准不应该盲目依赖形式化方法应该测试、测试再测试应该重用

2025/3/5大连理工大学软件学院74.2有穷状态机4.2.1概念一个保险箱上装了一个复合锁，锁有3个位置，分别标记为1、2、3，转盘可向左（L）或向右（R）转动。这样，任何时刻转盘都有6种可能的运动，即1L、1R、2L、2R、3L、3R。保险箱的组合密码是1L、3R、2L，转盘的任何其他运动都将引起报警。

2025/3/5大连理工大学软件学院84.2有穷状态机图4.1保险箱的状态转换图

2025/3/5大连理工大学软件学院94.2有穷状态机

2025/3/5大连理工大学软件学院104.2有穷状态机一个有穷状态机包括5个部分：状态集J：{保险箱锁定，A，B，保险箱解锁， 报警}输入集K：{1L、1R、2L、2R、3L、3R}转换函数T：如表4.1所示初始态S：保险箱锁定终态集F：{保险箱解锁，报警}

2025/3/5大连理工大学软件学院114.2有穷状态机一个有穷状态机可以表示为一个5元组（J，K，T，S，F），其中：J是一个有穷的非空状态集；K是一个有穷的非空输入集；T是一个从（J-F）*K到J的转换函数；S∈J，是一个初始状态；FJ，是终态集一个有穷状态机可以表示为一个5元组（J，K，T，S，F），其中：J是一个有穷的非空状态集；K是一个有穷的非空输入集；T是一个从（J-F）*K到J的转换函数；S∈J，是一个初始状态；FJ，是终态集

2025/3/5大连理工大学软件学院124.2有穷状态机加入谓词集P，把有穷状态机扩展为一个6元组，其中每个谓词都是系统全局状态Y的函数。则转换函数T：（J-F）*K*PJ

2025/3/5大连理工大学软件学院134.2有穷状态机4.2.2例子电梯按钮EB（e，f）：按下电梯e内的按钮并请求到f层去状态：EBON（e，f）：电梯按钮（e，f）打开EBOFF（e，f）：电梯按钮（e，f）关闭事件EBP（e，f）：电梯按钮（e，f）被按下EAF（e，f）：电梯到达f层谓词V（e，f）：电梯e停在f层

2025/3/5大连理工大学软件学院144.2有穷状态机图4.2电梯按钮的状态转换图

2025/3/5大连理工大学软件学院154.2有穷状态机楼层按钮FB（d，f）：f层请求电梯向d方向运动的按钮状态：FBON（d，f）：楼层按钮（d，f）打开FBOFF（d，f）：楼层按钮（d，f）关闭事件FBP（d，f）：楼层按钮（d，f）被按下EAF（1…n，f）：电梯1或…或n到达f层谓词S（d，e，f）：电梯e停在f层并且移动方向由d确定

2025/3/5大连理工大学软件学院164.2有穷状态机图4.3楼层按钮的状态转换图

2025/3/5大连理工大学软件学院174.2有穷状态机电梯状态M（d，e，f）：电梯e正沿d方向移动，即将到达的是第f层S（d，e，f）：电梯e停在f层，将朝d方向移动（尚未关门）W（e，f）：电梯e在f层等待（已关门）事件DC（e，f）：电梯e在楼层f关上门ST（e，f）：电梯e靠近f层时触发传感器，电梯控制器决定在当前楼层电梯是否停下RL：电梯按钮或楼层按钮被按下进入打开状态，登录