基于Petri網(wǎng)的電梯系統(tǒng)規(guī)格說明

邵麗麗

(菏澤學(xué)院 計(jì)算機(jī)與信息工程系，山東 菏澤 274015)

基于Petri網(wǎng)的電梯系統(tǒng)規(guī)格說明

邵麗麗

(菏澤學(xué)院 計(jì)算機(jī)與信息工程系，山東 菏澤 274015)

為克服非形式化技術(shù)描述系統(tǒng)規(guī)格說明帶來的二義性，采用了一種形式化技術(shù)——Petri網(wǎng)來描述電梯系統(tǒng)的規(guī)格說明。Petri網(wǎng)技術(shù)是對(duì)離散并行系統(tǒng)的數(shù)學(xué)表示，適合于描述并發(fā)的計(jì)算機(jī)系統(tǒng)模型，可以正確的描述電梯系統(tǒng)。

Petri網(wǎng);形式化技術(shù);電梯系統(tǒng)

0 引言

按照形式化的程度的不同，可以把描述系統(tǒng)規(guī)格說明的方法劃分成非形式化、半形式化和形式化方法3類。用自然語言描述的系統(tǒng)規(guī)格說明，是典型的非形式化方法;用數(shù)據(jù)流圖、實(shí)體－聯(lián)系圖或狀態(tài)圖等圖形方式建立模型，是典型的半形式化方法;用基于數(shù)學(xué)的方法描述系統(tǒng)性質(zhì)，那就是形式化的技術(shù)。Petri網(wǎng)技術(shù)是形式化技術(shù)的一種，它既有直觀的圖形表達(dá)方式，也有嚴(yán)格的數(shù)學(xué)表述方式，能有效地描述并發(fā)活動(dòng)，可以正確的描述系統(tǒng)的規(guī)格說明。

1 Petri網(wǎng)

1.1 Petri網(wǎng)的結(jié)構(gòu)

一個(gè)Petri網(wǎng)包括4個(gè)元素:庫所(Place)、變遷(Transition)、有向弧(Connection)、令牌(Token)，如圖1所示。其中庫所為圓形節(jié)點(diǎn)，變遷為短直線，有向弧是庫所和變遷之間的箭頭線，令牌是庫所中的動(dòng)態(tài)對(duì)象，可以從一個(gè)庫所移動(dòng)到另一個(gè)庫所。

在圖1中有一組庫所 P 為{P1，P2，P3，P4}，一組變遷 T為{t1，t2}，兩個(gè)用于變遷的輸入函數(shù):是由庫所指向變遷的箭頭表示，它們是:

兩個(gè)用于變遷的輸出函數(shù):是由變遷指向庫所的箭頭表示，它們是:

一個(gè)經(jīng)典的Petri網(wǎng)可以表示為一個(gè)四元組(庫所，變遷，輸入函數(shù)，輸出函數(shù))，如果使用更形式化的術(shù)語，一個(gè)Petri網(wǎng)可以表示為一個(gè)四元組C=(P，T，I，O)，任何圖都可以映射到這樣一個(gè)四元組上。

1.2 Petri網(wǎng)的規(guī)則和行為

Petri網(wǎng)的有向弧是有方向的、兩個(gè)庫所或變遷之間不允許有弧線、庫所可以擁有任意數(shù)量的令牌。如果一個(gè)變遷的每個(gè)輸入庫所擁有的令牌數(shù)大于等于該庫所到變遷的弧線數(shù)時(shí)，該變遷可被激發(fā)。一個(gè)變遷被激發(fā)后，輸入庫所的令牌被消耗，同時(shí)輸出庫所將產(chǎn)生令牌。如果有兩個(gè)變遷都有被激發(fā)的可能，其中任意一個(gè)變遷都有可能被激發(fā)，但是一次只能有一個(gè)變遷被激發(fā)。由此可見，Petri網(wǎng)的狀態(tài)由令牌在庫所中的分布決定。

圖1 Petri網(wǎng)的結(jié)構(gòu)

1.3 帶禁止線的Petri網(wǎng)

