4_形式化说明技术.ppt

  1. 1、本文档共49页,可阅读全部内容。
  2. 2、有哪些信誉好的足球投注网站(book118)网站文档一经付费(服务费),不意味着购买了该文档的版权,仅供个人/单位学习、研究之用,不得用于商业用途,未经授权,严禁复制、发行、汇编、翻译或者网络传播等,侵权必究。
  3. 3、本站所有内容均由合作方或网友上传,本站不对文档的完整性、权威性及其观点立场正确性做任何保证或承诺!文档内容仅供研究参考,付费前请自行鉴别。如您付费,意味着您自己接受本站规则且自行承担风险,本站不退款、不进行额外附加服务;查看《如何避免下载的几个坑》。如果您已付费下载过本站文档,您可以点击 这里二次下载
  4. 4、如文档侵犯商业秘密、侵犯著作权、侵犯人身权等,请点击“版权申诉”(推荐),也可以打举报电话:400-050-0827(电话支持时间:9:00-18:30)。
查看更多
4_形式化说明技术

为了定义与这些事件和状态相联系的状态转换规则,同样也需要一个谓词,它是S(d,e,f),它的定义如下: S(d,e,f):电梯e停在f层并且移动方向由d确定为向上(d=U)或向下(d=D)或待定(d=N)。 4.2.2 例子 使用谓词S(d,e,f),形式化转换规则为: FBOFF(d,f)+FBP(d,f)+notS(d,1…n,f)?FBON(d,f) 反之 FBON(d,f)+EAF(1…n,f)+S(d,1…n,f)?FBOFF(d,f) 其中,d=U or D。 4.2.2 例子 在讨论电梯按钮状态转换规则时定义的谓词V(e,f),可以用谓词S(d,e,f)重新定义如下: V(e,f)=S(U,e,f)or S(D,e,f)or S(N,e,f) 电梯的状态及其转换规则: 一个电梯状态实质上包含许多子状态,下面定义电梯的3个状态: M(d,e,f):电梯e正沿d方向移动,即将到达的是第f层 S(d,e,f):电梯e停在f层,将朝d方向移动(尚未关门) W(e,f):电梯e在f层等待(已关门) 4.2.2 例子 4.2.2 例子 图4.4 电梯的状态转换图 图4.4中包含了下述3个可触发状态发生改变的事件。 DC(e,f):电梯e在楼层f关上门 ST(e,f):电梯e靠近f层时触发传感器,电梯控制器决定在当前楼层电梯是否停下 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.2 例子 4.2.3 评价 有穷状态机方法描述规格说明: 当前状态+事件+谓词?下个状态 优点: 规格说明易于书写、易于验证,而且可以比较容易地把它转变成设计或程序代码。有穷状态机方法比数据流图技术更精确,而且和它一样易于理解。 缺点: 在开发一个大系统时三元组(即状态、事件、谓词)的数量会迅速增长。此外,和数据流图方法一样,形式化的有穷状态机方法也没有处理定时需求。 第4章 形式化说明技术 4.1 概述 4.2 有穷状态机 4.3 Petri网 4.4 Z语言 4.3 Petri网 4.3.1 概念 并发系统中需要解决的主要问题是定时问题:包括同步问题、竞争条件以及死锁问题。 定时问题常常是因不好的设计或有错误的实现引起的,归根到底又是由不好的规格说明造成的. Petri网技术可用于确定系统中隐含的定时问题。 Petri网技术在计算机领域应用较多,已经证明,用Petri网可以有效地描述并发活动。 Petri网包含4种元素: 一组位置P 一组转换T 输入函数I 输出函数O 4.3.1 概念 位置 转换 输入 输出 如图举例说明了Petri网的组成: 一组位置P为{P1,P2,P3,P4}:用圆圈代表; 一组转换T为{t1,t2}:图中用短直线表示转换;两个用于转换的输入函数,用由位置指向转换的箭头表示,它们是:I(t1)={P2,P4} I(t2)={P2} 两个用于转换的输出函数,用由转换指向位置的箭头表示,它们是:O(t1)={P1} O(t2)={P3,P3} Petri网是一个四元组C=(P,T,I,O),其中: P={P1,P2,…Pn}是一个有穷位置集,n≥0; T=(t1,…,tm)是一个有穷转换集,m≥0,且T和不相交; I:T→P∞为输入函数,是由转换到位置无序单位组的映射; O:T→P∞为输出函数,是由转换到位置无序单位组的映射。 4.3.1 概念 带标记的Petri网: 权标(token)的分配。如图中有4个权标 上述标记可以用向量(1,2,0,1)表示。 由于P2和P4中有权标,因此t1启动(即被激发)。 通常,当每个输入位置所拥有的权标数大于等于从该位置到转换的线数时,就允许转换。当t1被激发时,P2和P4上各有一个权标被移出,而P1上则增加一个权标(2,1,0,0)。 Petri网中权标总数不是固定的,在这个例子中两个权标被移出,而P1上只能增加一个权标。 4.3.1 概念 权标数 如图,P2上有权标,因此t2也可以被激发。当t2被激发时,P2上将移走一个权标,而P3上新增加两个权标(1,1,2,1)。 4.3.1 概念 Petri网具有非确定性,如果数个转换都达到了激发条件,则其中任意一个都可以被激发。图4.6所示Petri网的标记为(1,2,0,1),t1和t2都可以被激发。 4.3.1 概念 假设t1被激发了,标记

文档评论(0)

yan698698 + 关注
实名认证
内容提供者

该用户很懒,什么也没介绍

1亿VIP精品文档

相关文档