溫控系統(tǒng)的時序Petri網(wǎng)建模與驗證

李文翔

(福建商學院 信息工程系，福建 福州 350012)

Petri網(wǎng)是一種適合于描述異步的、并發(fā)的計算機系統(tǒng)的網(wǎng)結構模型，它能夠直觀地描述并發(fā)系統(tǒng)事件的順序、沖突和并發(fā)等依賴關系，但不能準確描述事件的時序關系以及因果關系[1].時序邏輯通過引入時間算子可描述并發(fā)事件的時序關系以及并發(fā)系統(tǒng)的與時間相關的性能，適合于分析和驗證并發(fā)系統(tǒng)的功能性需求以及性質[2].時序Petri網(wǎng)是一種特殊的Petri網(wǎng)，它結合了Petri網(wǎng)和時序邏輯的優(yōu)點，可用來描述和驗證具有時序關系的并發(fā)系統(tǒng)模型.在時序Petri網(wǎng)的應用方面國內外學者做了很多的研究工作[3-9].

溫控系統(tǒng)是一種交互強、具有時序關系的并發(fā)系統(tǒng).因此在溫控系統(tǒng)的功能性需求說明的基礎上，本文描述溫控系統(tǒng)的Petri網(wǎng)結構模型，并利用時序邏輯描述該系統(tǒng)模型的功能性需求.通過建立該模型的可達圖，有效利用Büchi自動機和ω-正則表達式理論進行分析，得到溫控系統(tǒng)時序Petri網(wǎng)模型的變遷引發(fā)序列集合的ω-正則表達式.最后分析證明該ω-正則表達式滿足溫控系統(tǒng)的功能性需求說明.

1 需求說明

文獻[10]給出了Android平臺下溫控系統(tǒng)的需求說明：該系統(tǒng)主要由風扇傳感器模塊(接收開關指令實現(xiàn)風扇開關操作)、溫度傳感器模塊(主要采集和傳送溫度)和中控中心模塊(對溫度數(shù)值進行閾值比較、轉換顯示、發(fā)送開關指令)3個核心模塊組成，主要實現(xiàn)3個邏輯功能：溫度閾值的修改功能、串口打開與關閉功能、串口打開后溫度控制功能.該系統(tǒng)主要由3部分組成：(1)實現(xiàn)采集和傳送溫度的CC2530溫感 Zigbee模塊；(2)實現(xiàn)風扇開關的CC2530風扇繼電器 Zigbee模塊；(3)實現(xiàn)中控中心模塊功能的Android平臺，且連接有CC2530協(xié)調器 Zigbee模塊.3個模塊通過Zigbee無線傳感網(wǎng)實現(xiàn)溫度數(shù)據(jù)和開關指令信號的傳輸.而Android平臺則通過串口讀取協(xié)調器 Zigbee模塊接收的溫度數(shù)據(jù)以及向協(xié)調器 Zigbee模塊發(fā)送開關指令信號，從而實現(xiàn)溫控的基本功能.

2 系統(tǒng)模型的時序Petri網(wǎng)描述

本節(jié)首先刻畫出溫控系統(tǒng)的Petri網(wǎng)結構模型，然后給出需求說明中3種功能性需求的時序邏輯公式，最后給出溫控系統(tǒng)的時序Petri網(wǎng)的定義.

2.1 溫控系統(tǒng)Petri網(wǎng)描述

定義1溫控系統(tǒng)Petri網(wǎng)模型是一個三元組TCF=.其中：

(1)庫所集合P={p0,p1,p2,p3,p4,p5,p6,p7,p8,p9,p10,p11}.

(2)變遷集合T={t0,t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11}.

(3)F?T×P∪P×T，模型中狀態(tài)和觸發(fā)事件的流關系.

圖1 溫控系統(tǒng)Petri網(wǎng)模型Fig.1 A model of intelligent temperature control system based on Petri nets

定義1的溫控系統(tǒng)Petri網(wǎng)模型拓撲結構圖如圖1所示.各個庫所和變遷的意義說明見表1.

表1 庫所和變遷的意義說明
Tab.1 The explanation of places and transitions

庫所/變遷名意義說明p0溫度傳感器處于準備狀態(tài)p1溫度傳感器成功采集溫度數(shù)值p2溫度傳感器成功發(fā)送溫度數(shù)值p3中控中心處于準備狀態(tài)p4中控中心成功打開串口并處于等待接收數(shù)據(jù)狀態(tài)p5中控中心成功接收到來自溫度傳感器的溫度數(shù)值p6中控中心已經按特殊結構轉換溫度數(shù)值p7顯示出轉換后的溫度數(shù)值p8進行閾值比較后等待發(fā)送開或關指令p9成功發(fā)送指令給風扇傳感器p10風扇傳感器處于準備狀態(tài)p11風扇傳感器成功接收指令并處于等待打開或關閉風扇t0采集當前溫度值t1發(fā)送溫度值t2打開串口t3接收溫度值t4修改閾值t5轉換溫度值的格式t6顯示格式化后的溫度數(shù)值t7閾值比較t8發(fā)送打開或關閉指令t9接收指令t10打開或關閉風扇t11關閉串口

