软件工程第4章(不讲).pptVIP

第4章 形式化说明技术 4.1 概述 4.2 有穷状态机 4.3 Petri网 4.4 Z语言 4.5 小结 形式化方法 是描述系统性质的基于数学的技术，有坚实的数学基础。 按照形式化的程度，划分成非形式化、半形式化和形式化3类。 用自然语言描述需求规格说明，是典型的非形式化方法。 用数据流图或实体-联系图建立模型，是典型的半形式化方法。 4.1.1 非形式化方法的缺点 自然语言书写的规格说明书，可能存在 矛盾 二义性 含糊性 不完整性 抽象层次混乱 4.1.2 形式化方法的优点 简洁准确，是理想的建模工具 验证需求，以发现存在的矛盾和不完整性 平滑过渡，也可以用于设计 提供了高层确认的手段 证明设计符合规格说明 证明程序代码正确地实现了设计结果 4.1.3 应用形式化方法的准则 (1) 应该选用适当的表示方法。 (2) 应该形式化，但不要过分形式化。 (3) 应该估算成本。 (4) 应该有形式化方法顾问随时提供咨询。 (5) 不应该放弃传统的开发方法。 (6) 应该建立详尽的文档。 (7) 不应该放弃质量标准。 (8) 不应该盲目依赖形式化方法。 (9) 应该测试、测试再测试。 (10) 应该重用。 4.2 有穷状态机 例如, 当有多个申请占用CPU运行的进程时, 有关CPU分配的进程的状态迁移。 保险箱的状态转换图 保险箱的状态转换图 有穷状态机的状态转换表 有穷状态机的表示 包括5个部分：状态集J、输入集K、由当前状态和当前输入确定下一个状态(次态)的转换函数T、初始态S和终态集F。 保险箱的有穷状态机： 状态集J：｛保险箱锁定，A，B，保险箱解锁，报警｝。 输入集K：｛1L，1R，2L，2R，3L，3R｝。 转换函数T：如表4.1所示。 初始态S：保险箱锁定。 终态集F：｛保险箱解锁，报警｝。 有穷状态机5元组表示 表示为一个5元组(J，K，T，S，F)，其中： J是一个有穷的非空状态集； K是一个有穷的非空输入集； T是一个从(J-F)×K到J的转换函数； S∈J，是一个初始状态； FJ，是终态集。 状态转换表示形式 状态的每个转换都具有下面的形式： 当前状态〔菜单〕+事件〔所选择的项〕下个状态。 加入谓词集P把有穷状态机扩展为一个6元组，其中每个谓词都是系统全局状态Y的函数。转换函数T则是一个从(J-F)×K×P到J的函数。转换规则形式如下： 当前状态〔菜单〕+事件〔所选择的项〕+谓词下个状态。 电梯系统的需求 自然语言描述的对电梯系统的需求： 在一幢m层的大厦中需要一套控制n部电梯的产品，要求这n部电梯按照约束条件C1，C2和C3在楼层间移动。 C1：每部电梯内有m个按钮，每个按钮代表一个楼层。当按下一个按钮时该按钮指示灯亮，同时电梯驶向相应的楼层，到达按钮指定的楼层时指示灯熄灭。 C2：除了大厦的最低层和最高层之外，每层楼都有两个按钮分别请求电梯上行和下行。这两个按钮之一被按下时相应的指示灯亮，当电梯到达此楼层时灯熄灭，电梯向要求的方向移动。 C3：当对电梯没有请求时，它关门并停在当前楼层。 电梯系统的需求 使用一个扩展的有穷状态机对本产品进行规格说明: 这个问题中有两个按钮集。 n部电梯中的每一部都有m个按钮，一个按钮对应一个楼层。因为这m×n个按钮都在电梯中，所以称它们为电梯按钮。 每层楼有两个按钮，一个请求向上，另一个请求向下，这些按钮称为楼层按钮。 电梯系统的需求 电梯按钮的状态转换图如图4.2所示。令EB(e,f)表示按下电梯e内的按钮并请求到f层去。EB(e,f)有两个状态，分别是按钮发光(打开)和不发光(关闭)。更精确地说，状态是： EBON(e,f)：电梯按钮(e,f)打开 EBOFF(e,f)：电梯按钮(e,f)关闭 如果电梯按钮(e,f)发光且电梯到达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层〔谓词〕，则该电梯按钮打开发光〔下个状态〕。 该状态转换规则的形式化描述如下： EBOFF(e,f)+EBP(e,f)+not V(e,f) EBON(e,f) 反之，如果电梯到达f层，而且电梯按钮是打开的，于是它就会熄灭。 该转换规则可以形式化地表示为： EBON(e,f)+EAF(e,f) EBOFF(e,f) 楼层按钮的状态描述 令楼层按钮FB(d,f)表示f层请求电梯向d方向运动的按钮 楼层按钮的状态如下：