禁止線是用一個(gè)小圓圈而不是用箭頭標(biāo)記的輸入線，帶禁止線的Petri網(wǎng)中，當(dāng)每個(gè)輸入庫所上至少有一個(gè)令牌，而帶禁止線上的庫所上沒有令牌的時(shí)候，相應(yīng)的變遷才能被激發(fā)。因此，圖2中的變遷t1可以被激發(fā)。

2 電梯系統(tǒng)

下面是用自然語言描述的對(duì)電梯系統(tǒng)的需求:在一幢m層的大廈中需要一套控制n部電梯的產(chǎn)品，要求這n部電梯按照下列約束條件在樓層間移動(dòng)。

(1)每部電梯內(nèi)有m個(gè)按鈕，每個(gè)按鈕代表一個(gè)樓層。當(dāng)按下一個(gè)按鈕時(shí)該按鈕指示燈亮，同時(shí)電梯駛向相應(yīng)的樓層，到達(dá)按鈕指定的樓層時(shí)指示燈熄滅。

(2)除了大廈的最低層和最高層之外，每層樓都有兩個(gè)按鈕分別請(qǐng)求電梯上行和下行。這兩個(gè)按鈕之一被按下時(shí)相應(yīng)的指示燈亮，當(dāng)電梯到達(dá)此樓層時(shí)燈熄滅，電梯向要求的方向移動(dòng)。

(3)當(dāng)對(duì)電梯沒有請(qǐng)求時(shí)，它關(guān)門并停在當(dāng)前樓層。

圖2 帶禁止線的Petri網(wǎng)

3 形式化規(guī)格說明

下面使用Petri網(wǎng)技術(shù)對(duì)電梯系統(tǒng)進(jìn)行規(guī)格說明。電梯問題中有兩個(gè)按鈕集:n部電梯中的每一部都有m個(gè)按鈕，一個(gè)按鈕對(duì)應(yīng)一個(gè)樓層。因?yàn)檫@m×n個(gè)按鈕都在電梯中，所以稱它們?yōu)殡娞莅粹o;此外，每層樓有兩個(gè)按鈕，一個(gè)請(qǐng)求向上，另一個(gè)請(qǐng)求向下，這些按鈕稱為樓層按鈕。當(dāng)用Petri網(wǎng)表示電梯系統(tǒng)的規(guī)格說明時(shí)，每個(gè)樓層用一個(gè)庫所Ff(1≤f≤m)，電梯用一個(gè)令牌表示。如果在庫所Ff上有令牌，表示在樓層f有電梯。

3.1 電梯按鈕的規(guī)格說明

為了用Petri網(wǎng)對(duì)電梯按鈕進(jìn)行規(guī)格說明，在Petri網(wǎng)中還需設(shè)置庫所EBf(1≤f≤m)，表示電梯中樓層f的按鈕，若在EBf上有一個(gè)令牌，表示電梯內(nèi)樓層f的按鈕被按下了。此時(shí)映射到Petri網(wǎng)的四元組C=(P，T，I，O)，

其中 P={EBf，F(xiàn)g，F(xiàn)f};

圖3所示的Petri網(wǎng)表示電梯在g層，此時(shí)庫所EBf上沒有令牌，在存在禁止線的情況下，變遷“EBf被按下”允許發(fā)生。假設(shè)現(xiàn)在按下電梯按鈕f，則變遷“EBf被按下”被激發(fā)并在EBf上放置了一個(gè)令牌，如圖4所示。若以后再次按下電梯按鈕f，禁止線與現(xiàn)有令牌的組合決定了變遷“EBf被按下”不能再被激發(fā)，因此庫所EBf上的令牌數(shù)不會(huì)多于1，且電梯按鈕只有在第1次被按下時(shí)才會(huì)由暗變亮，以后再按它則都將被忽略。

庫所Fg上有一個(gè)令牌，電梯按鈕f被按下后，庫所EBf上也有了一個(gè)令牌。由于每條輸入線上各有一個(gè)令牌，變遷“電梯在運(yùn)行”可以被激發(fā)，變遷的激發(fā)使電梯由g層駛到f層，從而庫所EBf和Fg上的令牌被消耗，然后按鈕EBf被關(guān)閉，在庫所Ff上出現(xiàn)一個(gè)新令牌，如圖5所示:

