張　丹,佘　維

(1.中國地震局地球物理勘探中心,鄭州　450002; 2.鄭州大學(xué) 軟件技術(shù)學(xué)院，鄭州　450003)

?

基于Petri網(wǎng)的電力系統(tǒng)監(jiān)控?cái)?shù)據(jù)多點(diǎn)校核方法

張丹1,佘維2

(1.中國地震局地球物理勘探中心,鄭州450002; 2.鄭州大學(xué) 軟件技術(shù)學(xué)院，鄭州450003)

由于人為誤操作和數(shù)據(jù)庫系統(tǒng)異步因素，電力系統(tǒng)監(jiān)控?cái)?shù)據(jù)存在錯(cuò)誤風(fēng)險(xiǎn)，需要對監(jiān)控?cái)?shù)據(jù)進(jìn)行多點(diǎn)校核來保障其一致性和正確性，可靠的監(jiān)控?cái)?shù)據(jù)保證電力系統(tǒng)的安全運(yùn)轉(zhuǎn)；然而多點(diǎn)校核業(yè)務(wù)流復(fù)雜且對數(shù)據(jù)精度要求高，目前的人工校核方法不僅成本高，且精度和效率低，不能保證整個(gè)監(jiān)控?cái)?shù)據(jù)的實(shí)時(shí)校核工作；為自動(dòng)化監(jiān)控?cái)?shù)據(jù)多點(diǎn)校核過程，需要對整個(gè)業(yè)務(wù)流建模，針對該問題，提出一種基于Petri網(wǎng)的監(jiān)控?cái)?shù)據(jù)多點(diǎn)校核動(dòng)態(tài)建模方法；首先將監(jiān)控系統(tǒng)的校核業(yè)務(wù)背景形式化Petri網(wǎng)中的具有不同約束的節(jié)點(diǎn)；然后使用工作流Petri方法對校核的業(yè)務(wù)流程進(jìn)行形式化定義、并將該業(yè)務(wù)流程用Petri網(wǎng)建模成為網(wǎng)狀模型；最后，針對該模型提出一種化簡技術(shù)對其進(jìn)行化簡，并證實(shí)該化簡方法的有效性和該模型能擬合監(jiān)控?cái)?shù)據(jù)多點(diǎn)校核的整個(gè)流程。

電力系統(tǒng)；監(jiān)控?cái)?shù)據(jù)；工作流；Petri網(wǎng)；形式化驗(yàn)證

0　引言

電力系統(tǒng)行業(yè)隨著電網(wǎng)規(guī)模的不斷擴(kuò)大和綜合自動(dòng)化的廣泛應(yīng)用，對其后臺監(jiān)控系統(tǒng)提出了很高的要求。因此，后臺監(jiān)控系統(tǒng)中存儲的監(jiān)控?cái)?shù)據(jù)、電網(wǎng)規(guī)模和設(shè)備信息顯得尤為重要。變電站監(jiān)控系統(tǒng)在現(xiàn)場調(diào)試和維護(hù)過程中往往由于數(shù)據(jù)庫更改或者誤操作而引起信息不一致，人工方法又難以準(zhǔn)確地進(jìn)行驗(yàn)證，導(dǎo)致原有的已經(jīng)校對測點(diǎn)信息無法匹配；另外，由于在線修改數(shù)據(jù)庫的同步方式不一致，導(dǎo)致了與主機(jī)數(shù)據(jù)庫的數(shù)據(jù)存在版本差異。因此，如果沒有專門的工具和手段對修改后的數(shù)據(jù)庫與原備份數(shù)據(jù)庫進(jìn)行校核和比對，將存在重大安全隱患。

電力系統(tǒng)的監(jiān)控?cái)?shù)據(jù)日常維護(hù)和調(diào)試業(yè)務(wù)流程非常復(fù)雜，并且對數(shù)據(jù)的準(zhǔn)確性要求極高，因此，迫切需要一種支持該復(fù)雜業(yè)務(wù)流程的建模分析方法。Petri 網(wǎng)作為一種強(qiáng)大的系統(tǒng)建模分析工具，可以完全從過程角度出發(fā)為各領(lǐng)域復(fù)雜系統(tǒng)提供建模與分析方法。它嚴(yán)格兼顧圖形語言和語義兩個(gè)方面，是一種基于狀態(tài)的建模方法。