根據(jù)文獻[1]的合并串行庫所(FSP)和合并串行變遷(FST)兩種化簡規(guī)則，化簡定義1中提及的TCF模型，化簡后的拓撲結構如圖2所示.

圖2 化簡后的TCF模型的Petri網(wǎng)模型Fig.2The reduced model of temperature control system based on Petri nets

定義2一個化簡后的溫控系統(tǒng)基本Petri網(wǎng)模型是一個三元組TCF1=.其中：

(1)庫所集合P={p00,p3,p4,p5,p9,p10,p11}，各個庫所的意義說明見表1和表2.

(2)變遷集合T={t2,t3,t4,t80,t9,t10,t11}，各個變遷的意義說明見表1和表2.

(3)F?T×P∪P×T，模型中狀態(tài)和觸發(fā)事件的流關系.

表2 化簡后新庫所和新變遷的意義說明
Tab.1 The interpretations of the new places and transitions after being reduced

2.2 溫控系統(tǒng)的時序Petri網(wǎng)描述

定義3溫控系統(tǒng)的時序Petri網(wǎng)模型是一個二元組TTCF=.其中：

(1)TCF1是定義2的溫控系統(tǒng)基本Petri網(wǎng)模型.

(2)η為時序邏輯公式集合，η=η1∧η2∧η3.

公式η1=□◇t4，表示變遷t4無限次的經常發(fā)生，即溫控系統(tǒng)的Petri網(wǎng)模型可以修改閾值.

公式η2=□◇(t2→◇t11)，表示無限次的經常發(fā)生一種情況：如果t2變遷發(fā)生，變遷t11必定會發(fā)生，即溫控系統(tǒng)的Petri網(wǎng)模型在串口打開后可以關閉串口.

公式η3=□◇(t2→○t3∧○2t80∧○3t9∧○4◇t10)，表示無限次的經常發(fā)生一種情況：如果t2變遷發(fā)生，下一時刻開始變遷t3、變遷t80、變遷t9按順序接連發(fā)生，第4個時刻里變遷t10最終也會發(fā)生，即溫控系統(tǒng)的Petri網(wǎng)模型在打開串口后可以正確實現(xiàn)溫度控制功能.○2表示○○的縮寫，依次類推.

事實上, 時序 Petri 網(wǎng)是在 Petri 網(wǎng)中引入時序邏輯公式，而這些邏輯公式對 Petri 網(wǎng)的變遷引發(fā)序列施加限制[8].那么，設L*(PN,M0)為Petri網(wǎng)PN從初始狀態(tài)M0開始引發(fā)的有限變遷序列，Lω(PN,M0)為Petri網(wǎng)PN從初始狀態(tài)M0開始引發(fā)的無限變遷序列，Petri網(wǎng)PN所有從初始狀態(tài)M0開始引發(fā)的變遷序列L∞(PN,M0)=L*(PN,M0)∪Lω(PN,M0).則時序 Petri 網(wǎng)TN所有從初始狀態(tài)M0開始引發(fā)的變遷序列L(TN,M0)={α|α∈L∞(PN,M0)且╞η}.

定義4溫控系統(tǒng)的時序Petri網(wǎng)TTCF=所有從初始狀態(tài)M0開始的變遷引發(fā)序列可以定義為：L(TTCF,M0)= {α|α∈L∞(TCF1,M0)且╞η}，其中M0=[1,1,0,0,0,1,0]T，α為變遷引發(fā)序列.

3 模型的形式化分析

根據(jù)時序Petri網(wǎng)的概念, 時序Petri網(wǎng)的每一步發(fā)生都需要進行判斷和分析, 以保證最終生成的變遷發(fā)生序列滿足時序邏輯公式[9].因此，將通過求解L(TTCF,M0)來分析和驗證溫控系統(tǒng)的時序Petri網(wǎng)模型TTCF滿足時序邏輯公式η，以證明模型與需求說明一致性問題.

3.1 TCF模型的可達圖RG

依據(jù)文獻[1]的可達圖建立規(guī)則，可以很容易得到TCF模型的可達圖RG，如圖3所示.

圖3 TCF模型的可達圖RGFig.3 The reachable graph of the model TCF

