04 第四章 形式化说明技术.pptx

第1页：第4章 形式化说明技术

第4章 形式化说明技术

• 1.非形式化方法：自然语言描述
• 2.半形式化方法：数据流图或实体－联系图
• 3.形式化方法：基于数学技术描述

第2页：非形式化方法的缺点

非形式化方法的缺点：概述4.1.1非形式化方法的缺点自然语言书写的系统规格说明书可能存在

• 矛盾
• 二义性；如：“操作员标识由操作员姓名和密码组成，密码由6位数字构成，当操作员登陆系统时它被存储在注册文件中。”
• 含糊性
• 不完整性
• 抽象层次混乱

第3页：形式化方法的优点与准则

形式化方法的优点与准则

• 数学是理想的建模工具，适合于表示系统状态和描述系统需求
• 用数学表达的需求可在不同开发阶段平滑过渡。4.1.3应用形式化方法的准则
• 选择合适的形式化方法
• 需要形式化，但不能过渡形式化，不能放弃传统的需求表达方法
• 应该有形式化方法的专家提供指导

第4页：有穷状态机的概念

有穷状态机的概念：有穷状态机法（FSM）4.2.1概念锁的三个位置：1、2、3；转盘可向左（L）或右（R）；锁密码：1L、3R、2L

第5页：

第6页：有穷状态机的五个组成部分

有穷状态机的五个组成部分：一个有穷状态机包括5

• 状态集J：{保险箱锁定，A，B，保险箱解锁，报警}
• 输入集K：{1L,1R,2L,2R,3L,3R}
• 转换函数T，如表4.14）初始状态S：保险箱锁定
• 终态集F：{保险箱解锁，报警}更形式化的术语：一个有穷状态机可表示一个为5元组（J,K,T,S,F）

第7页：状态转换形式与谓词集

状态转换形式与谓词集：状态转换形式：当前状态【菜单】＋事件【所选择的项】＝>下个状态加入谓词集P，把系统扩展成一个6元组后：当前状态【菜单】＋事件【所选择的项】＋谓词＝>下个状态计算机系统中每个菜单驱动的用户界面都是一个有穷状态机的实现

第8页：电梯系统的状态定义

电梯系统的状态定义

• M(d,e,f)：电梯e正沿d方向移动，即将到达第f层楼
• S(d,e,f)：电梯e停在f层楼，将朝d方向移动（未关门）
• W(e,f)：电梯e在f层等待（已关门）
• DC(e,f)：电梯e在楼层f关上门
• ST(e,f)：电梯e靠近f层时触发传感器，电梯控制器决定在当前楼层是否停下
• RL：电梯按钮或楼层按钮被按下进入打开状态4.2.2例子:

第9页：电梯状态转换规则

电梯状态转换规则

• S(U,e,f)+DC(e,f)=>M(U,e,f+
• ②S(D,e,f)+DC(e,f)=>M(D,e,f-
• ③S(N,e,f)+DC(e,f)=>W(e,f)

第10页：有穷状态机的评价

有穷状态机的评价：评价有穷状态机描述规格说明：当前状态＋事件＋谓词=>下个状态易于书写、验证、转变成设计或程序代码。有穷状态机方法比数据流图技术更精确，一样易于理解。但不能处理定时需求

第11页：Petri网的概念

Petri网的概念：Petri网

第12页：Petri网的四种元素

Petri网的四种元素：Petri网包含4

• 一组位置P，上例P＝{P1,P2,P3,P4}
• 一组转换T，上例T＝{t1,t2}
• 输入函数I，上例I（t
• ={P2,P4}I（t
• ={P2}
• 输出函数O，上例O（t
• ={P1}O（t
• ={P3,P3}更形式化的Petri网结构，是一个4元组（P，T，I，O）

第13页：权标向量（1，2，0，1）

权标向量（1，2，0，1）

第14页：权标向量（2，1，0，0）

权标向量（2，1，0，0）

第15页：权标向量（2，0，2，0）

权标向量（2，0，2，0）

第16页：带标记的Petri网五元组

带标记的Petri网五元组：更形式化地：标记M：P－>{0,1,2,…}Petri网成为一个5元组（P，T，I，O，M）

第17页：Petri网的禁止线扩充

Petri网的禁止线扩充：对Petri网的一个重要扩充是加入禁止线

第18页：电梯按钮的Petri网表示

电梯按钮的Petri网表示：例子1.电梯按钮EBf电梯中楼层f的按钮；Fg楼层g；Ff楼层f

第19页：楼层按钮的Petri网表示

楼层按钮的Petri网表示：楼层按钮FBfu第f楼层向上按钮；FBfd第f楼层向下按钮

第20页：第4章小结

第4章小结：小结基于数学的形式化说明技术，目前还没有在软件产业界广泛应用；应该把形式化方法与传统方法有机结合