形式化需求说明技术全解.ppt

形式化需求说明技术 形式化技术概述 有穷状态机 Petri Net Z语言 非形式化方法的缺点 矛盾 二义性 含糊性 不完整性 抽象层次混乱 非形式化方法的优点 能够简洁、精确地描述需求 可以在不同的软件工程活动之间平滑过渡 利于证明软件（包括中间产品）的正确性 应用非形式化方法的准则 应当选用适当的表示方法。 但不要过分和盲目依赖形式化。正确认识形式化、半形式化和非形式化之间的关系，不应该放弃传统的开发方法。 应该估算形式化方法对软件成本的影响。 应该有形式化方法顾问随时提供咨询。 建立详尽的文档。 不应该放弃质量标准。 测试仍然非常重要。 应该重视重用。 有限状态模型 状态迁移图 状态迁移图是描述系统的状态如何相应外部的信号进行推移的一种图形表示。 圆圈“○”表示可得到的系统状态 箭头“→”表示从一种状态向另一种状态的迁移。 例一, 当有多个申请占用CPU运行的进程时, 有关CPU分配的进程的状态迁移。 可得到的状态＝就绪，运行，等待 生成的事件＝t1，t2， t3， t4 ? t1 ─ 中断事件 ? t2 ─ 中断已处理 ? t3 ─ 分配CPU ? t4 ─ 用完CPU时间 例二:复合锁保险箱的状态转换图 复合锁保险箱的状态转换表 形式化描述 可以把有穷状态机表示为一个五元组{J,K,T,S,F) 状态集J:{锁定,A,B,解锁,报警},有穷非空状态集 输入集K:{1L,1R,2L,2R,3L,3R},有穷非空输入集 转换函数T是一个从(J-F)╳ K到J的转换函数 初态集S∈J,是一个初始状态:{保险箱锁定} 终态集F?J:{解锁,报警} 状态转换图的优点 状态之间的关系能够直观地捕捉到 由于状态迁移图的单纯性，能够机械地分析许多情况，可很容易地建立分析工具 Petri网 Petri网已广泛地应用于硬件与软件系统的开发中，它适用于描述与分析相互独立、协同操作的处理系统，也就是并发执行的处理系统。 Petri网简称PNG (Petri Net Graph)，它有两种结点： 位置(place)：符号为“○”，它用来表示系统的状态。 转移(transition)：符号为 “|”, 它用来表示系统中的事件。 图中的有向边表示对转移的输入，或由转移的输出 标记，或称令牌(token)，是表明系统当前处于什么状态的标志 形式化的Petri网结构 带有标记的PNG为一个五元组( P,T,I,0,M ) P ={p1,p2,…,pn } T ={t1,t2,…,tm } I:T→P∞为输入函数,是由转换到位置无序单元组的映射 O:T→P∞为输出函数,是由转换到位置无序单元组的映射 M:P→{1,2,…} 处理两个进程的同步问题 * parnas提出的使用最广泛的一种可执行规格说明形式。从一个初始状态开始接收输入，到产生输出，状态在推移变化。施加在状态元素上的约束确定了有效状态的推移。 B A 报警 保险箱 锁定 保险箱 解锁 初始态 1L 2L 3R 转盘的 任何其 它转动 终态 转盘的 任何其 它转动 转盘的 任何其 它转动 报警 B 报警 3R 报警 报警 报警 3L 报警 报警 报警 2R 保险箱解锁 报警 报警 2L 报警 报警 报警 1R 报警 报警 A 1L B A 保险箱锁定 ? f (State A, Event)→ State S f (State A, Event 1, Event 2, … ,Event N)→ State S f (State A, Event 1, Event 2, … ,Event N)→ State1, State2,…,State M *