形式化说明技术剖析

1、形式化说明技术剖析 第四章形式化说明技术 本堂课讲授重点 一、有穷状态机 二、Petri网 （4学时） 返回 形式化说明技术剖析 软件需求的说明技术 n非形式化：用自然语言描述需求规格说 明。比如，应力分析程序必须在一分种 之内生产任何一个梁的应力报告。 n半形式化：用数据流图、实体-联系图建 立模型。 n形式化方法：使用具有坚实的数学基础 的工具来描述系统性质。 形式化说明技术剖析 非形式化方法的缺点 n矛盾：是指一组相互冲突的陈述。 n二义性：是指读者可以用不同方式来理 解。 n含糊性：比如，友好的界面、很高的安 全性 n不完整性 n抽象层次混乱 形式化说明技术剖析 形式化方法的优点 n由

2、于逻辑的严密性，它能够简洁准确地 描述物理现象、对象或动作的结果。比 如，关系代数里面的联结运算。 n在不同的软件工程活动之间平滑地过渡 n可以使用数学方法证明，设计符合规格 说明，程序代码正确地实现了设计结果。 形式化说明技术剖析 应用形式化方法的准则 n应该选用适当的表示方法 n应该形式化，但不要过分形式化 n应该估算成本 n应该有形式化方法顾问随时提供咨询 n不应该放弃传统的开发方法 n应该建立详尽的文档 n不应该放弃质量标准 n不应该盲目依赖形式化方法 n应该测试、测试再测试 n应该重用 形式化说明技术剖析 有穷状态机的形式定义 n有穷状态机是一个5元组(J，K，T，S，F)，其 中：

3、 J是一个有穷的非空状态集，在任一确定的时 刻，只能处于一个确定的状态； K是一个有穷的非空输入集，在任一确定的时 刻，只能接收一个确定的输入； T是一个从(J-F)K到J的转换函数； SJ，是初始状态，由此状态开始接收输入； FJ，是终态集，到达终态后不再接收输入。 形式化说明技术剖析 有穷状态机的表示方法 n状态转换表:用表格的行表示状态机所处的当前状态， 列表示当前的输入，行列交叉处表示要到达的下一个 状态。 n状态转换图：用结点（圆圈，矩形或圆角矩形）表示 状态，将存在转换关系的状态用有向弧连接，并标注 相应的输入字符在有向弧旁，用标有箭头的结点表示 初始状态，终结状态集中的状态用双圈

4、表示。 n状态转移矩阵：用行表示状态机所处的当前状态，列 表示将要到达的下一个状态，行列交叉处表示输入字 符。 形式化说明技术剖析 有穷状态机的例子 n一个保险箱上装了一个复合锁，锁有三 个位置，分别标记为1、2、3，转盘可向 左(L)或向右(R)转动。这样，在任意时刻 转盘都有6种可能的运动，即1L、1R、2L、 2R、3L和3R。保险箱的组合密码是1L、 3R、2L，转盘的任何其他运动都将引起 报警。图4.1描绘了保险箱的状态转换情 况。 形式化说明技术剖析 图4.1 保险箱的状态转换图 形式化说明技术剖析 用有穷状态机描述的保险箱 n状态集J：保险箱锁定，A，B，保险箱 解锁，报警 n输

5、入集K：1L，1R，2L，2R，3L，3R n状态转换函数T：如表4.1所示 n初始态S：保险箱锁定 n终态集F：保险箱解锁，报警 形式化说明技术剖析 试描述下面的有穷状态机 n给出一个有穷状态机M （q0,q1,q2,q3,0,1,t, q0,q0）,其中状 态转换函数t的定义如下： t(q0,1)= q1, t(q0,0)= q2, t(q1,1)= q0, t(q1,0)= q3, t(q2,1)= q3, t(q2,0)= q0, t(q3,1)= q2, t(q3,0)= q1 形式化说明技术剖析 状态转换表 输入 次态 当前状态 01 q0q2q1 q1q3q0 q2q0q3 q3

6、q1q2 形式化说明技术剖析 状态转换图 q0 q1 q2q3 1 1 1 1 0 0 00 形式化说明技术剖析 状态转换矩阵 q0q1q2q3 q0 q1 q2 q3 10 1 1 1 0 0 0 形式化说明技术剖析 有穷状态机的扩展 n状态的每个转换都具有下面的形式： 当前状态+事件下个状态 n有时候需要对有穷状态机做一个很有用的扩展， 即在前述的5元组中加入第6个组件谓词集 P，从而把有穷状态机扩展为一个6元组，其中 每个谓词都是系统全局状态Y的函数。转换函 数T现在是一个从(J-F)KP到J的函数。 n现在的转换规则形式如下： 当前状态+事件+谓词下个状态 形式化说明技术剖析 电梯控制