本文針對電力系統(tǒng)監(jiān)控?cái)?shù)據(jù)多點(diǎn)校核中存在的數(shù)據(jù)不一致問題提出一種基于Petri網(wǎng)的多點(diǎn)校核方法。該方法主要有以下3個(gè)貢獻(xiàn)點(diǎn)：1)將電力系統(tǒng)監(jiān)控?cái)?shù)據(jù)多點(diǎn)校核系統(tǒng)(簡稱校核系統(tǒng))的業(yè)務(wù)流程(如角色和事物處理)形式化為Petri網(wǎng)模型中的兩大類型的節(jié)點(diǎn)，并進(jìn)一步細(xì)化不同角色和事物處理邏輯為具有相同大類約束和各自特點(diǎn)約束的節(jié)點(diǎn)；2)通過工作流網(wǎng)模型對校核系統(tǒng)建模，提出了在校核系統(tǒng)業(yè)務(wù)基礎(chǔ)上的工作流建模方法，構(gòu)建了校核業(yè)務(wù)系統(tǒng)工作流的形式化模型。3)基于該模型，提出一種簡化方法，對該復(fù)雜Petri模型進(jìn)行化簡，并對該化簡的模型進(jìn)行分析和驗(yàn)證[1-3]，從而證明了該模型的正確性和合理性。

1　Petri網(wǎng)及工作流網(wǎng)的定義

Petri[4-5]網(wǎng)的定義如下：

定義1：一個(gè)三元組N=(P,T;F)是Petri網(wǎng)，當(dāng)且僅當(dāng)：

1)P∪T≠?；

2)P∩T=?；

3)F?(P×T)∪(T×P)；

4)dom(F)∪cod(F)=P∪T。

其中，1)式中指出了P和T是兩個(gè)互不相交的集合(一般情況下假定為有限集)，它們構(gòu)成Petri網(wǎng)的基本元素，P的元素被稱為是庫所，T的元素被稱為是變遷。3)式中的F表示該網(wǎng)N的流關(guān)系，F(xiàn)中的元素被稱為是弧，由庫所指向變遷的弧被稱為輸入弧，由變遷指向庫所的弧被稱為輸出弧。4)式中的dom(F)和cod(F)分別為F的定義域和值域，同時(shí)也表示了網(wǎng)中不存在孤立的節(jié)點(diǎn)。

Petri網(wǎng)可以被圖形化，因此，當(dāng)一個(gè)網(wǎng)用圖形表示的時(shí)候，通常用一個(gè)小圓圈表示庫所，用一個(gè)小矩形框(里面填充黑色)表示變遷，用帶箭頭的有向邊來表示弧(輸入弧或輸出弧)。

定義2：設(shè)N=(P,T;F)是—個(gè)網(wǎng)，對x∈P∪T，記.x={y|y∈P∪T∧(y,x)∈F}稱為x的前集；x.={y|y∈P∪T∧(x,y)∈F}稱為x的后集；.x∪x.為元素x的外延。

工作流就是一系列相互銜接、自動(dòng)進(jìn)行的業(yè)務(wù)活動(dòng)或任務(wù)，它可以被圖形化的描述。而Petri網(wǎng)既有嚴(yán)格的數(shù)學(xué)表述方式，也有直觀的圖形表達(dá)方式，既有豐富的系統(tǒng)描述手段和系統(tǒng)行為分析技術(shù)，又為計(jì)算機(jī)科學(xué)提供堅(jiān)實(shí)的概念基礎(chǔ)。 加之研究領(lǐng)域趨向認(rèn)為Petri網(wǎng)是所有流程定義語言之母，因此在Petri網(wǎng)的基礎(chǔ)上，針對工作流的特點(diǎn)對其作了限制，產(chǎn)生了工作流Petri網(wǎng)，它能清晰地描述工作流狀態(tài)的變化。(工作流網(wǎng)的圖形表述)在建模時(shí)變遷代表工作流中的任務(wù)，庫所代表工作流中任務(wù)執(zhí)行的條件。

