软件工程形式化说明技术.ppt

1,第4章 形式化说明技术,4.1 概述 4.2 有穷状态机 4.3 Petri网 4.4 Z语言 4.5 小结,2,关于形式化方法,形式化方法是有争议的。它们的支持者宣称：它们可以引发软件开发的革命。而批评者认为：这是困难和不可能的。同时，对于大多数人来说，对形式化方法是如此不熟悉，以至难于判断这些争论。,3,形式化的程序,非形式化方法：自然语言描述 半形式化方法（欠形式化方法）：数据流图、实体-联系图 形式化方法：一种方法有坚实的数学基础,4,非形式化方法的缺点,二义性：操作员名和口令 可能存在矛盾：监控温度/往往距离很远 含糊性：由雷达操作员使用的系统界面应该是用户友好的 不完整性：传感器 抽象层次混乱：系统的目的是跟踪仓库中的库存/当店员输入命令withdraw及参数，系统将回馈是否允许移去货物,5,形式化方法的优点,简洁 几乎可以没有二义性 可以通过数学方法来发现矛盾和不完整性 在不同软件工程活动之间平滑地过渡 提供了高层确认的手段,6,有穷状态机,有穷状态机：可以准确的描述一个系统,7,有穷状态机,有穷状态机的组成部分（五元组） 状态集 输入集 转换函数 初始态 终态集,8,有穷状态机,谓词：全局状态的函数 “猫是动物”一句中的“是动物”就是一个谓词，而“猫”是客体 “3大于2”中“大于”是一个谓词 转换规则： 当前状态菜单+事件所选择的项=下个状态 当前状态菜单+事件所选择的项+谓词=下个状态,9,有穷状态机,电梯系统的描述,10,有穷状态机,11,有穷状态机,便于书写，验证 可以通过CASE工具将有穷状态机的规格说明直接转变为源代码 开发一个规模比较大的系统时，三元组数量太多 没有处理定时需求,12,Petri网,Petri网：最初用于自动化处理方面，后来才用于计算机科学中 位置：用圆圈表示 转换：用短直线表示 用于转换的输入函数：由位置指向转换的箭头表示 用于转换的输出函数：由转换指向位置的箭头表示,13,Petri网,权标（Token）及权标的表示 带权标的Petri网：是否允许转换 禁止线：带小圆圈的输入线表示 带禁止线的Petri网,14,Petri网,15,Petri网,16,Z语言,Z语言包含的内容： 给定的集合、数据类型及常数 状态定义 初始状态 操作,17,Z语言,给定的集合：用表示 状态定义：格（schema） 初始状态 操作：？表示输入变量，！表示输出变量，表示某个变量的值发生了改变， 表示差运算,18,Z语言,19,Z语言,20,Z语言,21,Z语言,块处理,22,Z语言,23,Z语言,24,Z语言,25,Z语言,用Z语言书写的规格说明，比较容易发现错误 减少了模糊性、不一致性和遗漏 可以严格验证规格说明的正确性 虽然完全掌握Z语言困难，但是学会编写还是比较容易的 使用Z语言可以降低软件开发费用和总时间 从Z语言的规格说明转换出自然语言的规格说明更为清晰,26,应用形式化方法的准则,应该选用适当的表示方法 应该形式化，但不要过分形式化 应该估算成本 应该有形式化方法顾问随时提供咨询 不应该放弃传统的开发方法 应该建立详尽的文档 不应该放弃质量标准 不应该盲目依赖形式化方法 应该测试、测试再测试 应该重用,27,形式化方法的未来发展,目前还没有在业界广泛应用 形式化技术主要关注于功能和数据，而问题的时序、控制和行为等方面却更难于表达 有些问题元素（界面）也最好用图形技术来刻画 形式化技术学习起来相对困