7、系统 n在一幢m层的大厦中需要一套控制n部电梯的产品，要 求这n部电梯按照约束条件C1，C2和C3在楼层间移动。 C1：每部电梯内有m个按钮，每个按钮代表一个 楼层。当按下一个按钮时该按钮指示灯亮，同时电梯 驶向相应的楼层，到达按钮指定的楼层时指示灯熄灭。 C2：除了大厦的最低层和最高层之外，每层楼都 有两个按钮分别请求电梯上行和下行。这两个按钮之 一被按下时相应的指示灯亮，当电梯到达此楼层时灯 熄灭，电梯向要求的方向移动。 C3：当对电梯没有请求时，它关门并停在当前楼 层。 形式化说明技术剖析 控制系统的三大组成部分 n电梯按钮： n楼层按钮： n电梯本身： 形式化说明技术剖析 电梯按钮的状

8、态转换图 令令EB(e,f)表示按下电梯表示按下电梯e内的按钮并请求到内的按钮并请求到f层去。层去。 EB(e,f)有两个状态，分别是按钮发光有两个状态，分别是按钮发光(打开打开)和不发光和不发光 (关闭关闭)。更精确地说，状态是：。更精确地说，状态是： EBON(e,f)：电梯按钮：电梯按钮(e,f)打开打开 EBOFF(e,f)：电梯按钮：电梯按钮(e,f)关闭关闭 如果电梯按钮如果电梯按钮(e,f)发光且电梯到达发光且电梯到达f层，该按钮将熄层，该按钮将熄 灭。相反如果按钮熄灭，则按下它时，按钮将发光。灭。相反如果按钮熄灭，则按下它时，按钮将发光。 上述描述中包含了两个事件，它们分别是：

9、上述描述中包含了两个事件，它们分别是： EBP(e,f)：电梯按钮：电梯按钮(e,f)被按下被按下 EAF(e,f)：电梯：电梯e到达到达f层层 形式化说明技术剖析 图图4.2 电梯按钮的状态转换图电梯按钮的状态转换图 形式化说明技术剖析 状态转换规则 为了定义与这些事件和状态相联系的状态转换规则， 需要一个谓词V(e,f)，它的含义如下： V(e,f)：电梯e停在f层 如果电梯按钮(e,f)处于关闭状态当前状态，而且 电梯按钮(e,f)被按下事件，而且电梯e不在f层 谓词，则该电梯按钮打开发光下个状态。状 态转换规则的形式化描述如下： EBOFF(e,f)+EBP(e,f)+not V(e,

10、f)EBON(e,f) 反之，如果电梯到达f层，而且电梯按钮是打开的，于 是它就会熄灭。这条转换规则可以形式化地表示为： EBON(e,f)+EAF(e,f)EBOFF(e,f) 形式化说明技术剖析 楼层按钮的状态转换图 n令FB(d,f)表示f层请求电梯向d方向运动的按钮，楼层 按钮的状态如下： FBON(d,f)：楼层按钮(d,f)打开 FBOFF(d,f)：楼层按钮(d,f)关闭 如果楼层按钮已经打开，而且一部电梯到达f层，则按 钮关闭。反之，如果楼层按钮原来是关闭的，被按下 后该按钮将打开。这段叙述中包含了以下两个事件： FBP(d,f)：楼层按钮(d,f)被按下 EAF(1n,f)：

11、电梯1或或n到达f层 其中1n表示或为1或为2或为n。 形式化说明技术剖析 为了定义与这些事件和状态相联系的状态转换规则， 同样也需要一个谓词，它是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)FBON(d,f) FBON(d,f)+EAF(1n,f)+S(d,1n,f)FBOFF(d,f) 其中，d=UorD。 形式化说

12、明技术剖析 图图4.3楼层按钮的状态转换图楼层按钮的状态转换图 形式化说明技术剖析 电梯的状态及其转换规则 电梯的3个状态： M(d,e,f)：电梯e正沿d方向移动，即将到达的是第f层 S(d,e,f)：电梯e停在f层，将朝d方向移动(尚未关门) W(e,f)：电梯e在f层等待(已关门) 3个可触发状态发生改变的事件。 DC(e,f)：电梯e在楼层f关上门 ST(e,f)：电梯e靠近f层时触发传感器，电梯控制器决 定在当前楼层电梯是否停下 RL：电梯按钮或楼层按钮被按下进入打开状态，登录 需求 形式化说明技术剖析 这里给出的规则仅发生在关门之时。 S(U,e,f)+DC(e,f)M(U,e,f

13、+1) S(D,e,f)+DC(e,f)M(D,e,f-1) S(N,e,f)+DC(e,f)W(e,f) 形式化说明技术剖析 图图4.4 电梯的状态转换图电梯的状态转换图 形式化说明技术剖析 有穷状态机方法采用了一种简单的格式来描述 规格说明： 当前状态+事件+谓词下个状态 这种形式的规格说明易于书写、易于验证，而 且可以比较容易地把它转变成设计或程序代码。 可以开发一个CASE工具把一个有穷状态机规格 说明直接转变为源代码。维护可以通过重新转 变来实现，也就是说，如果需要一个新的状态 或事件，首先修改规格说明，然后直接由新的 规格说明生成新版本的产品。 形式化说明技术剖析 P79 第三题

