《软件工程导论》（第6版）第4章形式化说明技术复习笔记

第4章　形式化说明技术

一、概述

按照形式化的程度，可以把软件工程使用的方法划分成非形式化、半形式化和形式化3类。用自然语言描述需求规格说明，是典型的非形式化方法。用数据流图或实体联系图建立模型，是典型的半形式化方法。所谓形式化方法，是描述系统性质的基于数学的技术，也就是说，如果一种方法有坚实的数学基础，那么它就是形式化的。

1．非形式化方法的缺点

（1）矛盾：一组相互冲突的陈述。

（2）二义性：指读者可以用不同方式理解的陈述。

（3）含糊性：指没有指明任何有用信息的笼统的陈述。

（4）不完整性：指没有指明具体功能的陈述。

（5）抽象层次混乱：指非抽象的陈述中混进了一些关于细节的低层次陈述。

2．形式化方法的优点

（1）能够简洁准确地描述物理现象、对象或动作的结果。准确到几乎没有二义性，而且可以用数学方法来验证，以发现存在的矛盾和不完整性，在这样的规格说明中完全没有含糊性。

（2）可以在不同的软件工程活动之间平滑地过渡。不仅功能规格说明，而且系统设计也可以用数学表达，当然，程序代码也是一种数学符号。

（3）提供了高层确认的手段。可以使用数学方法证明，设计符合规格说明，程序代码正确地实现了设计结果。

3．应用形式化方法的准则

为了更好地发挥形式化方法的长处，应用形式化方法应遵循以下几条准则：

（1）应该选用适当的表示方法

通常，一种规格说明技术只能用自然的方式说明某一类概念，如果用这种技术描述其不适于描述的概念，则不仅工作量大而且描述方式也很复杂。

（2）应该形式化，但不要过分形式化

形式化规格说明技术要求人们非常准确地描述事物，因此有助于防止含糊和误解。事实上，如果用形式化方法仔细说明系统中易出错的或关键的部分，则只用适中的工作量就能获得较大回报。

（3）应该估算成本

为了使用形式化方法，通常需要事先进行大量的培训。最好预先估算所需的成本并编入预算。

（4）应该有形式化方法顾问随时提供咨询

绝大多数软件工程师对形式化方法中使用的数学和逻辑并不很熟悉，而且没受过使用形式化方法的专业训练，因此，需要专家指导和培训。

（5）不应该放弃传统的开发方法

把形式化方法和结构化方法或面向对象方法集成起来是可能的，而且由于取长补短往往能获得很好的效果。

（6）应该建立详尽的文档

建议使用自然语言注释形式化的规格说明书，以帮助用户和维护人员理解系统。

（7）不应该放弃质量标准

形式化方法并不能保证软件的正确性，它们只不过是有助于开发出高质量软件的一种手段。除了使用形式化说明技术外，在系统开发过程中仍然必须一如既往地实施其他质量保证活动。

（8）不应该盲目依赖形式化方法

形式化方法并不能保证开发出的软件绝对正确，例如，无法用形式化方法证明从非形式化需求到形式化规格说明的转换是正确的，因此，必须用其他方法（例如评审、测试）来验证软件正确性。

（9）应该测试、测试再测试

形式化方法不仅不能保证软件系统绝对正确，也不能证明系统性能或其他质量指标符合需要，因此，软件测试的重要性并没有降低。

（10）应该重用

即使采用了形式化方法，软件重用仍然是降低软件成本和提高软件质量的唯一合理的方法。而且用形式化方法说明的软件构件具有清晰定义的功能和接口，使得它们有更好的可重用性。

二、有穷状态机

有穷状态机是表达规格说明的一种形式化方法。

1．概念

（1）引入

一个保险箱上装了一个复合锁，锁有3个位置，分别标记为1、2、3，转盘可向左（L）或向右（R）转动。在任意时刻转盘都有6种可能的运动，即1L、1R、2L、2R、3L和3R。保险箱的组合密码是1L、3R、2L转盘的任何其他运动都将引起报警。图4-1描绘了保险箱的状态转换情况。有一个初始态，即保险箱锁定状态。若输入为1L，则下一个状态为A，但是，若输入不是1L而是转盘的任何其他移动，则下一个状态为“报警”，报警是两个终态之一（另一个终态是“保险箱解锁”）。如果选择了转盘移动的正确组合，则保险箱状态转换的序列为从保险箱锁定到A再到B，最后到保险箱解锁，即另外一个终态。图4-1是一个有穷状态机的状态转换图。状态转换并不一定要用图形方式描述，表4-1的表格形式也可以表达同样的信息。除了两个终态之外，保险箱的其他状态将根据转盘的转动方式转换到下一个状态。

