软件工程 第4章 形式化说明技术

§4. Z 语言
1、Z 语言简介
用Z语言描述的，最简单的形式化规格说明包含4个部分： 给定的集合、数据类型及常数 状态定义 初始状态 操作 （1）给定的集合 Z规格说明从一系列给定的初始化集合开始。 初始化集合是不需要详细定义的集合，用方括号形式表示。 如电梯问题中，给定的初始化集合为Button，表示为 [Button]
报警
报警 报警 报警 报警
报警
报警 报警 报警 B
报警
保险箱解锁 报警 报警 报警
§2. 有穷状态机
初 始 态
保险箱 锁 定 其他 移动
1L
A
3R
B 其他 移动
2L
保险箱 解 锁
终 态
其他 移动
报 警
终态
有穷状态机的状态转换图
§2. 有穷状态机
2、应用例子——电梯问题P.79
(1) 电梯按钮的状态转换图：
（4）操作
例如电梯问题中的按按钮操作Push_Button：
Push_Button
Button_State button ? : Button (button ? buttons) (((button ? pushed) (pushed’ = pushed {button ? })) ((button ? pushed) (pushed’ = pushed)))
p1t1t2 Nhomakorabeap4
p3
p2
p1 t1
§3. Petri网
t2 p1 p3 p4 p2 t1 t2
p4
p3
p2 p1 t1
t2
Petri网的扩充： 加入禁止线 ， 表示没有权标才激发转换。 p3

当前状态〔菜单〕+事件〔所选择的项〕 当前状态〔菜单〕 事件〔所选择的项〕 事件 ⇒ 下个状态。 下个状态。
扩展:在 元组中加入第 个组件——谓词集 ， 元组中加入第6个组件 谓词集P， 扩展 在5元组中加入第 个组件 谓词集 每个谓词都是系统全局状态Y的函数 的函数。 每个谓词都是系统全局状态 的函数。 转换函数T现在是一个从 现在是一个从(J-F)×K×P到J的函数。现 的函数。 转换函数 现在是一个从 × × 到 的函数 在的转换规则形式如下： 在的转换规则形式如下：
第4章 形式化说明技术 章
4.1 概述 4.2 有穷状态机 4.3 Petri网 网 4.4 Z语言 语言 4.5 小结 习题
按照形式化的程度分3类 按照形式化的程度分 类: 非形式化:自然语言 非形式化 自然语言 半形式化:模型如 数据流图或实体-联系图 模型如:数据流图或实体 半形式化 模型如 数据流图或实体 联系图 形式化。 形式化。 :描述系统性质的基于数学的技术，也就是说，如 描述系统性质的基于数学的技术， 描述系统性质的基于数学的技术 也就是说， 果一种方法有坚实的数学基础， 果一种方法有坚实的数学基础，那么它就是形式化 的。
110101E-101 -100111E11101 +1E0 更形式化地，浮点二进制数定义如下： 更形式化地，浮点二进制数定义如下：
〈floatingpoint binary〉∷=［〈sign〉］〈bitstring〉E 〉 ［ 〉 〉 ［〈sign〉］〈bitstring〉 〉 〉 〈sign〉∷=+｜〉 ｜ 〈bitstring〉∷=〈bit〉［〈bitstring〉］ 〉 〈 〉 〉 〈bit〉∷=0｜1 〉 ｜
当然，形式化方法也有缺点： 当然，形式化方法也有缺点：大多数形式化的规格 说明主要关注于系统的功能和数据，而问题的时序、 说明主要关注于系统的功能和数据，而问题的时序、 控制和行为等方面的需求却更难于表示。此外， 控制和行为等方面的需求却更难于表示。此外，形 式化方法比欠形式化方法更难学习， 式化方法比欠形式化方法更难学习，不仅在培训阶 段要花大量的投资，而且对某些软件工程师来说， 段要花大量的投资，而且对某些软件工程师来说， 它代表了一种“文化冲击” 它代表了一种“文化冲击”。 把形式化方法和欠形式化方法有机地结合起来， 把形式化方法和欠形式化方法有机地结合起来，使 它们取长补短，应该能获得更理想的效果。本章讲 它们取长补短，应该能获得更理想的效果。 述的应用形式化方法的准则(见4.1.3节)，对于读者 述的应用形式化方法的准则 见 节， 今后在实际工作中更好地利用形式化方法， 今后在实际工作中更好地利用形式化方法，可能是 有帮助的。 有帮助的。

