资源描述
第五篇 高级课题 第 14章 形式化方法 概述 14.1 有穷状态杨 14.2 Petri网 14.3 语言 14.4 小结 14.5 根据形式化的程度，可以把软件工程 方法划分成非形式化、半形式化和形式化 三类。使用自然语言描述需求规格说明， 是典型的非形式化方法。使用数据流图或 实体 关系图等图形符号建立模型，是典型 用于开发计算机系统的形式化方法， 是描述系统性质的基于数学的技术，也就 是说，如果一 个方法有坚实的数学基础， 那么它就是形式化的。 14.1 概述 14.1.1 非形式化方法的缺点 基本上使用自然语言描述的系统规格 说明，可能存在矛盾、二义性、含糊性、 14.1.2 软件开发过程中的数 学 数学最有用的性质之一是，它能够简 洁、准确地描述物理现象、对象或动作的 结果，因此是 理想的建模工具。 在软件开发过程中使用数学的另一个 优点是，可以在软件工程活动之间平滑地 过渡。不仅功能规格说明，而且系统设计 也可以用数学表达，当然，程序代码也是 一种数学符号 (虽然是一种相当繁琐、冗长 的数学符号 ) 数学作为软件开发工具的最后一个优 点是，它提供了高层确认的手段。可以使 用数学方法证明，设计符合规格说明，程 序代码正确地反映了设计结果。 14.1.3 应用形式化方法的准 则 为了更好地发挥这种方法的长处，下 面给出应用形式化方法的几条准则，供读 者在实际工作中使用。 选择适用于当前项目的符号系统。 应该形式化，但不要过分形式化。 通常没有必要对系统的每个方面都使用形 式化方法。 应该进行成本 / 不要放弃传统的开发方法。把形式 化方法和结构化方法或面向对象方法集成 起来是可能 的，而且由于取长补短往往能 获得很好的效果。 应该建立详尽的文档。建议使用自 然语言注释来配合形式化的规格说明，以 不应该放弃质量标准。在系统开发 过程中必须一如既往地实施其他 SQA活动。 不应该盲目依赖形式化方法，这种 应该测试、测试再测试。由于形式 化方法不能保证系统绝对正确，因此，软 应该重用。即使使用了形式化方法， 软件重用仍然是降低软件成本和提高软件 14.2 有穷状态机 利用有穷状态机可以准确地描述一个 系统，因此是表达规格说明的一种形式化 14.2.1 下面通过一个简单例子介绍有穷状态 图 14.1 保险箱的状态转换图 表 14 . 1 当前状态 次态 转盘动作 保险箱锁定 A B 1L A 报警 报警 1R 报警 报警 报警 2L 报警 报警 保险箱解锁 2R 报警 报警 报警 3L 报警 报警 报警 3R 报警 B 报警 从上面这个简单例子可以看出，一个 有穷状态机包括下述 5个部分：状态集 J、 输入 集 K、由当前状态和当前输入确定下 一个状态 (次态 )的转换函数 T、初始态 S和 终态集 F。 如果使用更形式化的术语，一个有穷 状态机可以表示为一个 5元组 (J， R， T， S， F)，其中： J K T是一个从 (J-F) K到 J的转换函数； SJ F J 当前状态 菜单 +事件 所选择的项 下个状态为了对一个系统进行规格说明， 通常都需要对有穷状态机做一个很有用的 扩展，即在前述的 5元组中加入第 6个组 件 谓词集 P，即把有穷状态机扩展为一 个 6元组，其中每个谓词都是系统全局状态 Y的函数。 转换函数 T现在是一个从 (J-F) K P 到 J 当前状态 菜单 +事件 所选择的项 + 14.2.2 为了说明在实际工作中怎样使用形式 化的方法，现在我们用有穷状态机技术给 出电梯问题的 规格说明。 电梯按钮的状态转换图如图 14.2所示。 令 EB(e,f)表示按下电梯 e内的按钮并请求 到 f层去。 EB(e,f)有两个状态，分别是按 钮发光 (打开 )和不发光 (关闭 )。 EBON(e,f)：电梯按钮 (e， f) EBOFF(e,f)：电梯按钮 (e， f) 如果电梯按钮 (e,f)发光且电梯到达 f 层，该按钮将熄灭。相反如果按钮熄灭， 则按下它时，按钮将发光。上述描述中包 图 14.2 电梯按钮的状态转 换图 EBP(e,f)：电梯按钮 (e,f) EAF(e,f)：电梯 e到达 f 为了定义与这些事件和状态相联系的 状态转换规则，需要一个谓词 V， (e,f)， V(e,f)：电梯 e停在 f 接下来让我们考虑楼层按钮。令 FB(d,f)表示 f层的按钮请求电梯向 d方向运 动，楼层按钮 FB(d,f)的状态转换图如图 14.3 FBON(d,f)：楼层按钮 (d,f)打开； FBOFF(d,f)：楼层按钮 (d,f)关闭。 如果楼层按钮已经打开，而且一部电 梯到达 f层，则按钮关闭。反之，如果楼层 按钮原来是关闭的，被按下后该按钮将打 FBP(d,f)：楼层按钮 (d,f) EAF(1n,f)：电梯 1或 或 n到达 f层 其中 1n表示或为 1或为 2或为 n 图 14.3 楼层按钮的状态转 换图 为了定义与这些事件和状态相联系的 状态转换规则，同样也需要一个谓词，它 是 S(d,e， f) S(d,e,f)：电梯 e停在 f层并且移动方 向由 d确定为向上 (d=U)或向下 (d=D)或待定 (d=N) 这个谓词实际上是一个状态，形式化 使用谓词 S(d,e,f)，形式化转换规则 FBOFF(d,f)+FBP(d,f)+not S(d,1n,f) JX*9FBON(d,f) FBON(d,f)+EAF(1n,f)+S(d,1n,f) JX*9FBOFF(d,f) 其中， d=UorD 也就是说，如果在 f层请求电梯向 d方 向运动的楼层按钮处于关闭状态，现在该 按钮被按下，并且当时没有正停在 f层准备 向 d方向移动的电梯，则该楼层按钮打开。 反之，如果楼层按钮已经打开，且至少有 一部电梯到达 f层，该部电梯将朝 d方向运 在讨论电梯按钮状态转换规则时定义 的谓词 V(e,f)，可以用谓词 S(d,e,f)重新 V(e,f)=S(U， e,f)or S(D,e,f)or S(N,e,f) 定义电梯按钮和楼层按钮的状态都很 简单、直观的事情。现在转向讨论电梯的 状态及其转换规则，就会出现一些复杂的 情况。一个电梯状态实质上包含许多子状 态 (例如，电梯减速、停止、开门、在一段 时间后自动关门 ) M(d,e,f)：电梯 e正沿 d方向移动，即 将到达的是第 f S(d,e,f)：电梯 e停在 f层，将朝 d方向 移动 (尚未关门 ) W(e,f)：电梯 e在 f层等待 (已关门 )。 其中 S(d,e,f)状态已在讨论楼层按钮时 定义过，但是，现在的定义更完备一些。 图 14.4是电梯的状态转换图。注意， 三个电梯停止状态 S(U,e,f)、 S(N， e,f)和 S(D， e,f)已被组合成一个大的状态，这样 做的目的是减少状态总数以简化流图。 图 14.4 电梯的状态转换图 图 14.4中包含了下述三个可触发状态 发生改变的事件 DC(e,f)：电梯 e在楼层 f ST(e,f)：电梯 e靠近 f层时触发传感器， 电梯控制器决定在当前楼层电梯是否停下。 RL：电梯按钮或楼层按钮被按下进入 最后，给出电梯的状态转换规则。为 简单起见，这里给出的规则仅发生在关门 S(U， e,f)+DC(e,f) JX*9M(U， e,f+1) S(D， e,f)+DC(e,f) JX*9M(D,e,f-1) S(N,e,f)+DC(e,f) JX*9W(e,f) e停在 f 层准备向上移动，且门已经关闭，则电 梯将向上一楼层移动。第二条和第三条规 则，分别对应于电梯即将下降或者没有待 处理的请求的情况。 14.2.3 有穷状态机方法采用了一种简单的格 当前状态 +事件 + JX*9下个状态 这种形式的规格说明易于书写、易于 验证，而且可以比较容易地把它转变成设 计或程序代码。事实上，可以开发一个 CASE工具把一个有穷状态机规格说明直接 转变为源代码。 维护可以通过重新转变来实现，也就 是说，如果需要一个新的状态或事件，首 先修改规格说明，然后直接由新的规格说 有穷状态机方法比数据流图技术更精 确，而且和它一样易于理解。不过，它也 有缺点：在开发一个大系统时三元组 (即状 态、事件、谓词 )的数量会迅速增长。此外， 和数据流图方法一样，形式化的有穷状态 机方法也没有处理定时需求。下节将介绍 的 Petri网技术，是一种可处理定时问题的 14.3 Petri网 14.3.1 Petri网包含 4种元素：一组位置 P、一 组转换 T、输入函数 I以及输出函数 O。图 14.5举例说明了 Petri网的组成。 一组位置 P为 P1， P2， P3， P4，在 一组转换 T为 t1， t2，在图中用 图 14.5 Petri网的组成 两个用于转换的输入函数，用由位置 I(t1)= P2,P4 I(t2)= P2 两个用于转换的输出函数，用由转换 O(t1)= P1 O(t2)= P3， P3 注意，输出函数 O(t2)中有两个 P3，是因为 有两个箭头由 t2指向 P3 更形式化的 Petri网结构，是一个四元 组 C=(P,T,I,O) P= P1， ,Pn是一个有穷位置集， n0 T= t1,tm是一个有穷转换集， m0 ，且 T和 P I： TP 为输入函数，是由转换到位 置无序单位组 (bags) O： TP 为输出函数，是由转换到位 一个无序单位组或多重组是允许一个 Petri网的标记是在 Petri网中令牌 (token)的分配。例如，在图 14.6中有 4个 令牌，其中一个在 P1中，两个在 P2中， P3中 没有，还有一个在 P4中。上述标记可以用 向量 (1， 2， 0， 1)表示。由于 P2和 P4中有 令牌，因此 t1启动 (即被激发 )。 通常，当每个输入位置所拥有的令牌 数等于从该位置到转换的线数时，就允许 转换。当 t1被激发时， P2和 P4上各有一个令 牌被移出，而 P1上则增加一个令牌。 Petri网中令牌总数不 是固定的，在这 个例子中两个令牌被移出，而 P1上只能增 加一个令牌。 在图 14.6中 P2上有令牌，因此 t2也可 以被激发。当 t2被激发时， P2上将移走一 个令牌，而 P3上新增加两个令牌。 Petri网 具有非确定性，也就是说，如果数个转换 都达到了激发条件，则其中任意一个都可 以被激发。 图 14.6所示 Petri网的标记为 (1， 2， 0， 1)， t1和 t2都可以被激发。假设 t1被激发了， 则结果如图 14.7所示，标记为 (2， 1， 0， 0)。 此时，只有 t2可以被激发。如果 t2也 被激发了，则令牌从 P2中移出，两个新令 牌被放在 P3上，结果如图 14.8所示，标记 为 (2， 0， 2， 0)。 图 14.6 带标记的 Petri网 图 14.7 图 14.6的 Petri网在转换 t1被激发后的情况 图 14.8 图 14.7的 Petri网在转换 t2被激发后的情况 更形式化地说， Petri网 C=(P,T,I,O)中 的标记 M，是由一组位置 P到一组非负整数 M： P 0， 1， 2， 这样，带有标记的 Petri网成为一个五 元组 (P， T， I， O， M)。 对 Petri网的一个重要扩充是加入禁止 线。如图 14.9所示，禁止线是用一个小圆 圈而不是用箭头标记的输入线。 通常，当每个输入线上至少有一个令 牌，而禁止线上没有令牌的时候，相应的 转换才是允许的。在图 14.9中， P3上有一 个令牌而 P2上没有令牌，因此转换 t1可以被 激发。 图 14.9 含禁止线的 Petri网 14.3.2 让我们把 Petri网应用于上一节讨论过 的电梯问题。当用 Petri网表示电梯系统的 规格说明时，每个楼层用一个位置 Ff代表 (1fm) ，在 Petri网中电梯是用一个令 牌代表的。在位置 Ff上有令牌，表示在楼 层 f 1. 为了用 Petri网表达电梯按钮的规格说 明，在 Petri网中还必须设置其他的位置。 电梯中楼层 f的按钮，在 Petri网中用位置 EBf表示 (1fm) 。在 EBf上有一个令牌， 就表示电梯内楼层 f 电梯按钮只有在第一次被按下时才会 由暗变亮，以后再按它则只会被忽略。图 14.10所示的 Petri网准确地描述了电梯按 钮的行为规律。首先，假设按钮没有发亮， 显然在位置 EBf上没有令牌，从而在存在禁 止线的情况下，转换 “ EBf被按下 ” 是允许 发生的。 假设现在按下按钮，则转换被激发并 在 EBf上放置了一个令牌，如图 14.10所示。 以后不论再按下多少次按钮，禁止线与现 有令牌的组合都决定了转换 “ EBf被按下 ” 不能再被激发了，因此，位置 EBf上的令牌 数不会多于 1 图 14.10 Petri网表示的电梯按钮 假设电梯由 g层驶向 f层，因为电梯在 g 层，如图 14.10所示，位置 Fg上有一个令牌。 由于每条输入线上各有一个令牌，转换 “ 电梯在运行 ” 被激发，从而 EBf和 Fg上的 令牌被移走，按钮 EBf被关闭，在位置 Ff上 出现一个新令牌，即转换的激发使电梯由 g 层驶到 f 事实上，电梯由 g层移到 f层是需要时 间的，为处理这个情况及其他类似的问题 (例如，由于物理上的原因按钮被按下后不 能马上发亮 )， Petri网模型中必须加入时 限。 也就是说，在标准 Petri网中转换是瞬 时完成的，而在现实情况下就需要时间控 制 Petri网，以使转换与非零时间相联系。 2. 楼层按钮 在 Petri网中楼层按钮用位置 和 表示，分别代表 f楼层请求电梯上行和下行 的按钮。底层的按钮为 ，最高层的按 钮为 ，中间每一层有两个按钮 和 (1 f m) ufFB dfFB uFB1 dmFB ufFB dfFB 图 14.11 Petri网表示楼层按钮 第三条约束 C3：当电梯没有收到请求 这条约束很容易实现，如图 14.11所 示，当没有请求 ( 和 上无令牌 )时， 任何一个转换“电梯在运行”都不能被激 发。 ufFB d fFB 14.4 Z语言 14.4.1 简介 本节结合电梯问题的例子，简要地介绍 Z 用 Z语言描述的、最简单的形式化规格 说明含有下述 4 现在依次介绍这 4 1. 一个 Z规格说明从一系列给定的初始化 集合开始。所谓初始化集合就是不需要详 细定义的集合，这种集合用带方括号的形 式表示。对于电梯问题，给定的初始化集 合称为 Button，即所有按钮的集合，因此， Z Button 2. 一个 Z规格说明由若干个 “ 格 (schema)” 组成，每个格含有一组变量说明和一系列 限定变量取值范围的谓词。例如，格 S的格 式如图 14.12 在电梯问题中， Button有 4个子集，即 floor_buttons(楼层按钮的集合 )、 elevator_buttons(电梯按钮的集合 )、 buttons(电梯问题中所有按钮的集合 )以及 pushed(所有被按的按钮的集合，即所有处 于打开状态的按钮的集合 )。图 14.13描述 了格 Button_State，其中，符号 P表示幂集 (即给定集的所有子集 )。 约束条件声明， floor_buttons集与 elevator_buttons集不相交，而且它们共 同组成 buttons集 (在下面的讨论中并不需 要 floor_buttons集和 elevator_buttons集， 把它们放于图 14.13中只是用来说明 Z格包 含的内容 ) 图 14.12 Z格 S的格式 图 14.13 Z格 Button_State 3. 抽象的初始状态是指系统第一次开启 时的状态。对于电梯问题来说，抽象的初 Button_Init Button_State pushed= 上式表示，当系统首次开启时 pushed 4. 如果一个原来处于关闭状态的按钮被 按下，则该按钮开启，这个按钮就被添加 到 pushed集中。图 14.14定义了操作 Push_Button(按按钮 )。 Z语言的语法规定，当一个格被用在另 一个格中时，要在它的前面加上三角形符 号作为前缀，因此，格 Push_Button的第 一行最前面有一个三角形符号作为格 Button_State的前缀。 操作 Push_Button有一个输入变量 “ button?”。问号 “ ?”表示输入变量，而 感叹号 “ !”代表输出变量。 操作的谓词部分，包含了一组调用操 作的前置条件，以及操作完全结束后的后 置条件。如果前置条件成立，则操作执行 完成后可得到后置条件。但是，如果在前 置条件不成立的情况下调用该操作，则不 能得到指定的结果 (因此结果无法预测 )。 图 14.14中的第一个前置条件规定， “ button?”必须是 buttons的一个元素， 而 buttons是电梯系统中所有按钮的集合。 如果第二个前置条件 button? pushed得到 满足 (即按钮没有开启 )，则更新 pushed按 钮集，使之包含刚开启的按钮 “ button?”。 在 Z语言中，当一个变量的值发生改变 时，就用符号 “” 表示。也就是说，后 置条件是当执行完操作 Push_Button之后， “ button?”将被加入到 pushed集中。我们 无需直接打开按钮，只要使 “ button?”变 成 pushed 图 14.14 操作 Push_Button的 Z规格说明 还有一种可能性是，被按的按钮原先 已经打开了。由于 button?pushed ，根据 第三个前置条件，将没有任何事情发生， 这可以用 pushed=pushed 来表示，即 pushed的新状态和旧状态一样。 注意，如果没有第三个前置条件，规 格说明将不能说明在一个按钮已被按过之 后又被按了一次的情况下将发生什么事， 假设电梯到达了某楼层，如果相应的 楼层按钮已经打开，则此时它会关闭；同 样，如果相应的电梯按钮已经打开，则此 时它也会关闭。也就是说，如果 “ button?” 属于 pushed集，则将它移出该集合，如图 14.15所示 (符号 “ ” 表示集合差运算 )。 但是，如果按钮 “ button?”原先没有 打开，则 pushed集合不发生变化。 本节的讨论有所简化，没有区分上行 和下行楼层按钮，但是，仍然讲清了使用 Z 图 14.15 操作 Floor_Arrival的 Z规格说明 14.4.2 已经在许多软件开发项目中成功地运 用了 Z语言，目前， Z也许是应用得最广泛 的形式化语言，尤其是在大型项目中 Z语言 的优势更加明显。 Z语言之所以会获得如此 可以比较容易地发现用 Z写的规格 说明的错误，特别是在自己审查规格说明， 及根据形式化的规格说明来审查设计与代 用 Z写规格说明时，要求作者十分 精确地使用 Z说明符。由于对精确性的要求 很高，从而和非形式化规格说明相比，减 Z 是一种形式化语言，在需要时开 发者可以严格地验证规格说明的正确性。 虽然完全学会 Z语言相当困难，但 是，经验表明，只学过中学数学的软件开 发人员仍然可以只用比较短的时间就学会 编写 Z规格说明，当然，这些人还没有能力 使用 Z语言可以降低软件开发费用。 虽然用 Z写规格说明所需用的时间比使用非 形式化技术要多，但开发过程所需要的总 虽然用户无法理解用 Z写的规格说 明，但是，可以依据 Z规格说明用自然语言 重写规格说明。经验证明，这样得到的自 然语言规格说明，比直接用自然语言写出 使用形式化规格说明是全球的总趋势， 过去，主要是欧洲习惯于使用形式化规格 说明技术，现在越来越多的美国公司也开 14.5 小结 基于数学的形式化规格说明技术，目 前还没有在软件产业界广泛应用，但是， 与欠形式化的方法比较起来，它确实有实 质性的优点： 形式化的规格说明可以用数学方法研 究、验证 (例如，一个正确的程序可以被证 明满足其规格说明，两个规格说明可以被 证明是等价的，规格说明中存在的某些形 式的不完整性和不一致性可以被自动地检 测出来 )。 此外，形式化的规格说明消除了二义 性，而且它鼓励软件开发者在软件工程过 程的早期阶段使用更严格的方法，从而可 当然，形式化方法也有缺点：大多数 形式化的规格说明主要关注于系统的功能 和数据，而问题的时序、控制和行为等方 面的需求却更难于表示。此外，形式化方 法比欠形式化方法更难学习，不仅在培训 阶段要花大量的投资，而且对某些软件工 程师来说，它代表了一种 “ 文化冲击 ” 。 把形式化方法和欠形式化方法有机地 结合起来，使它们取长补短，应该能获得 更理想的效果。本章讲述的应用形式化方 法的准则 (见 14.1.3节 )，对于读者今后在 实际工作中更好地利用形式化方法，可能 本章简要地介绍了有穷状态机、 Petri 网和 Z语言等三种典型的形式化方法，使读 者对它们有初步的、概括的了解。当然， 要想在实际工作中使用这些方法，还需要
展开阅读全文