邵丽丽
(菏泽学院 计算机与信息工程系,山东 菏泽 274015)
基于Petri网的电梯系统规格说明
邵丽丽
(菏泽学院 计算机与信息工程系,山东 菏泽 274015)
为克服非形式化技术描述系统规格说明带来的二义性,采用了一种形式化技术——Petri网来描述电梯系统的规格说明。Petri网技术是对离散并行系统的数学表示,适合于描述并发的计算机系统模型,可以正确的描述电梯系统。
Petri网;形式化技术;电梯系统
按照形式化的程度的不同,可以把描述系统规格说明的方法划分成非形式化、半形式化和形式化方法3类。用自然语言描述的系统规格说明,是典型的非形式化方法;用数据流图、实体-联系图或状态图等图形方式建立模型,是典型的半形式化方法;用基于数学的方法描述系统性质,那就是形式化的技术。Petri网技术是形式化技术的一种,它既有直观的图形表达方式,也有严格的数学表述方式,能有效地描述并发活动,可以正确的描述系统的规格说明。
一个Petri网包括4个元素:库所(Place)、变迁(Transition)、有向弧(Connection)、令牌(Token),如图1所示。其中库所为圆形节点,变迁为短直线,有向弧是库所和变迁之间的箭头线,令牌是库所中的动态对象,可以从一个库所移动到另一个库所。
在图1中有一组库所 P 为{P1,P2,P3,P4},一组变迁 T为{t1,t2},两个用于变迁的输入函数:是由库所指向变迁的箭头表示,它们是:
两个用于变迁的输出函数:是由变迁指向库所的箭头表示,它们是:
一个经典的Petri网可以表示为一个四元组(库所,变迁,输入函数,输出函数),如果使用更形式化的术语,一个Petri网可以表示为一个四元组C=(P,T,I,O),任何图都可以映射到这样一个四元组上。
Petri网的有向弧是有方向的、两个库所或变迁之间不允许有弧线、库所可以拥有任意数量的令牌。如果一个变迁的每个输入库所拥有的令牌数大于等于该库所到变迁的弧线数时,该变迁可被激发。一个变迁被激发后,输入库所的令牌被消耗,同时输出库所将产生令牌。如果有两个变迁都有被激发的可能,其中任意一个变迁都有可能被激发,但是一次只能有一个变迁被激发。由此可见,Petri网的状态由令牌在库所中的分布决定。
图1 Petri网的结构
禁止线是用一个小圆圈而不是用箭头标记的输入线,带禁止线的Petri网中,当每个输入库所上至少有一个令牌,而带禁止线上的库所上没有令牌的时候,相应的变迁才能被激发。因此,图2中的变迁t1可以被激发。
下面是用自然语言描述的对电梯系统的需求:在一幢m层的大厦中需要一套控制n部电梯的产品,要求这n部电梯按照下列约束条件在楼层间移动。
(1)每部电梯内有m个按钮,每个按钮代表一个楼层。当按下一个按钮时该按钮指示灯亮,同时电梯驶向相应的楼层,到达按钮指定的楼层时指示灯熄灭。
(2)除了大厦的最低层和最高层之外,每层楼都有两个按钮分别请求电梯上行和下行。这两个按钮之一被按下时相应的指示灯亮,当电梯到达此楼层时灯熄灭,电梯向要求的方向移动。
(3)当对电梯没有请求时,它关门并停在当前楼层。
图2 带禁止线的Petri网
下面使用Petri网技术对电梯系统进行规格说明。电梯问题中有两个按钮集:n部电梯中的每一部都有m个按钮,一个按钮对应一个楼层。因为这m×n个按钮都在电梯中,所以称它们为电梯按钮;此外,每层楼有两个按钮,一个请求向上,另一个请求向下,这些按钮称为楼层按钮。当用Petri网表示电梯系统的规格说明时,每个楼层用一个库所Ff(1≤f≤m),电梯用一个令牌表示。如果在库所Ff上有令牌,表示在楼层f有电梯。
为了用Petri网对电梯按钮进行规格说明,在Petri网中还需设置库所EBf(1≤f≤m),表示电梯中楼层f的按钮,若在EBf上有一个令牌,表示电梯内楼层f的按钮被按下了。此时映射到Petri网的四元组C=(P,T,I,O),
其中 P={EBf,Fg,Ff};
图3所示的Petri网表示电梯在g层,此时库所EBf上没有令牌,在存在禁止线的情况下,变迁“EBf被按下”允许发生。假设现在按下电梯按钮f,则变迁“EBf被按下”被激发并在EBf上放置了一个令牌,如图4所示。若以后再次按下电梯按钮f,禁止线与现有令牌的组合决定了变迁“EBf被按下”不能再被激发,因此库所EBf上的令牌数不会多于1,且电梯按钮只有在第1次被按下时才会由暗变亮,以后再按它则都将被忽略。
库所Fg上有一个令牌,电梯按钮f被按下后,库所EBf上也有了一个令牌。由于每条输入线上各有一个令牌,变迁“电梯在运行”可以被激发,变迁的激发使电梯由g层驶到f层,从而库所EBf和Fg上的令牌被消耗,然后按钮EBf被关闭,在库所Ff上出现一个新令牌,如图5所示:
图3 电梯在g层的Petri网
图4 电梯按钮EBf被按下后的Petri网
图5 电梯到达f层后的Petri网
在Petri网中,楼层按钮用库所FBuf和FBdf表示,分别代表f楼层请求电梯上行和下行的按钮。那么最底层的按钮为FB1u,最高层的按钮为FBdm,中间每一层有两个按钮FBuf和FBdf(1≤f≤m)。图6表示根据电梯乘客的要求,某一个楼层按钮被按下或两个楼层按钮都被按下。如果两个楼层按钮都被按下了,则只能有一个按钮熄灭。此时映射到Petri网的四元组C=(P,T,I,O),
其中P={FBuf,FBdf,Fg,Ff};
T={FBuf被按下,电梯在运行,FBdf被按下};
I(t1)={FBuf},I(t2)={FBuf,Fg},I(t3)={FBdf},I(t4)={FBdf,Fg};
O(t1)={FBuf},O(t2)={Ff},O(t3)={FBdf},O(t4)={Ff}
图7表示电梯没有收到请求时,它将停在当前楼层g并关门。当电梯没有请求时,库所FBuf和FBdf都没有令牌,任何一个变迁“电梯在运行”都不能被激发。
图6 楼层按钮被按下时的Petri网
图7 对电梯没有请求时的Petri网
Petri网技术采用加入禁止线和令牌的技术来描述系统的规格说明,同时辅以形式化的四元组说明,这种方法是建立在严格的数学基础上的方法,具有严谨的逻辑性,所以基于Petri网的电梯系统规格说明能够克服传统的非形式化技术描述的规格说明中的不完整性、二义性和不一致性,并可以有效的保证下一步电梯系统设计工作的正确性。尽管Petri网技术为系统做需求分析规格说明提供了很好的技术,但它有个缺点就是在电梯由g层移动到f层是需要时间的,为处理这个情况及其他类似的问题,Petri网模型中必须加入时限。也就是说,在现实情况下需要时间控制Petri网,以使变迁与非零时间相联系。
[1] 张海藩.软件工程导论[M].5版,北京:清华大学出版社,2008.
[2] 袁崇义.Petri网原理与应用[M].北京:电子工业出版社,2005.
[3] 乐晓波,汪琳,庹清.面向对象的Petri网建模技术的研究[J].计算机工程,2002,28(5):86-88.
[4] 张俊毅,葛世伦,张清优.基于工作流的现代造船工程计划管理业务建模研究[J].船海工程,2009,38(6):57-60.
[5] 宗群,蔡昱,雷小锋.基于面向对象Petri网的电梯群控系统建模[J].系统工程与电子技术,2001,23(1):27-30.
Specification of elevators system based on Petri net
SHAO Li-li
(Computer and Information Engineering Department,Heze University,Heze 274015,China)
In order to avoid the ambiguity of system specification described by non-formal technology,this paper introduces a formal technology,Petri net,to describe the specification of elevator system.Petri net technology is a mathematical representation of the discrete parallel system,which is suitable to describe concurrent computer system models and can describe elevator system correctly.
Petri net;formal technology;elevator system
TP393.02
A
1009-3907(2011)06-0019-03
2011-04-22
邵丽丽(1979-),女,山东曹县人,讲师,硕士,主要从事软件工程与智能管理方面研究。
责任编辑:吴旭云