4_形式化说明技术.ppt

为了定义与这些事件和状态相联系的状态转换规则，同样也需要一个谓词，它是S(d,e,f)，它的定义如下: S(d,e,f)：电梯e停在f层并且移动方向由d确定为向上(d=U)或向下(d=D)或待定(d=N)。 4.2.2 例子 使用谓词S(d,e,f)，形式化转换规则为： FBOFF(d,f)+FBP(d,f)+notS(d,1…n,f)?FBON(d,f) 反之 FBON(d,f)+EAF(1…n,f)+S(d,1…n,f)?FBOFF(d,f) 其中，d=U or D。 4.2.2 例子 在讨论电梯按钮状态转换规则时定义的谓词V(e,f)，可以用谓词S(d,e,f)重新定义如下： V(e,f)=S(U,e,f)or S(D,e,f)or S(N,e,f) 电梯的状态及其转换规则: 一个电梯状态实质上包含许多子状态,下面定义电梯的3个状态： M(d,e,f)：电梯e正沿d方向移动，即将到达的是第f层 S(d,e,f)：电梯e停在f层，将朝d方向移动(尚未关门) W(e,f)：电梯e在f层等待(已关门) 4.2.2 例子 4.2.2 例子 图4.4 电梯的状态转换图 图4.4中包含了下述3个可触发状态发生改变的事件。 DC(e,f)：电梯e在楼层f关上门 ST(e,f)：电梯e靠近f层时触发传感器，电梯控制器决定在当前楼层电梯是否停下 RL：电梯按钮或楼层按钮被按下进入打开状态，登录需求 4.2.2 例子 最后，给出电梯的状态转换规则。为简单起见，这里给出的规则仅发生在关门之时。 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) 4.2.2 例子 4.2.3 评价 有穷状态机方法描述规格说明： 当前状态+事件+谓词?下个状态 优点： 规格说明易于书写、易于验证，而且可以比较容易地把它转变成设计或程序代码。有穷状态机方法比数据流图技术更精确，而且和它一样易于理解。 缺点： 在开发一个大系统时三元组(即状态、事件、谓词)的数量会迅速增长。此外，和数据流图方法一样，形式化的有穷状态机方法也没有处理定时需求。 第4章 形式化说明技术 4.1 概述 4.2 有穷状态机 4.3 Petri网 4.4 Z语言 4.3 Petri网 4.3.1 概念 并发系统中需要解决的主要问题是定时问题：包括同步问题、竞争条件以及死锁问题。 定时问题常常是因不好的设计或有错误的实现引起的，归根到底又是由不好的规格说明造成的. Petri网技术可用于确定系统中隐含的定时问题。 Petri网技术在计算机领域应用较多，已经证明，用Petri网可以有效地描述并发活动。 Petri网包含4种元素： 一组位置P 一组转换T 输入函数I 输出函数O 4.3.1 概念 位置 转换 输入 输出 如图举例说明了Petri网的组成： 一组位置P为｛P1，P2，P3，P4｝：用圆圈代表； 一组转换T为｛t1，t2｝：图中用短直线表示转换；两个用于转换的输入函数，用由位置指向转换的箭头表示，它们是：I(t1)=｛P2，P4｝ I(t2)=｛P2｝ 两个用于转换的输出函数，用由转换指向位置的箭头表示，它们是：O(t1)=｛P1｝ O(t2)=｛P3，P3｝ Petri网是一个四元组C=(P，T，I，O)，其中： P={P1,P2,…Pn}是一个有穷位置集，n≥0； T=(t1,…,tm)是一个有穷转换集，m≥0,且T和不相交； I:T→P∞为输入函数，是由转换到位置无序单位组的映射； O:T→P∞为输出函数，是由转换到位置无序单位组的映射。 4.3.1 概念 带标记的Petri网： 权标(token)的分配。如图中有4个权标 上述标记可以用向量(1，2，0，1)表示。 由于P2和P4中有权标，因此t1启动(即被激发)。 通常，当每个输入位置所拥有的权标数大于等于从该位置到转换的线数时，就允许转换。当t1被激发时，P2和P4上各有一个权标被移出，而P1上则增加一个权标（2，1，0，0）。 Petri网中权标总数不是固定的，在这个例子中两个权标被移出，而P1上只能增加一个权标。 4.3.1 概念 权标数 如图，P2上有权标，因此t2也可以被激发。当t2被激发时，P2上将移走一个权标，而P3上新增加两个权标（1，1，2，1）。 4.3.1 概念 Petri网具有非确定性，如果数个转换都达到了激发条件，则其中任意一个都可以被激发。图4.6所示Petri网的标记为(1，2，0，1)，t1和t2都可以被激发。 4.3.1 概念 假设t1被激发了，标记