定義3：Petri網(wǎng)N=(P,T;F)是一個(gè)工作流網(wǎng)WF_net的充分必要條件是[6]：

1)?i∈P，使得.i=?，這里的庫所i被稱為起始庫所；

2)?o∈P，使o.=?，這里的庫所o被稱為終止庫所；

3)?x∈P∪T都位于從i到o的一條路徑上。

在上述3個(gè)充分必要條件中，條件1)和2)表示了一個(gè)工作流有始有終，從而限制了工作流網(wǎng)有且僅有一個(gè)起始庫所和一個(gè)終止庫所，一個(gè)工作過程的開始都是從起始庫所開始，而一個(gè)工作過程的結(jié)束也都是在終止庫所結(jié)束；條件3)表示了工作流網(wǎng)中沒有孤立的狀態(tài)和條件，在圖形表示上，工作流網(wǎng)中不存在單獨(dú)出來的庫所或變遷，網(wǎng)中所有的庫所和變遷都處在起始庫所到終止庫所的一條有向路徑上。

2　數(shù)據(jù)多點(diǎn)校核業(yè)務(wù)工作流網(wǎng)建模

2.1業(yè)務(wù)流映射與系統(tǒng)建模

對電力系統(tǒng)監(jiān)控?cái)?shù)據(jù)多點(diǎn)校核系統(tǒng)來說，處理的業(yè)務(wù)流程有以下兩個(gè)方面：

1)給定某一時(shí)間點(diǎn)的數(shù)據(jù)庫備份文件和另外某一個(gè)時(shí)間點(diǎn)(該時(shí)間點(diǎn)有可能在該備份文件的時(shí)間點(diǎn)之前，也有可能在備份文件的時(shí)間點(diǎn)之后)，完成到給定時(shí)間點(diǎn)的數(shù)據(jù)庫的回滾或恢復(fù)；

2)給定兩個(gè)不同時(shí)間點(diǎn)的數(shù)據(jù)庫備份文件，找出該段時(shí)間上數(shù)據(jù)庫中呈現(xiàn)的不同點(diǎn)。

鑒于以上兩項(xiàng)任務(wù)，表1顯示了一般的業(yè)務(wù)流程與工作流網(wǎng)的映射關(guān)系，可以利用這種映射關(guān)系來刻畫校核系統(tǒng)業(yè)務(wù)流程。

基于表1的映射關(guān)系，通過定義庫所、變遷節(jié)點(diǎn)及其關(guān)聯(lián)關(guān)系，模型可以有效地描述該流程中的業(yè)務(wù)環(huán)節(jié)，并反映它們之間的時(shí)序關(guān)系。如圖1所示的工作流網(wǎng)模型就是一個(gè)具體的校核系統(tǒng)業(yè)務(wù)流程的Petri網(wǎng)模型。該模型主要描述了用戶在數(shù)據(jù)校核過程中所涉及的信息處理、交互及文件操作等。在該模型中，有兩個(gè)V1表示同一個(gè)角色，也就是說，后一個(gè)V1是前一個(gè)V1的副本，兩個(gè)是完全相同的。

表1　一般業(yè)務(wù)流程與工作流網(wǎng)的映射關(guān)系

圖1　數(shù)據(jù)校核的工作流Petri網(wǎng)模型

該模型中的庫所節(jié)點(diǎn)具體的對應(yīng)關(guān)系如表2所示。

表2　庫所節(jié)點(diǎn)映射關(guān)系

表3則給出了工作流模型中的變遷節(jié)點(diǎn)具體的對應(yīng)關(guān)系。

2.2模型的化簡

圖1模型較為復(fù)雜不適合對其進(jìn)行計(jì)算機(jī)編程[1]，因此需要對該工作流模型進(jìn)行相應(yīng)的化簡，來驗(yàn)證該模型的合理性，以顯示對應(yīng)任何工作流實(shí)例，在沒有異常情況下，處理過程都能夠終止。

