M (U,e,f+1)M(D,ef),e,J)DC(e,f)ST(e,f)s(N,e,f)s(D,e,f)s(U,e,f)DC(e,f)DC(e,f)W(e,f)M(U,e,f)M(D,e,f-1)图4.电梯的状态转换图3个电梯停止状态S(U,e,f)、S(N,e,f)和S(D,e,f)已被组合成一个大的状态，这样做的目的是减少状态总数以简化流图。图4中包含了下述3个可触发状态发生改变的事件。DC(e,f)：电梯e在楼层f关上门ST(e,f)：电梯e靠近f层时触发传感器，电梯控制器决定在当前楼层电梯是否停下RL：电梯按钮或楼层按钮被按下进入打开状态，登录需求最后，给出电梯的状态转换规则。为简单起见，这里给出的规则仅发生在关门之时。S(U,e,f)+DC(e,f)M(U,e,f+1)S(D,e,f)+DC(e,f)M(D,e,f-1)S(N,e,f)+DC(e,f)W(e,f)第一条规则表明，如果电梯e停在f层准备向上移动，且门已经关闭，则电梯将向上一楼层移动。第二条和第三条规则，分别对应于电梯即将下降或者没有待处理的请求的情况。评价4.2.3有穷状态机方法采用了一种简单的格式来描述规格说明：当前状态+事件+谓词下个状态这种形式的规格说明易于书写、易于验证，而且可以比较容易地把它转变成设计或程序代码。事实上，可以开发一个CASE工具把一个有穷状态机规格说明直接转变为源代码。维护可以通过重新转变来实现，也就是说，如果需要一个新的状态或事件，首先修改规格说明，然后直接由新的规格说明生成新版本的产品。有穷状态机方法比数据流图技术更精确，而且和它一样易于理解。不过，它也有缺点：
图 4.电梯的状态转换图 3 个电梯停止状态 S(U,e,f)、S(N,e,f)和 S(D,e,f)已被组合成一个大的状态，这样做的目的 是减少状态总数以简化流图。 图 4 中包含了下述 3 个可触发状态发生改变的事件。 DC(e,f)：电梯 e 在楼层 f 关上门 ST(e,f)：电梯 e 靠近 f 层时触发传感器，电梯控制器决定在当前楼层电梯是否停下 RL：电梯按钮或楼层按钮被按下进入打开状态，登录需求 最后，给出电梯的状态转换规则。为简单起见，这里给出的规则仅发生在关门之时。 S(U,e,f)+DC(e,f) M(U,e,f+1) S(D,e,f)+DC(e,f) M(D,e,f-1) S(N,e,f)+DC(e,f) W(e,f) 第一条规则表明，如果电梯 e 停在 f 层准备向上移动，且门已经关闭，则电梯将向上一 楼层移动。第二条和第三条规则，分别对应于电梯即将下降或者没有待处理的请求的情况。 4.2.3 评价 有穷状态机方法采用了一种简单的格式来描述规格说明： 当前状态+事件+谓词 下个状态 这种形式的规格说明易于书写、易于验证，而且可以比较容易地把它转变成设计或程序 代码。事实上，可以开发一个 CASE 工具把一个有穷状态机规格说明直接转变为源代码。维 护可以通过重新转变来实现，也就是说，如果需要一个新的状态或事件，首先修改规格说明， 然后直接由新的规格说明生成新版本的产品。 有穷状态机方法比数据流图技术更精确，而且和它一样易于理解。不过，它也有缺点：
在开发一个大系统时三元组（即状态、事件、谓词)的数量会迅速增长。此外，和数据流图方法一样，形式化的有穷状态机方法也没有处理定时需求。下节将介绍的Petri网技术，是-种可处理定时问题的形式化方法。4.3Petri网概念4.3.1并发系统中遇到的一个主要问题是定时问题。这个问题可以表现为多种形式，如同步问题、竞争条件以及死锁问题。定时问题通常是由不好的设计或有错误的实现引起的，而这样的设计或实现通常又是由不好的规格说明造成的。如果规格说明不恰当，则有导致不完善的设计或实现的危险。用于确定系统中隐含的定时问题的一种有效技术是Petri网，这种技术的一个很大的优点是它也可以用于设计中。etri网是由CarlAdamPetri发明的。最初只有自动化专家对Petri网感兴趣，后来Petri网在计算机科学中也得到广泛的应用，例如，在性能评价、操作系统和软件工程等领域，Petri网应用得都比较广泛。特别是已经证明，用Petri网可以有效地描述并发活动。Petri网包含4种元素：一组位置P、一组转换T、输入函数1以及输出函数O。图4.5举例说明了Petri网的组成。P2tP3P1pP4图5Petri网的组成一组位置P为（P1，P2，P3，P4)，在图中用圆圈代表位置。一组转换T为（t1，t2)，在图中用短直线表示转换。两个用于转换的输入函数，用由位置指向转换的箭头表示，它们是：I(t1)=(P2,P4)I(t2)= (P2)两个用于转换的输出函数，用由转换指向位置的箭头表示，它们是：O(t1)= (P1)O(t2)=(P3,P3)注意，输出函数O(t2)中有两个P3，是因为有两个箭头由t2指向P3。更形式化的Petri网结构，是一个四元组C=(PT,I,O)。其中,P=（P1，，Pn）是一个有穷位置集，n≥0。T=（t1，，tm）是一个有穷转换集，m≥0，且T和P不相交
在开发一个大系统时三元组(即状态、事件、谓词)的数量会迅速增长。此外，和数据流图方 法一样，形式化的有穷状态机方法也没有处理定时需求。下节将介绍的 Petri 网技术，是一 种可处理定时问题的形式化方法。 4.3 Petri 网 4.3.1 概念 并发系统中遇到的一个主要问题是定时问题。这个问题可以表现为多种形式，如同步问 题、竞争条件以及死锁问题。定时问题通常是由不好的设计或有错误的实现引起的，而这样 的设计或实现通常又是由不好的规格说明造成的。如果规格说明不恰当，则有导致不完善的 设计或实现的危险。用于确定系统中隐含的定时问题的一种有效技术是 Petri 网，这种技术 的一个很大的优点是它也可以用于设计中。 etri 网是由 Carl Adam Petri 发明的。最初只有自动化专家对 Petri 网感兴趣，后来 Petri 网在计算机科学中也得到广泛的应用，例如，在性能评价、操作系统和软件工程等领域，Petri 网应用得都比较广泛。特别是已经证明，用 Petri 网可以有效地描述并发活动。 Petri 网包含 4 种元素：一组位置 P、一组转换 T、输入函数 I 以及输出函数 O。图 4.5 举例说明了 Petri 网的组成。 图 5 Petri 网的组成 一组位置 P 为｛P1，P2，P3，P4｝，在图中用圆圈代表位置。 一组转换 T 为｛t1，t2｝，在图中用短直线表示转换。 两个用于转换的输入函数，用由位置指向转换的箭头表示，它们是： 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｝是一个有穷位置集，n≥0。 T=｛t1，.，tm｝是一个有穷转换集，m≥0，且 T 和 P 不相交
I：T→Poo为输入函数，是由转换到位置无序单位组(bags)的映射。O：T→P为输出函数，是由转换到位置无序单位组的映射。一个无序单位组或多重组是允许一个元素有多个实例的广义集。Petri网的标记是在Petri网中权标(token)的分配。例如，在图4.6中有4个权标，其中一个在P1中，两个在P2中，P3中没有，还有一个在P4中。上述标记可以用向量(1，2，0，1)表示。由于P2和P4中有权标，因此t1启动(即被激发)。通常，当每个输入位置所拥有的权标数大于等于从该位置到转换的线数时，就允许转换。当t1被激发时，P2和P4上各有一个权标被移出，而P1上则增加一个权标。Petri网中权标总数不是固定的，在这个例子中两个权标被移出，而P1上只能增加一个权标。在图4.6中P2上有权标，因此t2也可以被激发。当t2被激发时，P2上将移走一个权标，而P3上新增加两个权标。Petri网具有非确定性，也就是说，如果数个转换都达到了激发条件，则其中任意一个都可以被激发。图4.6所示Petri网的标记为(1，2，0，1)，t1和t2都可以被激发。假设t1被激发了，则结果如图4.7所示，标记为(2，1，0，0)。此时，只有t2可以被激发。如果t2也被激发了，则权标从P2中移出，两个新权标被放在P3上，结果如图4.8所示，标记为(2，0，2，0)。P2tiPiP3p4图6带标记的Petri网t2P2Pit,P3P4图7Petri网被激发后的情况
I：T→P∞为输入函数，是由转换到位置无序单位组(bags)的映射。 O：T→P∞为输出函数，是由转换到位置无序单位组的映射。 一个无序单位组或多重组是允许一个元素有多个实例的广义集。 Petri 网的标记是在 Petri 网中权标(token)的分配。例如，在图 4.6 中有 4 个权标，其中 一个在 P1 中，两个在 P2 中，P3 中没有，还有一个在 P4 中。上述标记可以用向量(1，2，0， 1)表示。由于 P2 和 P4 中有权标，因此 t1 启动(即被激发)。通常，当每个输入位置所拥有的 权标数大于等于从该位置到转换的线数时，就允许转换。当 t1 被激发时，P2 和 P4 上各有 一个权标被移出，而 P1 上则增加一个权标。Petri 网中权标总数不是固定的，在这个例子中 两个权标被移出，而 P1 上只能增加一个权标。 在图 4.6 中 P2 上有权标，因此 t2 也可以被激发。当 t2 被激发时，P2 上将移走一个权 标，而 P3 上新增加两个权标。Petri 网具有非确定性，也就是说，如果数个转换都达到了激 发条件，则其中任意一个都可以被激发。图 4.6 所示 Petri 网的标记为(1，2，0，1)，t1 和 t2 都可以被激发。假设 t1 被激发了，则结果如图 4.7 所示，标记为(2，1，0，0)。此时，只有 t2 可以被激发。如果 t2 也被激发了，则权标从 P2 中移出，两个新权标被放在 P3 上，结果 如图 4.8 所示，标记为(2，0，2，0)。 图 6 带标记的 Petri 网 图 7 Petri 网被激发后的情况