李文翔

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

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

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

1 需求說(shuō)明

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

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

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

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

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

(1)庫(kù)所集合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ā)事件的流關(guān)系.

圖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)模型拓?fù)浣Y(jié)構(gòu)圖如圖1所示.各個(gè)庫(kù)所和變遷的意義說(shuō)明見(jiàn)表1.

表1 庫(kù)所和變遷的意義說(shuō)明
Tab.1 The explanation of places and transitions

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

根據(jù)文獻(xiàn)[1]的合并串行庫(kù)所(FSP)和合并串行變遷(FST)兩種化簡(jiǎn)規(guī)則，化簡(jiǎn)定義1中提及的TCF模型，化簡(jiǎn)后的拓?fù)浣Y(jié)構(gòu)如圖2所示.

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

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

(1)庫(kù)所集合P={p00,p3,p4,p5,p9,p10,p11}，各個(gè)庫(kù)所的意義說(shuō)明見(jiàn)表1和表2.

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

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

表2 化簡(jiǎn)后新庫(kù)所和新變遷的意義說(shuō)明
Tab.1 The interpretations of the new places and transitions after being reduced

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

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

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

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

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

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

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

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

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

3 模型的形式化分析

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

3.1 TCF模型的可達(dá)圖RG

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

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

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

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

3.2 可達(dá)圖RG的分析

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

定理1(不動(dòng)點(diǎn)定理[5，12]) 設(shè)R1和R2為字母表Σ上的ω-正則表達(dá)式，那么

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可達(dá)圖RG表示的Büchi自動(dòng)機(jī)Δ可以接受的無(wú)限序列集合為

(15)

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

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

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

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

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

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

4 結(jié)束語(yǔ)

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