表3　變遷節(jié)點(diǎn)映射關(guān)系

下面先給出工作流網(wǎng)的合理性定義：

定義4(合理性)：一個(gè)工作流網(wǎng)WF_net=(P,T;F)是合理的，當(dāng)且僅當(dāng)[6]：

1)對于每一個(gè)狀態(tài)i可達(dá)的狀態(tài)M，存在一個(gè)實(shí)施序列，使得狀態(tài)M可達(dá)狀態(tài)o，可以形式化的表示為：

2)狀態(tài)o是從狀態(tài)i可達(dá)的唯一最終狀態(tài)，而且結(jié)束時(shí)其中至少會(huì)有—個(gè)標(biāo)記，可以形式化的表示為：

3)在(N,i)中不存在死變遷，可以形式化的表示為：

該條件有效地將合理性問題轉(zhuǎn)化為了對Petri網(wǎng)動(dòng)態(tài)性質(zhì)的分析和驗(yàn)證[2]。但性質(zhì)判定方法可能會(huì)受到狀態(tài)空間爆炸的約束，因此，在文獻(xiàn)[7]中研究了基于結(jié)構(gòu)的分析方法，如果一個(gè)自由選擇擴(kuò)展工作流網(wǎng)基于這些規(guī)則能將其化簡為只包含一個(gè)庫所和一個(gè)變遷的閉環(huán)網(wǎng)，則該工作流網(wǎng)是滿足合理性的。因此本文基于化簡技術(shù)對圖1工作流網(wǎng)進(jìn)行分析，并使用若干保持合理性的化簡規(guī)則，即可得到等價(jià)于原模型的化簡模型，并最后驗(yàn)證。

在文獻(xiàn)[1]提供的化簡規(guī)則基礎(chǔ)上，擴(kuò)充一條化簡規(guī)則(f)(如圖2所示)：

圖2　化簡規(guī)則f

在該圖所示的網(wǎng)中包含一個(gè)非負(fù)線性相關(guān)的庫所P，如果該網(wǎng)中去掉該庫所P，在關(guān)系上去掉與P相關(guān)的弧，這個(gè)網(wǎng)仍然是連通的，因此，可以化簡掉庫所P。

針對圖1所示的工作流網(wǎng)模型，利用文獻(xiàn)[3]提供的化簡規(guī)則，很容易驗(yàn)證工作流網(wǎng)的合理性，化簡步驟如下：

鑒于以上的化簡規(guī)則，工作流網(wǎng)WF_net的化簡過程如下：

步驟1：兩次應(yīng)用化簡規(guī)則(b)，化簡掉符合該條規(guī)則所述的庫所V2和alter2，合并變遷t5和t9為T1，合并變遷t8和t10為T2，得到化簡后的工作流網(wǎng)WF_net1，如圖3所示。

圖3　WF_net1

步驟2：兩次應(yīng)用化簡規(guī)則(a)，化簡掉符合條件的變遷t6和t7，合并庫所V3和time3為P1，合并庫所V4和time4為P2，得到化簡后的工作流網(wǎng)WF_net2，如圖4所示。

圖4　WF_net2

步驟3：應(yīng)用化簡規(guī)則(f)，化簡掉庫所V1和time2以及與其相關(guān)聯(lián)的弧，得到化簡后的工作流網(wǎng)WF_net3，如圖5所示。

圖5　WF_net3

步驟4：應(yīng)用化簡規(guī)則(c)，合并庫所P1和P2為P3，得到化簡后的工作流網(wǎng)WF_net4，如圖6所示。

圖6　WF_net4

步驟5：多次應(yīng)用化簡規(guī)則(b)，先化簡掉符合規(guī)則(b)中的庫所V1，time1，alter1，再合并變遷t1，t3，t4和T1為T2，然后化簡掉庫所P3，再合并變遷t2和t8為T3得到化簡后的工作流網(wǎng)WF_net5，如圖7所示。

步驟5：應(yīng)用化簡規(guī)則(d)，合并變遷T2和T3為T，最終化簡為只有一個(gè)起始庫所、一個(gè)終止庫所和一個(gè)變遷的簡單網(wǎng)WF_net6，如圖8所示。

