基于Petri網的電梯系統規格說明

邵麗麗

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

基于Petri網的電梯系統規格說明

邵麗麗

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

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

Petri網;形式化技術;電梯系統

0 引言

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

1 Petri網

1.1 Petri網的結構

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

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

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

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

1.2 Petri網的規則和行為

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

圖1 Petri網的結構

1.3 帶禁止線的Petri網

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

2 電梯系統

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

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

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

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

圖2 帶禁止線的Petri網

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)，

其中 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網

3.2 樓層按鈕的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網

4 結語

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-)，女，山東曹縣人，講師，碩士，主要從事軟件工程與智能管理方面研究。

責任編輯:吳旭云