《(cen)第七章形式化方法与需求工程》由会员分享，可在线阅读，更多相关《(cen)第七章形式化方法与需求工程（67页珍藏版）》请在金锄头文库上搜索。
1、第七章 形式化方法与需求工程,7.1 形式化方法介绍 7.1.1 形式化方法在需求中的应用 形式化的需求规格说明由严格的数学符号及由符号组成的规则形成的规格说明。 形式化规格说明的优点 : 通过形式化能减少规格说明完成后的错误； 利用数学的方法进行分析，可以证明规格说明的正确性，或判断多个规格说明间的等价性； 形式化规格说明可用计算机处理。,7.1.2 形式化方法概述 一、非形式化方法的缺点 非形式化是指用自然语言描述软件需求（如系统规格说明书）。因此，可能存在矛盾性、二义性、含糊性、不完整性、抽象层次混乱等问题。 （）矛盾性 在需求规格说明书（Reqirement Specification
2、s）中对同一问题前后存在不同的描述。 （）二义性 需求规格说明书的读者对其中同一问题的描述存在不同的理解。 （）含糊性 需求规格说明书中对某一问题的描述不清晰、不可理解、不知如何实现、不具可操作性。,（）不完整性 需求规格说明书中对某一问题的描述不完整。只说明了局部，没有说明整体；或者只说明了概要，未说明细节。因此不具可操作性。 （）抽象层次混乱 在不同层次的抽象模型中内容混乱，如在高层模型中混有底层细节，造成读者不能理解系统的整体功能和下级功能。,二、形式化方法的优点 形式化方法是指在软件工程中引入数学方法和模型。利用数学的简洁性、严谨性、科学性，克服非形式化方法的缺点。 （）可严谨地描述软
3、件需求中的问题 可简洁、准确描述物理现象、对象或动作的结果问题；适用于描述详细的需求规格；可用数学方法验证需求。 （）可在软件工程不同阶段平滑过渡 从需求、到设计、到实现都基于同一系统模型，平滑过渡。 （）可提供高层确认手段 可用数学方法证明软件工程各阶段的正确性（可回溯性），如“设计”符合“规格说明”、“编码实现”符合“设计”。,形式化方法的适用性问题 形式化方法能较好地解决需求的“二义性”、“含糊性”问题。但不能解决需求的矛盾性、完整性等问题，这些问题涉及工程管理。 三、应用形式化方法的准则 “软件需求”是软件产品的高层、概念模型，而“形式化方法”是严谨、科学的数学方法，因此，在形式化方法
4、的应用方面应考虑适度性、实用性、实用性。,应该选用适当的规格说明表示方法 应该形式化，但不要过分形式化 应该估算推行形式化的成本 应该有形式化方法顾问随时提供咨询 应该结合传统的、证明有效的开发方法 应该在采用形式化的同时，建立详尽的文档 应该坚持质量保障活动 应该不总是盲目依赖形式化方法 应该重视测试 应该重视重用,常用的形式化方法 较严格的形式化方法（语法和语义都严谨）：有穷状态机、Petri网、Z语言 半形式化方法（语法和语义都不太严谨） ：系统流程图、数据流图、数据字典、ER图、数据库范式、状态转换图、层次方框图、Warnier图、IPO图、IPO表,7.2 有穷状态机 一、有穷状态机
5、概念 通过下面的简单例子引入有穷状态机的基本概念： 一个保险箱上装了一个复合锁，锁有三个位置，分别标记为 1 、 2 、 3 ，转盘可向左 (L) 或向右 (R) 转动。这样，在任意时刻转盘都有 6 种可能的运动，即 1L 、 1R 、 2L 、 2R 、 3L 和 3R 。保险箱的组合密码是 1L 、 3R 、 2L ，转盘的任何其他运动都将引起报警。,保险箱的状态转换图如下：,保险箱的状态转换表,一个有穷状态机包括下述 5 个部分：状态集 J 、输入集 K 、由当前状态和当前 输入确定下一个状态 ( 次态 ) 的转换函数T 、初始态 S 和 终态集 F 。 状态集 J ：由所有可能的状态构
6、成的有穷集合； 输入集 K：引发状态变换的可能的外部输入（或操作）； 转换函数T：由当前状态和当前 输入变换到下一个状态 ( 次态 ) 的函数（或规则）； 初始态 S J ，状态机的初始状态； 终态集 F J ，状态机的终止状态集；,例：保险箱的有穷状态机 （）状态集 J ： 保险箱锁定， A ， B ，保险箱解锁，报 警。 （）输入集 K ： 1L ， 1R ， 2L ， 2R ， 3L ， 3R 。 （）转换函数 T ： 见“状态转换表” （）初始态 S ： 保险箱锁定 （）终态集 F ： 保险箱解锁，报警,二、有穷状态机的形式化表示,、一个有穷状态机可以表示为一个 5 元组 (J，K，T
7、，S，F) ，其中： J 是一个有穷的非空状态集； K 是一个有穷的非空输入集； T 是一个从 (J-F) K 到 J 的转换函数； S J ，是一个初始状态； F J ，是终态集。,、扩展的有穷状态机增加谓词集,一个有穷状态机可以表示为一个 6 元组 (J, K, P, T, S, F) ，其中： J 是一个有穷的非空状态集； K是一个有穷的非空输入集； P是一个有穷的非空谓词集(条件函数集合)； T 是一个从 (J-F)KP 到 J 的转换函数； S J ，是一个初始状态； F J ，是终态集。,三、有穷状态机实例：电梯控制系统,(A) 自然语言描述的对电梯系统的需求,在一幢 m 层的大厦
8、中需要一套控制 n 部电梯的产品，要求这 n 部电梯按照约束条件 C1 ， C2 和 C3 在楼层间移 动。 C1 ：每部电梯内有 m 个按钮，每个按钮代表一个楼层。当按下一个按钮时该按钮指示灯亮，同时电梯驶向相应的楼层，到达按钮指定的楼层时指示灯熄灭。 C2 ：除了大厦的最低层和最高层之外，每层楼（电梯外）都有两个按钮分别请求电梯上行和下行。这两个按钮之一被按下时相应的指示灯亮，当电梯到达此楼层时灯熄灭，电梯向要求的方向移动。 C3 ：当对电梯没有请求时，它关门并停在当前楼层。,(B)电梯系统有穷状态机的按钮集,现在使用一个扩展的有穷状态机对本产品进行规格说 明。这个问题中有两个按钮集： n
9、 部电梯中的每一部都 有 m 个按钮，一个按钮对应一个楼层。因为这 m n 个 按钮都在电梯中，所以称它们为电梯按钮。 此外，每层楼有两个按钮，一个请求向上，另一个请求向下，这些按钮称为楼层按钮。,(C)电梯按钮的状态转换,令 EB(e,f) 表示按下电梯 e 内的按钮并请求到 f 层去。 EB(e,f) 有两个状态， 分别是按钮发光( 打开 ) 和不发光 ( 关闭 ) ，状态是： EBON(e,f) ：电梯按钮 (e,f) 打开 EBOFF(e,f) ：电梯按钮 (e,f) 关闭 如果电梯按钮 (e,f) 发光且电梯到达 f 层，该按钮将熄灭。相反如果按钮熄灭，则按下它时，按钮将发光。 上述
10、描述中包含了两个事件，它们分别是： EBP(e,f) ：电梯按钮 (e,f) 被按下 EAF(e,f) ：电梯 e 到达 f 层,电梯按钮状态转换的相关谓词如下:,为了定义与这些事件和状态相联系的状态转换规则，需要一个谓词 V(e,f) ，它的含义如下： V(e,f) ：电梯 e 停在 f 层 如果电梯按钮 (e,f) 处于关闭状态当前状态，而且电梯按钮 (e,f) 被按下事件，而且电梯 e 不在 f 层谓 词，则该电梯按钮打开发光下个状态。状态转 换规则的形式化描述如下： EBOFF(e,f)+EBP(e,f)+not V(e,f) = EBON(e,f) 反之，如果电梯到达 f 层，而且电
11、梯按钮是打开的，于是它就会熄灭。这条转换规则可以形式化地表示为： EBON(e,f)+EAF(e,f) = EBOFF(e,f),(D)楼层按钮的状态转换,(1)令 FB(d,f) 表示 f 层请求电梯向 d 方向运动的按钮，楼层按钮 FB(d,f) 的状态转换图如图 所示。楼层按钮的状态如下： FBON(d,f) ：楼层按钮 (d,f) 打开 FBOFF(d,f) ：楼层按钮 (d,f) 关闭 (2)如果楼层按钮已经打开，而且一部电梯到达 f 层，则按钮关闭。反之，如果楼层按钮原来是关闭的，被按下后该按钮将打开。这段叙述中包含了以下两个事件。 FBP(d,f) ：楼层按钮 (d,f) 被按下
12、 EAF(1 n,f) ：电梯 1 或 或 n 到达 f 层，其中 1 n 表示或为 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,1 n,f) = FBON(d,f) FBON(d
13、,f)+EAF(1 n,f)+S(d,1 n,f) = FBOFF(d,f) ；其中， d=U or D 。,也就是说: 如果在f层请求电梯向d方向运动的楼层按钮处于关闭状态，现在该按钮被按下，并且当时没有正停在f层准备向d方向移动的电梯，则该楼层按钮打开。 反之，如果楼层按钮已经打开，且至少有一部电梯到达f层，且该部电梯将朝d方向运动，则按钮将关闭。,V(e,f)重新定义,讨论电梯按钮状态转换规则时定义的谓词 V(e,f) （电梯e停在f层），可以用谓词 S(d,e,f) 重新定义如下： V(e,f)=S(U,e,f)or S(D,e,f)or S(N,e,f),(E)电梯的状态、事件及转换
14、规则,电梯的 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+1)： 如果电梯 e 停在
15、f 层准备向上(U)移动，且门已经关闭，则电梯将向上一楼层移动。 S(D,e,f)+DC(e,f) =M(D,e,f-1) 如果电梯 e 停在 f 层准备向下(D)移动，且门已经关闭，则电梯将向下一楼层移动。 S(N,e,f)+DC(e,f)= W(e,f)。 如果电梯 e 停在 f 层没有移动请求(N)，且门已经关闭，则电梯等待移动。,电梯的状态转换图,7.3 Petri网 一、Petri网概念,Petri网及其用途： 用于确定系统中隐含的定时问题的一种有效技术 是 Petri 网，这种技术的一个很大的优点是它也可以用于设计中，有效地描述并发活动。 Petri网是对离散并行系统的数学表示。P
16、etri网既有严格的数学表述方式，也有直观的图形表达方式。 Petri网适合于描述异步的、并发的自动化系统和计算机系统模型。Petri 网在计算机科学得到了广泛的应用，例如，在系统性能评价、操作系统和软件 工程等领域， Petri 网应用得都比较广泛。,二、Petri网的构成,Petri 网包含 4 种元素： 一组位置 P (Place):圆形 一组转换 T (Transition):线性/矩形 输入函数 I (Input) 输出函数 O (Output) 其他元素 连接Connection:箭头 权标Token(令牌):圆点,三、Petri网的形式化表示,一个Petri网是一个四元组C C=(P,T,I,O) 其中: P= P1 ， ， Pn 是一个有穷位置集， n 0 。 T= t1 ， ， tm 是一个有穷转换集， m 0 ，且 T 和 P 不相交。 I ： T P 为输入函数，是由转换到位置无序单位组(b
