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