邵麗麗

(菏澤學院 計算機與信息工程系，山東 菏澤 274015)

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

邵麗麗

(菏澤學院 計算機與信息工程系，山東 菏澤 274015)

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

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

0 引言

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

1 Petri網(wǎng)

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

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

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

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

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

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

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

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

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

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

2 電梯系統(tǒng)

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

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

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

(3)當對電梯沒有請求時，它關(guān)門并停在當前樓層。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

T={FBuf被按下，電梯在運行，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表示電梯沒有收到請求時，它將停在當前樓層g并關(guān)門。當電梯沒有請求時，庫所FBuf和FBdf都沒有令牌，任何一個變遷“電梯在運行”都不能被激發(fā)。

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

圖7 對電梯沒有請求時的Petri網(wǎng)

4 結(jié)語

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

［1］ 張海藩.軟件工程導論［M］.5版，北京:清華大學出版社，2008.

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

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

［4］ 張俊毅，葛世倫，張清優(yōu).基于工作流的現(xiàn)代造船工程計劃管理業(yè)務建模研究［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-)，女，山東曹縣人，講師，碩士，主要從事軟件工程與智能管理方面研究。

責任編輯:吳旭云