系统分析与的设计4形式化说明技术.ppt

对一个系统进行规格说明，通常都需要对有穷状态机做一个很有用的扩展: 即在前述的5元组中加入第6个组件——谓词集P，从而把有穷状态机扩展为一个6元组，其中每个谓词都是系统全局状态Y的函数。转换函数T现在是一个从(J-F)×K×P到J的函数。现在的转换规则形式如下： 当前状态[菜单]+事件[所选择的项]+谓词→下个状态。 4.2.1 概念 用这种技术给出大家熟悉的电梯系统的规格说明。首先给出用自然语言描述的对电梯系统的需求： 在一幢m层的大厦中需要一套控制n部电梯的产品，要求这n部电梯按照约束条件C1，C2和C3在楼层间移动。 C1：每部电梯内有m个按钮，每个按钮代表一个楼层。当按下一个按钮时该按钮指示灯亮，同时电梯驶向相应的楼层，到达按钮指定的楼层时指示灯熄灭。 4.2.2 例子 C2：除了大厦的最低层和最高层之外，每层楼都有两个按钮分别请求电梯上行和下行。这两个按钮之一被按下时相应的指示灯亮，当电梯到达此楼层时灯熄灭，电梯向要求的方向移动。 C3：当对电梯没有请求时，它关门并停在当前楼层。 现在使用一个扩展的有穷状态机对本产品进行规格说明。 4.2.2 例子 这个问题中有两个按钮集。n部电梯中的每一部都有m个按钮，一个按钮对应一个楼层，称它们为电梯按钮。 每层楼有两个按钮，一个请求向上，另一个请求向下，这些按钮称为楼层按钮。 4.2.2 例子 令EB(e,f)表示按下电梯e内的按钮并请求到f层去。EB(e,f)有两个状态： EBON(e,f)：电梯按钮(e,f)打开 EBOFF(e,f)：电梯按钮(e,f)关闭 EBP(e,f)：电梯按钮(e,f)被按下 EAF(e,f)：电梯e到达f层 4.2.2 例子 图4.2 电梯按钮的状态转换图 C1：每部电梯内有m个按钮，每个按钮代表一个楼层。当按下一个按钮时该按钮指示灯亮，同时电梯驶向相应的楼层，到达按钮指定的楼层时指示灯熄灭。 为了定义与这些事件和状态相联系的状态转换规则，需要一个谓词V(e,f)： V(e,f)：电梯e停在f层 则状态转换规则的形式化描述如下： EBOFF(e,f)+EBP(e,f)+not V(e,f)?EBON(e,f) 反之： EBON(e,f)+EAF(e,f) ? EBOFF(e,f) 4.2.2 例子 接下来考虑楼层按钮: 令FB(d,f)表示f层请求电梯向d方向运动的按钮，楼层按钮的状态如下： FBON(d,f)：楼层按钮(d,f)打开 FBOFF(d,f)：楼层按钮(d,f)关闭 FBP(d,f)：楼层按钮(d,f)被按下 EAF(1…n,f)：电梯1或…或n到达f层 其中1…n表示或为1或为2…或为n。 4.2.2 例子 C2：除了大厦的最低层和最高层之外，每层楼都有两个按钮分别请求电梯上行和下行。这两个按钮之一被按下时相应的指示灯亮，当电梯到达此楼层时灯熄灭，电梯向要求的方向移动。 为了定义与这些事件和状态相联系的状态转换规则，同样也需要一个谓词，它是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。 也就是说，如果在f层请求电梯向d方向运动的楼层按钮处于关闭状态，现在该按钮被按下，并且当时没有正停在f层准备向d方向移动的电梯，则该楼层按钮打开。反之，如果楼层按钮已经打开，且至少有一部电梯到达f层，该部电梯将朝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.4是电梯的状态转换图。 3个电梯停止状态S(U,e,f)、S(N,e,f)和S(D,e,f)已被组合成一个大的状态，这样做的目的是减少状态总数以简化流图。 图4.4中包含了下述3个可触发状态发生改变的事件。 DC(e,f)：电梯e在楼层f关上门 ST(e,f)：电梯e靠近f层时触发传感器，电梯控制器决定在当前楼层电梯是否停下 RL：电梯按钮或楼层按钮被按下进入打开状态，登录需求 4.2.