⑴ 能简洁准确地描述物理现象、对象或动作的 结果。 ⑵ 可以在不同的软件工程活动之间平滑地过渡。 ⑶ 提供了高层确认的手段。可以使用数学方法 证明设计符合规格说明，程序代码正确地实现 了设计结果。
5
2. 应用形式化方法的准则
对形式化方法也应该“一分为二”，既不要 过分夸大它的优点也不要一概排斥。 (1) 应该选择一种适用于当前项目的形式化说 明的技术。 (2)形式化也不要“过分”地追求。如果用形式 化方法详实说明系统中易出错或关键化的部分， 则可达到事半功倍、即只用适中的工作量就能 获得较大回报。
18
Petri网的标记是在 Petri网中权标 (token) 的分配。 例如，在上图中有4个权标，其中一个在P1中， 两个在P2中，P3中没有，还有一个在P4中。 由于P2和P4中有权标，因此t1启动(激发)。通 常当每个输入位置所拥有的权标数大于等于从该 位置到转换的线数时，就允许转换。当t1被激发 时，P2 和P4上各有一个权标被移出，而P1上则 增加一个权标。Petri网中权标总数不是固定的， 在这个例子中两个权标被移出，而P1上只能增加 一个权标。
23
例子1: 使用PN表示“图书馆借书”案例中一本书 的状态图。( 设：P1表示“图书馆”；P2表示 “借书者”；C 表示“借书”转换；R 表示“还 书”转换）
24
例子1’ : 使用PN表示“图书馆借书”案例中一本书 的状态图。( 假设只有会员才能借书）
25
例子2:使用PN表示“图书馆借书”案例中一本书的扩 展状态图，包括超期罚款部分。
7
一.
有穷状态机
1、引入概念 （为抽象的描述系统状态机制） 一个基本有穷状态机可以表示为一个5元组。 (J，K，T，S，F)， 其中： J 是一个有穷的非空状态集； K 是一个有穷的非空输入集； T 是一个从 (J-F)×K 到 J的转换函数； S∈J，是一个初始状态； F J，是终态集。

04章形式化说明技术形式化说明技术（Formal Specification Techniques）是一种系统性、精确地描述和定义软件系统执行行为、功能和性质的技术方法。

它通过使用数学语言和形式规约的方法，将软件系统的设计和实现过程从自然语言的模糊性和歧义性中解放出来，从而改善了软件开发和维护的效率和质量。

形式化说明技术的核心思想是将软件系统描述为一个数学模型，通过形式化的推理和证明，确保系统满足设计要求并具备所需的性质。

形式化说明技术不仅能够精确地描述系统的行为和功能，还可以检查系统的正确性、一致性、完备性、可靠性和安全性等方面的属性，提前发现和解决潜在的问题。

形式化说明技术的应用范围广泛，包括需求分析、系统设计、编码验证、软件测试、系统仿真和代码生成等方面。

下面将介绍几种常见的形式化说明技术。

1. 判定性有穷状态自动机（Deterministic Finite State Automaton，DFSA）：DFSA 是一种常用的形式化说明技术，用于描述系统的状态和状态转移。

它可以形式化地描述系统的行为，通过状态转移图来表示系统的状态变化，从而帮助开发人员更好地理解和设计系统。

2. 时序逻辑（Temporal Logic）：时序逻辑是一种扩展的命题逻辑，用于描述系统的时序性质。

通过形式化的规约、语义和推理，可以验证系统是否满足时序性质，如安全性、活性、不变性等。

时序逻辑广泛应用于软硬件系统的验证和验证。

3. Petri 网（Petri Nets）：Petri 网是一种用于建模和分析并发系统的图形化形式化说明技术。

Petri 网通过描述系统的状态、变迁和资源，揭示系统的并发行为和资源竞争情况，从而帮助开发人员理解和设计并发系统。

4. Z 规范（Z Specification）：Z 规范是一种基于集合论和一阶谓词逻辑的形式化说明技术，用于描述系统的状态、操作和约束等。

Z 规范通过形式化地定义系统的状态集合、操作集合和约束条件，帮助开发人员更好地理解和设计系统。