從可達圖RG中可以看出：(1)從初始狀態(tài)M0開始，經過變遷引發(fā)序列得到了8個可達標記(M0,M1,M2,M3,M4,M5,M6,M7).(2)顯然可達圖RG是一個無限循環(huán)的有向圖.(3)時序Petri網(wǎng)的變遷引發(fā)序列就是在該有向圖上從初始狀態(tài)M0開始且符合時序邏輯公式的路徑，很明顯該變遷引發(fā)序列是一個無限序列.

依據(jù)文獻[5]，將該可達圖RG表示成在字母表Σ={t2,t3,t4,t80,t9,t10,t11}上的Büchi自動機[11]Δ，其狀態(tài)集合為M={M0,M1,M2,M3,M4,M5,M6,M7}，初始狀態(tài)為M0.設Büchi自動機Δ可接受的無限序列集合為L(Δ).那么L(TTCF,M0)的求解就演變成無限序列集合L(Δ)的求解.

3.2 可達圖RG的分析

Büchi自動機可接受的無限序列的集合就是一個ω正規(guī)集[5,12].因此將借助ω-正則表達式理論求解L(Δ).

定理1(不動點定理[5，12]) 設R1和R2為字母表Σ上的ω-正則表達式，那么

M0=t4M0+t2M1

(1)

同理可得：

M1=t11M0+t3M2

(2)

M2=t80M3

(3)

M3=t9M4

(4)

M4=t10M1+t3M6+t11M5

(5)

M5=t4M5+t2M4+t10M0

(6)

M6=t80M7+t10M2

(7)

M7=t10M3

(8)

由式(1)、(2)、(3)以及定理1得

(9)

由式(3)、(4)、(7)、(8)以及定理1得到

M6=(t80t10+t10t80)t9M4

(10)

由定理1得

(11)

由式(2)、(3)、(4)、(10)、(11)以及定理1得

M4=(t10t3t80t9+t3(t80t10+t10t80)t9+

(12)

由式(9)、(12)得

(13)

令S0=t4,S1=t2t11,S2=t2t3t80t9,S3=t10t3t80t9+t3(t80t10+t10t80)t9,S4=t11,S5=t2,S6=t10t11,S7=t10.

那么，式(13)可表示為

則根據(jù)定理1得

(14)

引理1可達圖RG表示的Büchi自動機Δ可以接受的無限序列集合為

(15)

首先S0在式(17)無限觸發(fā)，且S0=t4，也就是說t4無限發(fā)生，那么，式(17)滿足公式η1.

其次S1在式(17)無限觸發(fā)，且S1=t2t11.顯然t2t11意味著t2發(fā)生后t11就發(fā)生了,為此式(17)滿足公式η2.

最后S2,S3,S6,S7在式(17)無限觸發(fā).S2=t2t3t80t9意味著t2變遷發(fā)生，下一時刻開始變遷t3、變遷t80、變遷t9按順序接連發(fā)生.同時由于變遷t10出現(xiàn)在S3,S6,S7里，而且S3,S6,S7都在S2后觸發(fā)，由此可見在S2里t9發(fā)生后的下一時刻開始變遷t10必定會發(fā)生.因此，式(17)滿足公式η3.

綜上所述，式(17)同時滿足公式η1、η2和η3.為此我們有如下結論：

推論1溫控系統(tǒng)的時序Petri網(wǎng)模型TTCF從初始狀態(tài)M0開始的變遷引發(fā)序列集合為

推論2溫控系統(tǒng)的時序Petri網(wǎng)模型TTCF從初始狀態(tài)M0開始的變遷引發(fā)序列集合滿足了時序邏輯公式η，該模型與溫控系統(tǒng)的需求說明一致.

4 結束語

本文利用Petri網(wǎng)對溫控系統(tǒng)進行物理結構的描述，并利用時序邏輯公式描述系統(tǒng)的功能需求規(guī)范.通過建立溫控系統(tǒng)Petri網(wǎng)模型的可達圖，結合ω-正則表達式和Büchi自動機理論分析和證明了溫控系統(tǒng)的需求規(guī)范與模型的一致.雖然使用時序Petri網(wǎng)可以描述并發(fā)系統(tǒng)以及與時間相關的屬性性質，但不能很好地表達數(shù)據(jù)項的數(shù)值和類型，比如溫度的數(shù)值和類型、串口號和串口類型.對此，今后將進一步使用高級Petri網(wǎng)對溫控系統(tǒng)分析和驗證.本文也未對溫控系統(tǒng)的動態(tài)事件Petri網(wǎng)模型的活性、有界性和公平性進行正確的分析和證明，這也是將來研究和突破的方向.