圖7 WF_net5圖8 WF_net6

通過上述化簡過程，將工作流網(wǎng)WF_net 化簡為只有一個(gè)起始庫所、一個(gè)終止庫所和一個(gè)變遷的簡單網(wǎng)WF_net6，說明該工作流網(wǎng)是滿足合理性的。

2.3模型的分析與驗(yàn)證

計(jì)算可達(dá)圖可以根據(jù)Petri網(wǎng)中庫所狀態(tài)知道其托肯在網(wǎng)中的流動(dòng)，判斷是否只有一個(gè)終點(diǎn)庫所有托肯。因此，基于Petri網(wǎng)的可達(dá)圖，可以模擬和仿真系統(tǒng)的運(yùn)行，從所有的可達(dá)狀態(tài)，發(fā)現(xiàn)系統(tǒng)的動(dòng)態(tài)特性和運(yùn)行機(jī)理，從而測試出所涉及的工作流是否能夠達(dá)到預(yù)期的目標(biāo)。

根據(jù)可達(dá)圖算法[9]，得到校核系統(tǒng)的可達(dá)圖，如圖9所示。

圖中括號里面的編碼順序?yàn)?begin，V1，time2，V1，time1，alter1，V2，V3，V4，time3，time4，alter2，end)。上述可達(dá)圖模擬了系統(tǒng)可達(dá)的狀態(tài)，反應(yīng)了校核系統(tǒng)運(yùn)行的全過程，而且，通過該圖可以看出該模型能夠從初始庫所開始，進(jìn)行兩項(xiàng)業(yè)務(wù)的操作，最終到達(dá)到終止庫所，其間沒有出現(xiàn)死鎖，并且也沒有出現(xiàn)循環(huán)，說明該網(wǎng)是結(jié)構(gòu)合理的。因此，如圖9所示的可達(dá)圖驗(yàn)證了校核系統(tǒng)運(yùn)行過程中的正確性以及該工作流網(wǎng)的有效性，表明了該工作流能夠達(dá)到預(yù)期的目的。

3　結(jié)論

基于Petri網(wǎng)的相關(guān)理論，本文給出了校核系統(tǒng)工作流的Petri 網(wǎng)建模方法，構(gòu)建了相應(yīng)的形式化模型。利用該模型可以對校核系統(tǒng)工作流進(jìn)行分析與驗(yàn)證。

本文的工作一方面為校核系統(tǒng)工作流進(jìn)行了相應(yīng)的映射，提供了理論分析與驗(yàn)證方法，從而為校核系統(tǒng)的應(yīng)用提供了理論支持，更驗(yàn)證了所建模型的合理性和正確性；另一方面，也拓寬了Petri 網(wǎng)模型及其理論的應(yīng)用領(lǐng)域。相應(yīng)地，新的領(lǐng)域和應(yīng)用也必將出現(xiàn)新的理論課題和挑戰(zhàn)，這也為Petri 網(wǎng)理論的深入研究提出了要求，有助于豐富和發(fā)展Petri 網(wǎng)基礎(chǔ)理論。

[1] Murata T.Petri Nets: Properties,analysis and applications[J]. Proceedings of the IEEE，1989:541-580.

[2] 劉清華，李璐璐，萬立熊，等．工作流的動(dòng)態(tài)變更處理方法[J]．計(jì)算機(jī)輔助設(shè)計(jì)與圖形學(xué)學(xué)報(bào)，2011，23(1)：331-338.

[3] 李海凌，史本山，劉克劍,等．基于Petri網(wǎng)的建設(shè)工程項(xiàng)目實(shí)施階段工作流建模與仿真[J]．計(jì)算機(jī)應(yīng)用，2011，31(10)：2828-2831.

[4] 吳哲輝．Petri網(wǎng)導(dǎo)論[M]．北京：機(jī)械工業(yè)出版社，2006.

[5] 袁崇義．Petri網(wǎng)原理與應(yīng)用[M]．北京：電子工業(yè)出版社，2005.

