软件工程4(西南交通大学软件工程)剖析.ppt

第4章：形式化说明技术 1.非形式化方法：自然语言描述 2.半形式化方法：数据流图或实体－联系图 3.形式化方法：基于数学技术描述 4.1 概述 4.1.1 非形式化方法的缺点 自然语言书写的系统规格说明书可能存在： 1）矛盾； 2）二义性； 如：“操作员标识由操作员姓名和密码组成，密码由6位数字构成，当操作员登陆系统时它被存储在注册文件中。” 3）含糊性； 4）不完整性； 5）抽象层次混乱。 4.1.2 形式化方法的优点 （1）数学是理想的建模工具，适合于表示系统状态和描述系统需求； （2）用数学表达的需求可在不同开发阶段平滑过渡。 4.1.3 应用形式化方法的准则 （1）选择合适的形式化方法； （2）需要形式化，但不能过渡形式化，不能放弃传统的需求表达方法； （3）应该有形式化方法的专家提供指导。 4.2 有穷状态机法（FSM） 4.2.1 概念 锁的三个位置：1、2、3； 转盘可向左（L）或右（R）； 锁密码：1L、3R、2L 一个有穷状态机包括5部分： 1）状态集J：{保险箱锁定，A，B，保险箱解锁，报警} 2）输入集K：{1L,1R,2L,2R,3L,3R} 3）转换函数T，如表4.1 4）初始状态S：保险箱锁定 5）终态集F：{保险箱解锁，报警} 更形式化的术语： 一个有穷状态机可表示一个为5元组（J,K,T,S,F） 状态转换形式： 当前状态【菜单】＋事件【所选择的项】＝下个状态 加入谓词集P，把系统扩展成一个6元组后： 当前状态【菜单】＋事件【所选择的项】＋谓词＝下个状态 计算机系统中每个菜单驱动的用户界面都是一个有穷状态机的实现。 定义状态： （1）M(d,e,f)：电梯e正沿d方向移动，即将到达第f层楼。 （2）S(d,e,f)：电梯e停在f层楼，将朝d方向移动（未关门）。 （3）W(e,f)：电梯e在f层等待（已关门）。 （4）DC(e,f)：电梯e在楼层f关上门。 （5）ST(e,f)：电梯e靠近f层时触发传感器，电梯控制器决定在当前楼层是否停下。 （6）RL：电梯按钮或楼层按钮被按下进入打开状态 4.2.2 例子:电梯的状态转换 电梯状态转换规则：①S(U,e,f)+DC(e,f)=M(U,e,f+1); ②S(D,e,f)+DC(e,f)=M(D,e,f-1); ③S(N,e,f)+DC(e,f)=W(e,f) 4.2.3 评价 有穷状态机描述规格说明： 当前状态＋事件＋谓词=下个状态 易于书写、验证、转变成设计或程序代码。 有穷状态机方法比数据流图技术更精确，一样易于理解。但不能处理定时需求。 4.3 Petri网 4.3.1 概念 Petri网包含4种元素： 1）一组位置P，上例 P＝{P1,P2,P3,P4} 2）一组转换T，上例 T＝{t1,t2} 3）输入函数I，上例 I（t1）={P2,P4} I（t2）={P2} 4）输出函数O，上例O（t1）={P1} O（t2）={P3,P3} 更形式化的Petri网结构，是一个4元组（P，T，I，O） 权标向量（1，2，0，1） 权标向量（2，1，0，0） 权标向量（2，0，2，0） 更形式化地： 标记 M：P－{0,1,2,…} Petri网成为一个5元组（P，T，I，O，M） 对Petri网的一个重要扩充是加入禁止线： 4.3.2 例子 1. 电梯按钮 EBf 电梯中楼层 f 的按钮；Fg 楼层g；Ff 楼层 f。 2. 楼层按钮 FBfu 第 f 楼层向上按钮； FBfd 第 f 楼层向下按钮； 小结 基于数学的形式化说明技术，目前还没有在软件产业界广泛应用； 应该把形式化方法与传统方法有机结合。