第4章形式化说明技术.PPT
《第4章形式化说明技术.PPT》由会员分享,可在线阅读,更多相关《第4章形式化说明技术.PPT(22页珍藏版)》请在三一文库上搜索。
1、2019/4/6,1,第4章 形式化说明技术,4.1 概述 4.2 有穷状态机 4.3 Petri网 4.4 Z语言,2,2019/4/6,形式化方法,按照形式化的程度划分软件工程使用的方法: 非形式化 半形式化 形式化 形式化方法定义: 是描述系统性质的、基于数学的技术。,3,2019/4/6,形式化方法与欠形式化方法比较,4,2019/4/6,应用形式化方法的准则,应该选用适当的表示方法 应该形式化,但不要过分形式化 应该估算成本 应该有形式化方法顾问随时提供咨询 不应该放弃传统的开发方法 应该建立详尽的文档 不应该放弃质量标准 不应该盲目依赖形式化方法 应该测试、测试再测试 应该重用,5
2、,2019/4/6,有穷状态机(Finite State Machine),例:一个保险箱上装了一个复合锁,锁有三个位置,分别标记为1、2、3,转盘可向左(L)或向右(R)转动。这样,在任意时刻转盘都有6种可能的运动,即1L、1R、2L、2R、3L和3R。保险箱的组合密码是1L、3R、2L,转盘的任何其他运动都将引起报警。,保险箱的状态转换图,6,2019/4/6,有穷状态机的组成包括5个部分:状态集J、输入集K、由当前状态和当前输入确定下一个状态(次态)的转换函数T、初始态S和终态集F。 保险箱的有穷状态机的各部分如下: 状态集J:保险箱锁定,A,B,保险箱解锁,报警。 输入集K:1L,1R
3、,2L,2R,3L,3R。 转换函数T:见书P68表4.1所示。 初始态S:保险箱锁定。 终态集F:保险箱解锁,报警。,7,2019/4/6,使用更形式化的术语,一个有穷状态机可以表示为一个5元组(J,K,T,S,F),其中: J是一个有穷的非空状态集; K是一个有穷的非空输入集; T是一个从(J-F)K到J的转换函数; SJ,是一个初始状态; FJ,是终态集。,8,2019/4/6,Petri网,Petri网简称PNG (Petri Net Graph) Petri网已广泛地应用于硬件与软件系统的开发中,它适用于描述与分析相互独立、协同操作的处理系统,也就是并发执行的处理系统。,Petri网
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 形式化 说明 技术
链接地址:https://www.31doc.com/p-2550203.html