[6] 郝玫，王道平,等．基于Petri網(wǎng)的工作流建模合理性驗(yàn)證算法[J]．計(jì)算機(jī)工程與應(yīng)用，2008,44(13)：228-231.

[7] 李建強(qiáng)，范玉順,等．基于Petri網(wǎng)化簡方法的工作流模型驗(yàn)證[J]．信息與控制，2001,30(6)：492-497.

[8] 吳紹艷．工程項(xiàng)目工作流的Petri 網(wǎng)表示及模型建立[J]．計(jì)算機(jī)工程與應(yīng)用，2009，45(30)：10-12.

[9] 劉鐵銘，范玉順,等．基于工作流的企業(yè)過程的建模和仿真技術(shù)研究[J]．清華大學(xué)學(xué)報(bào)(自然科學(xué)版)，2000，40(1)：107-111.

[10] 李慧芳，范玉順,等．基于時(shí)間Petri網(wǎng)的工作流模型分析[J]．軟件學(xué)報(bào)，2004,15(1)：17-26.

[11] 盧捍華，閔麗娟，王亞石,等．工作流主從實(shí)例處理方法及其Petri網(wǎng)建模[J]．通信學(xué)報(bào)，2010,31(1)：92-99.

[12] 張銳，李勇，楊嘉偉,等.電力系統(tǒng)穩(wěn)定試驗(yàn)數(shù)據(jù)的自動(dòng)校核與優(yōu)化[J]．水電能源科學(xué)，2010，28(5)：139-143.

[13] 陶佳燕，李銀紅，石東源,等．EMS與繼電保護(hù)定值校核系統(tǒng)實(shí)時(shí)數(shù)據(jù)匹配新方法[J]．電力系統(tǒng)自動(dòng)化，2012，36(10)：79-84.

[14] 劉恒，丘建棟，方杰,等．基于聯(lián)網(wǎng)收費(fèi)數(shù)據(jù)的實(shí)時(shí)滑動(dòng)、動(dòng)態(tài)校核的高速公路交通預(yù)測方法研究[J]．公路，2014，12(12)：134-139.

[15] 付紅軍，孟遠(yuǎn)景，熊浩清，等．電網(wǎng)運(yùn)行方式綜合管理系統(tǒng)設(shè)計(jì)與應(yīng)用[J]．電力自動(dòng)化設(shè)備，2010，30(4)：119-123.

Multipoint Verification about Monitoring Data of Power System Based on Petri Net

Zhang Dan1，She Wei2

(1.Geophysical Exploration Center,China Earthquake Administration,Zhengzhou450002,China; 2.School of Software Technology,Zhengzhou University,Zhengzhou450003,China)

due to manual misuse and database asynchronously,monitoring data of power system are usually inconsistent among databases,resulting that we have to ensure them consistent and accurate by the method of multipoint verification. Thus,the method is so complex that the high cost only gets the low accuracy by manual verification. The best method verifying monitoring data is automation by the computer modeling and program. To model the process of multipoint verification about monitoring data of power system,we propose a method based on Petri net that can formalize the whole business process and is transformed into computer program easily. Firstly,we map the background of verification process into the tokens and places,being constrained by different conditions,in Petri net. Secondly,we use work flow Petri method to define the verification process expressed into a net model finally. And last,we simplify the model and test the simplification method is effective.

power system;monitoring data;workflow;Petri net;formal verification

1671-4598(2016)04-0101-04DOI：10.16526/j.cnki.11-4762/tp.2016.04.030

TP301

A

2015-10-09；

2015-11-09。

國家自然科學(xué)基金(U1204610)；河南省基礎(chǔ)與前沿技術(shù)研究計(jì)劃項(xiàng)目(152300410047)；中國地震局地球物理勘探中心青年基金項(xiàng)目(YFGEC2014004)。

張丹(1986-)，女，河南安陽人，碩士，助理工程師，主要從事智能系統(tǒng)建模、數(shù)據(jù)庫工作方向的研究。

佘維(1977-)，男，湖南常德人，博士，副教授，碩士生導(dǎo)師，主要從事Petri網(wǎng)理論，復(fù)雜系統(tǒng)建模方向的研究。