软件工程 第4章 ppt.ppt

第第4 4章章 形式化说明技术形式化说明技术1.有穷状态机有穷状态机2.Petri网网3.Z语言语言 非形式化方法：非形式化方法：用自然语言描述需求规格说明，是典型的非形用自然语言描述需求规格说明，是典型的非形 式化方法。式化方法。半形式化方法：半形式化方法：用数据流图或实体用数据流图或实体-联系图建立模型，是典型的联系图建立模型，是典型的 半形式化方法。半形式化方法。形式化方法：形式化方法：是用基于数学的技术来描述系统性质的方法；是用基于数学的技术来描述系统性质的方法；也就是说，如果一种方法有坚实的数学基础，也就是说，如果一种方法有坚实的数学基础，那么它就是形式化的。那么它就是形式化的。4.1 概述概述 4.1.1 形式化方法的优点形式化方法的优点1）能够简洁准确地描述物理现象、对象或动作的）能够简洁准确地描述物理现象、对象或动作的 结果，因此是结果，因此是理想的建模工具理想的建模工具。2）在软件开发的过程中使用数学可以在不同的软）在软件开发的过程中使用数学可以在不同的软 件工程活动之间件工程活动之间平滑地过渡平滑地过渡。不仅功能规格说。不仅功能规格说 明，而且系统设计也可以用数学表达。明，而且系统设计也可以用数学表达。3）数学作为软件开发工具的最后一个优点是它）数学作为软件开发工具的最后一个优点是它提提 供了高层确认的手段供了高层确认的手段。可以使用数学方法证明，。可以使用数学方法证明，设计符合规格说明，程序代码正确地实现了设设计符合规格说明，程序代码正确地实现了设 计结果。计结果。(1)应该选用适当的表示方法；应该选用适当的表示方法；(2)应该形式化，但不要过分形式化；应该形式化，但不要过分形式化；(3)应该估算成本；应该估算成本；(4)应该有形式化方法顾问随时提供咨询；应该有形式化方法顾问随时提供咨询；(5)不应该放弃传统的开发方法；不应该放弃传统的开发方法；(6)应该建立详尽的文档；应该建立详尽的文档；(7)不应该放弃质量标准；不应该放弃质量标准；(8)不应该盲目依赖形式化方法；不应该盲目依赖形式化方法；(9)应该测试、测试再测试；应该测试、测试再测试；(10)应该重用。应该重用。4.1.2 应用形式化方法的准则应用形式化方法的准则1.通过通过“保险箱开锁保险箱开锁”这个例子介绍有穷状态机的这个例子介绍有穷状态机的 基本概念。基本概念。一个保险箱上装了一个复合锁，锁有三个位置，一个保险箱上装了一个复合锁，锁有三个位置，分别标记为分别标记为1、2、3，转盘可向左，转盘可向左(L)或向右或向右(R)转动。这样，在任意时刻转盘都有转动。这样，在任意时刻转盘都有6种可能的运种可能的运 动，即动，即1L、1R、2L、2R、3L和和3R。保险箱的。保险箱的 组合密码是组合密码是:1L、3R、2L，转盘的任何其他运，转盘的任何其他运 动都将引起报警。动都将引起报警。状态转换情况如表所示：状态转换情况如表所示：4.2 有穷状态机有穷状态机 4.2.1 概念概念图图4.1 保险箱的状态转换图保险箱的状态转换图 一个有穷状态机包括下述一个有穷状态机包括下述 5 个部分：个部分：状态集状态集J 输入集输入集K 由当前状态和当前输入确定下一个状态由当前状态和当前输入确定下一个状态(次态次态)的转换函数的转换函数T、初始态初始态S 终态集终态集F 对于上例，相应的有穷状态机的各部分如下：对于上例，相应的有穷状态机的各部分如下：状态集状态集J：保险箱锁定，：保险箱锁定，A，B，保险箱解锁，报警；，保险箱解锁，报警；输入集输入集K：1L，1R，2L，2R，3L，3R；转换函数转换函数T：如表：如表4.1所示。所示。初始态初始态S：保险箱锁定。：保险箱锁定。终态集终态集F：保险箱解锁，报警。：保险箱解锁，报警。2.可以使用更形式化的术语来描述有穷状态机：可以使用更形式化的术语来描述有穷状态机：一个有穷状态机可以表示为：一个有穷状态机可以表示为：一个一个5元组元组(J，K，T，S，F)，其中：其中：J 是一个有穷的非空状态集；是一个有穷的非空状态集；K是一个有穷的非空输入集；是一个有穷的非空输入集；T 是一个从是一个从(J-F)K到到J的转换函数；的转换函数；SJ，是一个初始状态；，是一个初始状态；FJ，是终态集。，是终态集。3.3.状态转换的形式状态转换的形式:当前状态当前状态 +事件事件 下个状态下个状态4.4.谓词谓词:为了对一个系统进行规格说明，通常都需要对有穷为了对一个系统进行规格说明，通常都需要对有穷 状态机进行很有用的扩展，即在前述的状态机进行很有用的扩展，即在前述的5元组中加元组中加 入第入第 6 个组件个组件谓词集谓词集P，从而把有穷状态机扩展为一个从而把有穷状态机扩展为一个 6 元组，元组，转换函数转换函数T现在是一个从现在是一个从(J-F)K P到到 J 的函数。的函数。现在的转换规则形式如下：现在的转换规则形式如下：当前状态当前状态+事件事件+谓词谓词 下个状态。下个状态。现在用有穷状态机技术给出电梯系统的规格说明：现在用有穷状态机技术给出电梯系统的规格说明：1.1.首先给出用自然语言描述的对电梯系统的需求：首先给出用自然语言描述的对电梯系统的需求：1 1）在一幢在一幢m m层的大厦中需要一套控制层的大厦中需要一套控制n n部电梯的产品，要求部电梯的产品，要求 这这n n部电梯按照约束条件部电梯按照约束条件C1C1，C2C2和和C3C3在楼层间移动；在楼层间移动；2 2）C1C1：每部电梯内有：每部电梯内有m m个按钮，每个按钮代表一个楼层；个按钮，每个按钮代表一个楼层；3 3）C2C2：除了大厦的最低层和最高层之外，每层楼都有两个：除了大厦的最低层和最高层之外，每层楼都有两个 按钮分别请求电梯上行和下行；按钮分别请求电梯上行和下行；4 4）C3C3：当对电梯没有请求时，它关门并停在当前楼层。：当对电梯没有请求时，它关门并停在当前楼层。2.现在使用一个扩展的有穷状态机对本产品进行规格说明现在使用一个扩展的有穷状态机对本产品进行规格说明：1）两个按钮集：）两个按钮集：电梯按钮电梯按钮:EB 楼层按钮楼层按钮:FB 4.2.2 实例实例2）电梯按钮的状态转换图：）电梯按钮的状态转换图：EB(e,f)：表示按下电梯：表示按下电梯 e内的按钮，并请求到内的按钮，并请求到 f层去；层去；EBON(e,f)：电梯按钮：电梯按钮(e,f)打开；打开；EBOFF(e,f)：电梯按钮：电梯按钮(e,f)关闭；关闭；EBP(e,f)：电梯按钮：电梯按钮(e,f)被按下；被按下；EAF(e,f)：电梯：电梯 e到达到达 f 层；层；V(e,f)：为了定义与这些事件和状态相联系的状态转换规则：为了定义与这些事件和状态相联系的状态转换规则 需要一个谓词需要一个谓词V(e,f)，它的含义是：电梯，它的含义是：电梯 e停在停在f层。层。电梯按钮的状态转换规则：电梯按钮的状态转换规则：如果当前状态是：电梯按钮如果当前状态是：电梯按钮(e,f)处于关闭状态；处于关闭状态；事事 件是：电梯按钮件是：电梯按钮(e,f)被按下；被按下；谓谓 词是：电梯词是：电梯 e不在不在 f 层；层；下个状态是：下个状态是：则该电梯按钮打开发光。则该电梯按钮打开发光。状态转换规则的形式化描述如下：状态转换规则的形式化描述如下：1.EBOFF(e,f)+EBP(e,f)+not V(e,f)EBON(e,f)2.EBON(e,f)+EAF(e,f)EBOFF(e,f)3）楼层按钮的状态转换图）楼层按钮的状态转换图 FB(d,f)：表示：表示 f 层请求电梯向层请求电梯向 d方向运动的按钮；方向运动的按钮；FBON(d,f)：楼层按钮：楼层按钮(d,f)打开；打开；FBOFF(d,f)：楼层按钮：楼层按钮(d,f)关闭；关闭；FBP(d,f)：楼层按钮：楼层按钮(d,f)被按下；被按下；EAF(1n,f)：电梯：电梯1或或或或n到达到达 f 层；层；其中其中1n表示或为表示或为1或为或为2或为或为n。S(d,e,f)：是一个谓词，含义是：电梯：是一个谓词，含义是：电梯e停在停在 f 层并且移动方层并且移动方 向由向由 d 确定；确定；d=U：向上：向上，d=D：向下，：向下，d=N：待定：待定 楼层按钮的形式化转换规则为：楼层按钮的形式化转换规则为：如果当前状态是：在如果当前状态是：在 f 层请求电梯向层请求电梯向 d 方向运动的方向运动的 楼层按钮处于关闭状态，楼层按钮处于关闭状态，事事 件是：该楼层按钮被按下，件是：该楼层按钮被按下，谓谓 词是：当时没有正停在词是：当时没有正停在 f 层准备向层准备向 d方方 向移动的电梯，向移动的电梯，下个状态是：下个状态是：则该楼层按钮打开。则该楼层按钮打开。状态转换规则的形式化描述如下：状态转换规则的形式化描述如下：1.FBOFF(d,f)+FBP(d,f)+not S(d,1n,f)FBON(d,f)，2.FBON(d,f)+EAF(1n,f)+S(d,1n,f)FBOFF(d,f)，其中，其中，d=U or D。V(e,f)：讨论电梯按钮状态转换规则时定义的谓：讨论电梯按钮状态转换规则时定义的谓 词，可以用谓词词，可以用谓词 S(d,e,f)重新定义如下：重新定义如下：V(e,f)=S(U,e,f)or S(D,e,f)or S(N,e,f)4）定义电梯的）定义电梯的 3 个状态：个状态：1.M(d,e,f)：电梯：电梯 e正沿正沿 d方向移动，即将到达的是第方向移动，即将到达的是第 f 层；层；2.S(d,e,f)：电梯电梯 e 停在停在 f 层，将朝层，将朝 d方向移动方向移动(尚未关门尚未关门)；3.W(e,f)：电梯电梯 e 在在 f 层等待层等待(已关门已关门)。5）电梯中可触发状态发生改变的事件：电梯中可触发状态发生改变的事件：1.DC(e,f)：电梯电梯 e 在楼层在楼层 f 关上门；关上门；2.ST(e,f)：电梯电梯 e 靠近靠近 f 层时触发传感器，电梯控制器决定层时触发传感器，电梯控制器决定 在当前楼层电梯是否停下；在当前楼层电梯是否停下；3.RL：电梯按钮或楼层按钮被按下进入打开状态，登录需求：电梯按钮或楼层按钮被按下进入打开状态，登录需求6）电梯的状态转换图）电梯的状态转换图 S(d,e,f)：由：由 S(U,e,f)、S(N,e,f)和和 S(D,e,f)组合；组合；电梯的状态转换规则：电梯的状态转换规则：（为简单起见，这里给出的规则仅发生在关门之时）（为简单起见，这里给出的规则仅发生在关门之时）1.S(U,e,f)+DC(e,f)M(U,e,f+1)2.S(D,e,f)+DC(e,f)M(D,e,f-1)3.S(N,e,f)+DC(e,f)W(e,f)有穷状态机方法描述规格说明的格式为：有穷状态机方法描述规格说明的格式为：当前状态当前状态+事件事件+谓词谓词下个状态下个状态优点：优点：这种格式，易于书写，易于验证，易于理这种格式，易于书写，易于验证，易于理 解，易于将其转变澄设计解，易于将其转变澄设计 or 代码。代码。缺点：缺点：在开发一个大系统时，三元组在开发一个大系统时，三元组(即状态、即状态、事件、谓词事件、谓词)的数量会迅速增长。的数量会迅速增长。没有处理定时需求。没有处理定时需求。4.2.3 评价评价1.简介简介 Petri网是由网是由Carl Adam Petri发明的，在计算机科学发明的，在计算机科学 中得到广泛的应用。中得到广泛的应用。2.Petri网的组成网的组成4.3 Petri网网4.3.1 概念概念1）4种元素种元素 一组位置一组位置P P、一组转换、一组转换T T、输入函数、输入函数I I以及输出函数以及输出函数O O；上图中：上图中：一组位置一组位置P P为为P1P1，P2P2，P3P3，P4P4，在图中用圆圈代表位置；，在图中用圆圈代表位置；一组转换一组转换T T为为t1t1，t2t2，在图中用短直线表示转换；，在图中用短直线表示转换；两个用于转换的输入函数，用由位置指向转换的箭头表示：两个用于转换的输入函数，用由位置指向转换的箭头表示：I(t1)=I(t1)=P2P2，P4P4，I(t2)=I(t2)=P2P2 两个用于转换的输出函数，用由转换指向位置的箭头表示；两个用于转换的输出函数，用由转换指向位置的箭头表示；O(t1)=O(t1)=P1P1，O(t2)=O(t2)=P3P3，P3P3 注意：输出函数注意：输出函数O(t2)O(t2)中有两个中有两个P3P3，是因为有两个箭头由，是因为有两个箭头由t2t2指指 向向P3P3。2 2）更形式化的）更形式化的PetriPetri网结构网结构 是一个是一个四元组四元组C=(P,T,I,O)C=(P,T,I,O)；其中，；其中，P=P=P1P1，PnPn，是一个有穷位置集，是一个有穷位置集，n0n0；T=T=t1t1，tmtm，是一个有穷转换集，是一个有穷转换集，m0m0，且且T T和和P P不相交；不相交；I I：TPTP为输入函数，是由位置到无序单位组的映射；为输入函数，是由位置到无序单位组的映射；O O：TPTP为输出函数，是由转换到位置无序单位组的映射。为输出函数，是由转换到位置无序单位组的映射。3）Petri网的标记网的标记 指的是在指的是在Petri网中权标网中权标(token)的分配。的分配。图图4.6 带标记的带标记的Petri网网 上述标记可以用向量上述标记可以用向量(1，2，0，1)表示。表示。Petri网中权标总数不是固定的网中权标总数不是固定的 图图4.6 的的Petri网在转换网在转换t1被激发后的情况被激发后的情况 上述标记可以用向量上述标记可以用向量(2，1，0，0)表示。表示。上述标记可以用向量上述标记可以用向量(2，0，2，0)表示；表示；图图4.7 Petri网在转换网在转换t2被激发后的情况被激发后的情况4）带有标记的）带有标记的Petri网网 更形式化地说，更形式化地说，Petri网网C=(P，T，I，O)中的标记中的标记M，是由，是由 一组位置一组位置P到一组非负整数的映射：到一组非负整数的映射：M：P0，1，2，这样，带有标记的这样，带有标记的Petri网成为一个五元组：网成为一个五元组：(P，T，I，O，M)。5）Petri网的扩充网的扩充 Petri网的一个重要扩充是：加入禁止线。网的一个重要扩充是：加入禁止线。禁止线禁止线:是用一个小圆圈而不是用箭头标记的输入线。是用一个小圆圈而不是用箭头标记的输入线。上图中转换上图中转换 t1是可以被激发的。是可以被激发的。1.1.首先给出用自然语言描述的对电梯系统的需求：首先给出用自然语言描述的对电梯系统的需求：1 1）在一幢在一幢m m层的大厦中需要一套控制层的大厦中需要一套控制n n部电梯的产品，要求部电梯的产品，要求 这这n n部电梯按照约束条件部电梯按照约束条件C1C1，C2C2和和C3C3在楼层间移动；在楼层间移动；2 2）C1C1：每部电梯内有：每部电梯内有m m个按钮，每个按钮代表一个楼层；个按钮，每个按钮代表一个楼层；3 3）C2C2：除了大厦的最低层和最高层之外，每层楼都有两个：除了大厦的最低层和最高层之外，每层楼都有两个 按钮分别请求电梯上行和下行；按钮分别请求电梯上行和下行；4 4）C3C3：当对电梯没有请求时，它关门并停在当前楼层。：当对电梯没有请求时，它关门并停在当前楼层。2.现在使用现在使用Petri网技术对本产品进行规格说明网技术对本产品进行规格说明：4.3.2 实例实例当用当用Petri网表示电梯系统的规格说明时，网表示电梯系统的规格说明时，每个楼层用一个位置每个楼层用一个位置 Ff 表示表示(1fm)，电梯是用一个权标表示，电梯是用一个权标表示，在位置在位置 Ff 上有权标，表示在楼层上有权标，表示在楼层f上有电梯。上有电梯。1.电梯按钮电梯按钮1）约束条件约束条件C1:每部电梯内有每部电梯内有m m个按钮，每个按钮代表一个楼个按钮，每个按钮代表一个楼 层；层；2）描述电梯按钮的行为描述电梯按钮的行为:3）在在Petri网中设置的其他位置：网中设置的其他位置：电梯中楼层电梯中楼层 f 的按钮，用位置的按钮，用位置EBf表示表示(1fm)。若在若在EBf上有一个权标，就表示电梯内楼层上有一个权标，就表示电梯内楼层f的按钮被按下了。的按钮被按下了。4.3.2 实例实例3）用用Petri网表示的电梯按钮网表示的电梯按钮4）时限问题时限问题3）用用Petri网表示的电梯按钮网表示的电梯按钮4）时限问题时限问题2.楼层按钮楼层按钮1）约束条件约束条件C2:除了大厦的最低层和最高层之外，每层楼除了大厦的最低层和最高层之外，每层楼 都有两个按钮分别请求电梯上行和下行；都有两个按钮分别请求电梯上行和下行；2）描述楼层按钮的行为描述楼层按钮的行为:3）在在Petri网中楼层按钮的用位置网中楼层按钮的用位置FBfu和和FBfd表示：表示：FBfu:代表代表 f 楼层请求电梯上行的按钮（楼层请求电梯上行的按钮（1fm）；FBfd:代表代表 f 楼层请求电梯下行的按钮（楼层请求电梯下行的按钮（1fm）；FB1u:最底层的按钮；最底层的按钮；FBmd:最高层的按钮；最高层的按钮；4）用用Petri网表示楼层按钮：网表示楼层按钮：图图4.11 Petri网表示楼层按钮网表示楼层按钮2.楼层按钮楼层按钮5）第三条约束第三条约束C3：当对电梯没有请求时，它关门当对电梯没有请求时，它关门 并停在当前楼层。并停在当前楼层。用用Z语言描述的、最简单的形式化规格说明含有下语言描述的、最简单的形式化规格说明含有下述述4个部分：个部分：1）给定的集合、数据类型及常数）给定的集合、数据类型及常数2）状态定义）状态定义3）初始状态）初始状态4）操作）操作4.4 Z语言语言 1.简介简介1.基于数学的形式化规格说明技术，目前还没有在软件产业界基于数学的形式化规格说明技术，目前还没有在软件产业界 广泛应用，但是，与欠形式化的方法比较起来，它确实有实广泛应用，但是，与欠形式化的方法比较起来，它确实有实 质性的优点：质性的优点：1）可以用数学方法研究、验证；）可以用数学方法研究、验证；2）消除了二义性；）消除了二义性；3）减少差错。）减少差错。2.形式化方法也有缺点：形式化方法也有缺点：1）主要关注于系统的功能和数据；）主要关注于系统的功能和数据；2）而问题的时序、控制和行为等方面的需求却更难于表示；）而问题的时序、控制和行为等方面的需求却更难于表示；3）难于学习。）难于学习。3.The best,把形式化方法和欠形式化方法有机地结合起来，使把形式化方法和欠形式化方法有机地结合起来，使 它们取长补短，应该能获得更理想的效果。它们取长补短，应该能获得更理想的效果。4.5 小结小结