搜索
软件工程(SoftwareEngineering)计算机学院软件工程系杨易扬第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）应该有形式化方法的专家提供指导。•一个旋转栅门的例子：•两种状态：锁定状态（Locked）、非锁定状态(Unlocked)•动作：投币(Coin)与推动旋转臂(Push)•投币才能推动旋转臂一次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{J-F}*K•4）初始状态S：保险箱锁定•5）终态集F：{保险箱解锁，报警}•更形式化的术语：•一个有穷状态机可表示一个为5元组（J,K,T,S,F）•状态转换形式：•当前状态【菜单】＋事件【所选择的项】＝下个状态•{J-F}*K•加入谓词集P，把系统扩展成一个6元组后：•当前状态【菜单】＋事件【所选择的项】＋谓词＝下个状态•{J-F}*K*P计算机系统中每个菜单驱动的用户界面都是一个有穷状态机的实现。•定义状态：•（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评价•有穷状态机描述规格说明：•当前状态＋事件＋谓词=下个状态•易于书写、验证、转变成设计或程序代码。有穷状态机方法比数据流图技术更精确，一样易于理解。1.但不能处理定时需求。2.大系统时，数量迅速增长4.3Petri网•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楼层向下按钮；•小结•基于数学的形式化说明技术，目前还没有在软件产业界广泛应用；•应该把形式化方法与传统方法有机结合。