圖3 電梯在g層的Petri網(wǎng)

圖4 電梯按鈕EBf被按下后的Petri網(wǎng)

圖5 電梯到達(dá)f層后的Petri網(wǎng)

3.2 樓層按鈕的Petri網(wǎng)

在Petri網(wǎng)中，樓層按鈕用庫所FBuf和FBdf表示，分別代表f樓層請(qǐng)求電梯上行和下行的按鈕。那么最底層的按鈕為FB1u，最高層的按鈕為FBdm，中間每一層有兩個(gè)按鈕FBuf和FBdf(1≤f≤m)。圖6表示根據(jù)電梯乘客的要求，某一個(gè)樓層按鈕被按下或兩個(gè)樓層按鈕都被按下。如果兩個(gè)樓層按鈕都被按下了，則只能有一個(gè)按鈕熄滅。此時(shí)映射到Petri網(wǎng)的四元組C=(P，T，I，O)，

其中P={FBuf，F(xiàn)Bdf，F(xiàn)g，F(xiàn)f};

T={FBuf被按下，電梯在運(yùn)行，F(xiàn)Bdf被按下};

I(t1)={FBuf}，I(t2)={FBuf，F(xiàn)g}，I(t3)={FBdf}，I(t4)={FBdf，F(xiàn)g};

O(t1)={FBuf}，O(t2)={Ff}，O(t3)={FBdf}，O(t4)={Ff}

圖7表示電梯沒有收到請(qǐng)求時(shí)，它將停在當(dāng)前樓層g并關(guān)門。當(dāng)電梯沒有請(qǐng)求時(shí)，庫所FBuf和FBdf都沒有令牌，任何一個(gè)變遷“電梯在運(yùn)行”都不能被激發(fā)。

圖6 樓層按鈕被按下時(shí)的Petri網(wǎng)

圖7 對(duì)電梯沒有請(qǐng)求時(shí)的Petri網(wǎng)

4 結(jié)語

Petri網(wǎng)技術(shù)采用加入禁止線和令牌的技術(shù)來描述系統(tǒng)的規(guī)格說明，同時(shí)輔以形式化的四元組說明，這種方法是建立在嚴(yán)格的數(shù)學(xué)基礎(chǔ)上的方法，具有嚴(yán)謹(jǐn)?shù)倪壿嬓?，所以基于Petri網(wǎng)的電梯系統(tǒng)規(guī)格說明能夠克服傳統(tǒng)的非形式化技術(shù)描述的規(guī)格說明中的不完整性、二義性和不一致性，并可以有效的保證下一步電梯系統(tǒng)設(shè)計(jì)工作的正確性。盡管Petri網(wǎng)技術(shù)為系統(tǒng)做需求分析規(guī)格說明提供了很好的技術(shù)，但它有個(gè)缺點(diǎn)就是在電梯由g層移動(dòng)到f層是需要時(shí)間的，為處理這個(gè)情況及其他類似的問題，Petri網(wǎng)模型中必須加入時(shí)限。也就是說，在現(xiàn)實(shí)情況下需要時(shí)間控制Petri網(wǎng)，以使變遷與非零時(shí)間相聯(lián)系。

［1］ 張海藩.軟件工程導(dǎo)論［M］.5版，北京:清華大學(xué)出版社，2008.

［2］ 袁崇義.Petri網(wǎng)原理與應(yīng)用［M］.北京:電子工業(yè)出版社，2005.

［3］ 樂曉波，汪琳，庹清.面向?qū)ο蟮腜etri網(wǎng)建模技術(shù)的研究［J］.計(jì)算機(jī)工程，2002，28(5):86－88.

［4］ 張俊毅，葛世倫，張清優(yōu).基于工作流的現(xiàn)代造船工程計(jì)劃管理業(yè)務(wù)建模研究［J］.船海工程，2009，38(6):57－60.

［5］ 宗群，蔡昱，雷小鋒.基于面向?qū)ο驪etri網(wǎng)的電梯群控系統(tǒng)建模［J］.系統(tǒng)工程與電子技術(shù)，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-)，女，山東曹縣人，講師，碩士，主要從事軟件工程與智能管理方面研究。

責(zé)任編輯:吳旭云