14、n该有穷状态机的初态是“等待字符串输 入”。在初态若接收到字符+、或者字符 -、或者二进制位，则进入“输入尾数” 状态；在初态若接收到其他字符，则进 入终态“非浮点二进制 数”。 n有穷状态机如下图： 形式化说明技术剖析 初态 终态终态 等待字 符串输入 输入 尾数 等待输 入指数 输入 指数 +或-或 二进制位 E +或-或 二进制位 非浮点二进制数 浮点二 进制数 其他 字符 其他 字符 其他 字符 其他 字符 输入 结束 二进制位 二进制位 形式化说明技术剖析 Petri网 n并发系统中遇到的一个主要问题是定时问题。 这个问题可以表现为多种形式，如冲突、死锁 等问题。有穷状态机不能处理定

15、时需求。 nPetri网是由德国的Carl Adam Petri发明的，适 合于并发、异步、分布式软件系统规格说明。 n用Petri网描述的系统有一个共同的特征：系统 的动态行为表现为资源（物质资源和信息资源） 的流动。 形式化说明技术剖析 生产流水线 n一个典型的物质资源流动：半成品在流水线上移动， 每个生产环节再组装上一两个部件，直到产出成品。 显然，生产环节是系统中的转换元素（T元素），代表 半成品、部件等存放位置的是位置元素（P元素） . . . . . p1 p4 p5 p6 p2 p3 p0 t1 t1 2 4 P1， p2， p3：半成品 P4， p6：部件 P5：螺丝钉 P0：

16、工具 T1， t2：组装环节 形式化说明技术剖析 Petri网例子 n Petri网包含4种元素：一组位置P、一组转换T、输入函数I以及输 出函数O。 一组位置P为P1，P2，P3，P4，在图中用圆圈代表位置。 一组转换T为t1，t2，在图中用短直线表示转换。 两个用于转换的输入函数，用由位置指向转换的箭头表示，它们 是： I(t1)=P2，P4 I(t2)=P2 两个用于转换的输出函数，用由转换指向位置的箭头表示，它们 是： O(t1)=P1 O(t2)=P3，P3 形式化说明技术剖析 Petri网的组成 图4.5 形式化说明技术剖析 Petri网结构的定义 形式化的Petri网结构，是一个

17、四元组C=(P,T,I,O)。 其中， P=P1，Pn是一个有穷位置集，n0。 T=t1，tm是一个有穷转换集，m0， 且T和P不相交。 I：TP为输入函数，是由转换到位置无序单位 组(bags)的映射。 O：TP为输出函数，是由转换到位置无序单 位组的映射。 形式化说明技术剖析 Petri网的标记 n前面给出的Petri网是系统的结构框架，是 静态的。只有在结构框架上加上系统中流 动的资源才能构成一个真正的Petri网。 nPetri网的标记是在Petri网中权标(token) 的分配。在图4.6中有4个权标，其中一个 在P1中，两个在P2中，P3中没有，还有 一个在P4中。上述标记可以用向

18、量(1，2， 0，1)表示。 形式化说明技术剖析 带标记的Petri网 图4.6 形式化说明技术剖析 转换的激发 n当每个输入位置所拥有的权标数大于等 于从该位置到转换的线数时，就允许转 换。 n由于P2和P4中有权标，因此t1启动(即被 激发)。 P2和P4上各有一个权标被移出， 而P1上则增加一个权标。Petri网中权标 总数不是固定的，在这个例子中两个权 标被移出，而P1上只能增加一个权标。 形式化说明技术剖析 t1被激发后的情况 图4.7 形式化说明技术剖析 n图4.6所示Petri网的标记为(1，2，0，1) nt1被激发了，则结果如图4.7所示，标记 为(2，1，0，0)。 n只有

19、t2可以被激发。如果t2也被激发了， 则权标从P2中移出，两个新权标被放在 P3上，结果如图4.8所示，标记为(2，0， 2，0)。 形式化说明技术剖析 t2被激发后的情况 图图4.8 形式化说明技术剖析 带有标记的Petri网 n带有标记的Petri网实际上是一个五元组 (P，T，I，O，M)。 标记M，是由一组位置P到一组非负整数 的映射： M：P0，1，2， 形式化说明技术剖析 Petri网丰富的结构描述能力 n顺序关系 n并发关系 n冲突关系 n死锁 形式化说明技术剖析 顺序关系 n设M为某Petri网的一个标记，存在两个转 换t1 和t2，在M标记下， t1可以激发， t2 不能激发，并且t1的激发会使t2激发，则 称t1和t2在M下有顺序关系。 . p1 t1 t2 p2 p3 形式化说明技术剖析 并发关系 n设M为某Petri网的一个标记，存在两个转换t1 和t2，在M标记下， t1和 t2都可以激发 ，并且它 们当中任何一个转换的激发都不会使另一个转 换不能激发，则称t1和t2在M下有并发关系。 . p1 p2 t1 . p3 p4 t2 t