图4-1 保险箱的状态转换图

表4-1 保险箱的状态转换表

（2）构成

一个有穷状态机包括下述5个部分：状态集J、输入集K、由当前状态和当前输入确定下一个状态（次态）的转换函数T、初始态S和终态集F。一个有穷状态机可以表示为一个5元组（J，K，T，S，F）。

①状态集J：{保险箱锁定，A，B，保险箱解锁，报警}。

②输入集K：{1L，1R，2L，2R，3L，3R}。

③转换函数T：如表4-1所示。

④初始态S：保险箱锁定。

⑤终态集F：{保险箱解锁，报警}。

其中：J是一个有穷的非空状态集；K是一个有穷的非空输入集；T是一个从（J-F）×K到J的转换函数；S∈J，是一个初始状态；F⊆J，是终态集。

（3）状态转换

状态的每个转换都具有下面的形式：

当前状态[菜单]+事件[所选择的项]->下个状态

（4）扩展

对有穷状态机做一个扩展，即在前述的5元组中加入第6个组件—谓词集P，从而把有穷状态机扩展为一个6元组，其中每个谓词都是系统全局状态Y的函数。转换函数T现在是一个从（J-F）×K×P到J的函数。现在的转换规则形式如下：

当前状态[菜单]+事件[所选择的项]+谓词->下个状态

2．评价

（1）优点

①有穷状态机方法采用了一种简单的格式来描述规格说明：当前状态+事件+谓词->下个状态。这种形式的规格说明易于书写、易于验证，而且可以比较容易地把它转变成设计或程序代码。

②有穷状态机方法比数据流图技术更精确，而且易于理解。

（2）缺点

①在开发一个大系统时，三元组（即状态、事件、谓词）的数量会迅速增长。

②形式化的有穷状态机方法没有处理定时需求。

三、Petri网

1．概念

（1）功能

并发系统中遇到的一个主要问题是定时问题。定时问题通常是由不好的设计或有错误的实现引起的，而这样的设计或实现通常又是由不好的规格说明造成的。如果规格说明不恰当，则有导致不完善的设计或实现的危险。用于确定系统中隐含的定时问题的一种有效技术是Petri网，这种技术的一个很大的优点是它也可以用于设计中。

（2）构成

①一般构成

Petri网包含4种元素：一组位置P、一组转换T、输入函数I，以及输出函数O。图4-2举例说明了Petri网的组成。

图4-2 Petri网的组成

a．一组位置P为{ P1，P2，P3，P4 }，在图中用圆圈代表位置。

b．一组转换T为{ T1，T2 }在图中用短直线表示转换。

c．两个用于转换的输入函数，用由位置指向转换的箭头表示，它们是：

I（t1）={ P2，P4 }

I（t2）={ P2 }

d．两个用于转换的输出函数，用由转换指向位置的箭头表示，它们是：

O（t1）={ P1 }

O（t2）={ P3，P3 }

注意：输出函数O（t1）中有两个P3，是因为有两个箭头由t2指向P3。

②形式化的Petri网

更形式化的Petri网结构是一个四元组：

C=（P，T，I，O）

其中：

a．P={P1，...Pn}是一个有穷位置集，n≥0。

b．T={t1，…，tm}是一个有穷转换集，m≥0，且T和P不相交。

c．I：T→P∞为输入函数，是由转换到位置无序单位组（bags）的映射。

d．O：T→P∞为输出函数，是由转换到位置无序单位组的映射。

（3）分配权标

①带标记的Petri网

在图4-3中有4个权标，其中一个在P1中，两个在P2中，P3中没有，还有一个在P4中。标记可以用向量（1，2，0，1）表示。由于P2和P4中有权标，因此t1启动（即被激发）。当每个输入位置所拥有的权标数大于等于从该位置到转换的线数时，就允许转换。当t1被激发时，P2和P4上各有一个权标被移出，而P1上则增加一个权标。Petri网中权标总数不是固定的，在这个例子中两个权标被移出，而P1上只能增加一个权标。

图4-3 带标记的Petri网

②Petri网转换

在图4-3中P2上有权标，因此t2也可以被激发。当t2被激发时，P2上将移走一个权标，而P3上新增加两个权标。Petri网具有非确定性，也就是说，如果数个转换都达到了激发条件，则其中任意一个都可以被激发。图4-3所示Petri网的标记为（1，2，0，1），t1和t2都可以被激发。假设t1被激发了，则结果如图4-4所示，标记为（2，1，0，0）。此时，只有t2可以被激发。如果t2也被激发了，则权标从P2中移出，两个新权标被放在P3上，结果如图4-5所示，标记为（2，0，2，0）。