载入中....
设为首页 收藏本站 联系我们 网站地图
论文网
您现在的位置: 免费毕业论文网 >> 计算机论文 >> 计算机应用 >> 正文
搜索: 论文

基于Petri网的电梯系统规格说明

更新时间 2011-7-31 11:11:16 点击数:

    邵丽丽(菏泽学院计算机与信息工程系,山东菏泽274015)摘要:为克服非形式化技术描述系统规格说明带来的二义性,采用了一种形式化技术———Petri网来描述电梯系统的规格说明。Petri网技术是对离散并行系统的数学表示,适合于描述并发的计算机系统模型,可以正确的描述电梯系统。
     关键词:Petri网;形式化技术;电梯系统
    0引言
    按照形式化的程度的不同,可以把描述系统规格说明的方法划分成非形式化、半形式化和形式化方法3类。用自然语言描述的系统规格说明,是典型的非形式化方法;用数据流图、实体-联系图或状态图等图形方式建立模型,是典型的半形式化方法;用基于数学的方法描述系统性质,那就是形式化的技术。Petri网技术是形式化技术的一种,它既有直观的图形表达方式,也有严格的数学表述方式,能有效地描述并发活动,可以正确的描述系统的规格说明。
    1 Petri网
    1.1 Petri网的结构一个Petri网包括4个元素:库所(Place)、变迁(Transition)、有向弧(Connection)、令牌(Token),如图1所示。其中库所为圆形节点,变迁为短直线,有向弧是库所和变迁之间的箭头线,令牌是库所中的动态对象,可以从一个库所移动到另一个库所。
    图1 Petri网的结构
    在图1中有一组库所P为{P1,P2,P3,P4},一组变迁T为{t1,t2},两个用于变迁的输入函数:是由库所指向变迁的箭头表示,它们是:I(t1)={P2,P4}I(t2)={P2}两个用于变迁的输出函数:是由变迁指向库所的箭头表示,它们是:O(t1)={P1}O(t2)={P3,P3}一个经典的Petri网可以表示为一个四元组(库所,变迁,输入函数,输出函数),如果使用更形式化的术语,一个Petri网可以表示为一个四元组C=(P,T,I,O),任何图都可以映射到这样一个四元组上。
    1.2 Petri网的规则和行为
    Petri网的有向弧是有方向的、两个库所或变迁之间不允许有弧线、库所可以拥有任意数量的令牌。如果一个变迁的每个输入库所拥有的令牌数大于等于该库所到变迁的弧线数时,该变迁可被激发。一个变迁被激发后,输入库所的令牌被消耗,同时输出库所将产生令牌。如果有两个变迁都有被激发的可能,其中任意一个变迁都有可能被激发,但是一次只能有一个变迁被激发。由此可见,Petri网的状态由令牌在库所中的分布决定。1.3带禁止线的Petri网禁止线是用一个小圆圈而不是用箭头标记的输入线,带禁止线的Petri网中,当每个输入库所上至少有一个令牌,而带禁止线上的库所上没有令牌的时候,相应的变迁才能被激发。因此,图2中的变迁t1可以被激发。
    2电梯系统
    下面是用自然语言描述的对电梯系统的需求:在一幢m层的大厦中需要一套控制n部电梯的产品,要求这n部电梯按照下列约束条件在楼层间移动。
    (1)每部电梯内有m个按钮,每个按钮代表一个楼层。当按下一个按钮时该按钮指示灯亮,同时电梯驶向相应的楼层,到达按钮指定的楼层时指示灯熄灭。
    (2)除了大厦的最低层和最高层之外,每层楼都有两个按钮分别请求电梯上行和下行。这两个按钮之一被按下时相应的指示灯亮,当电梯到达此楼层时灯熄灭,电梯向要求的方向移动。
    (3)当对电梯没有请求时,它关门并停在当前楼层。
    3形式化规格说明
    下面使用Petri网技术对电梯系统进行规格说明。电梯问题中有两个按钮集:n部电梯中的每一部都有m个按钮,一个按钮对应一个楼层。因为这m×n个按钮都在电梯中,所以称它们为电梯按钮;此外,每层楼有两个按钮,一个请求向上,另一个请求向下,这些按钮称为楼层按钮。当用Petri网表示电梯系统的规格说明时,每个楼层用一个库所Ff(1≤f≤m),电梯用一个令牌表示。如果在库所Ff上有令牌,表示在楼层f有电梯。
    3.1电梯按钮的规格说明
    为了用Petri网对电梯按钮进行规格说明,在Petri网中还需设置库所EBf(1≤f≤m),表示电梯中楼层f的按钮,若在EBf上有一个令牌,表示电梯内楼层f的按钮被按下了。此时映射到Petri网的四元组C=(P,T,I,O),图3电梯在g层的Petri网其中P={EBf,Fg,Ff};
    T={EB
    f被按下,电梯在运行};
    I(t
    1)={EBf},I(t2)={EBf,Fg};
    O(t
    1)={EBf},O(t2)={Ff}。
    图3所示的Petri网表示电梯在g层,此时库所EBf上没有令牌,在存在禁止线的情况下,变迁“EBf被按下”允许发生。假设现在按下电梯按钮f,则变迁“EBf被按下”被激发并在EBf上放置了一个令牌,如图4所示。若以后再次按下电梯按钮f,禁止线与现有令牌的组合决定了变迁“EBf被按下”不能再被激发,因此库所EBf上的令牌数不会多于1,且电梯按钮只有在第1次被按下时才会由暗变亮,以后再按它则都将被忽略。
    库所F
    g上有一个令牌,电梯按钮f被按下后,库所EBf上也有了一个令牌。由于每条输入线上各有一个令牌,变迁“电梯在运行”可以被激发,变迁的激发使电梯由g层驶到f层,从而库所EBf和Fg上的令牌被消耗,然后按钮EBf被关闭,在库所Ff上出现一个新令牌,如图5所示:图4电梯按钮EBf被按下后的Petri网图5电梯到达f层后的Petri网3.2楼层按钮的Petri网在Petri网中,楼层按钮用库所FBuf和FBdf表示,分别代表f楼层请求电梯上行和下行的按钮。那么最底层的按钮为FBu1,最高层的按钮为FBdm,中间每一层有两个按钮FBuf和FBdf(1≤f≤m)。图6表示根据电梯乘客的要求,某一个楼层按钮被按下或两个楼层按钮都被按下。如果两个楼层按钮都被按下了,则只能有一个按钮熄灭。此时映射到Petri网的四元组C=(P,T,I,O),其中P={FBuf,FBdf,Fg,Ff};
    T={FBu
    f被按下,电梯在运行,FBdf被按下};
    I(t
    1)={FBuf},I(t2)={FBuf,Fg},I(t3)={FBdf},I(t4)={FBdf,Fg};
    O(t
    1)={FBuf},O(t2)={Ff},O(t3)={FBdf},O(t4)={Ff}图7表示电梯没有收到请求时,它将停在当前楼层g并关门。当电梯没有请求时,库所FBuf和FBdf都没有令牌,任何一个变迁“电梯在运行”都不能被激发。
    图6楼层按钮被按下时的Petri网图7对电梯没有请求时的Petri网4结语Petri网技术采用加入禁止线和令牌的技术来描述系统的规格说明,同时辅以形式化的四元组说明,这种方法是建立在严格的数学基础上的方法,具有严谨的逻辑性,所以基于Petri网的电梯系统规格说明能够克服传统的非形式化技术描述的规格说明中的不完整性、二义性和不一致性,并可以有效的保证下一步电梯系统设计工作的正确性。尽管Petri网技术为系统做需求分析规格说明提供了很好的技术,但

[1] [2] 下一页

返回栏目页:计算机应用论文

设为主页】【收藏论文】【保存论文】【打印论文】【回到顶部】【关闭此页