基于Petri网的电力系统监控数据多点校核方法

张　丹,佘　维

(1.中国地震局地球物理勘探中心,郑州　450002; 2.郑州大学 软件技术学院，郑州　450003)



基于Petri网的电力系统监控数据多点校核方法

张丹1,佘维2

(1.中国地震局地球物理勘探中心,郑州450002; 2.郑州大学 软件技术学院，郑州450003)

由于人为误操作和数据库系统异步因素，电力系统监控数据存在错误风险，需要对监控数据进行多点校核来保障其一致性和正确性，可靠的监控数据保证电力系统的安全运转；然而多点校核业务流复杂且对数据精度要求高，目前的人工校核方法不仅成本高，且精度和效率低，不能保证整个监控数据的实时校核工作；为自动化监控数据多点校核过程，需要对整个业务流建模，针对该问题，提出一种基于Petri网的监控数据多点校核动态建模方法；首先将监控系统的校核业务背景形式化Petri网中的具有不同约束的节点；然后使用工作流Petri方法对校核的业务流程进行形式化定义、并将该业务流程用Petri网建模成为网状模型；最后，针对该模型提出一种化简技术对其进行化简，并证实该化简方法的有效性和该模型能拟合监控数据多点校核的整个流程。

电力系统；监控数据；工作流；Petri网；形式化验证

0　引言

电力系统行业随着电网规模的不断扩大和综合自动化的广泛应用，对其后台监控系统提出了很高的要求。因此，后台监控系统中存储的监控数据、电网规模和设备信息显得尤为重要。变电站监控系统在现场调试和维护过程中往往由于数据库更改或者误操作而引起信息不一致，人工方法又难以准确地进行验证，导致原有的已经校对测点信息无法匹配；另外，由于在线修改数据库的同步方式不一致，导致了与主机数据库的数据存在版本差异。因此，如果没有专门的工具和手段对修改后的数据库与原备份数据库进行校核和比对，将存在重大安全隐患。

电力系统的监控数据日常维护和调试业务流程非常复杂，并且对数据的准确性要求极高，因此，迫切需要一种支持该复杂业务流程的建模分析方法。Petri 网作为一种强大的系统建模分析工具，可以完全从过程角度出发为各领域复杂系统提供建模与分析方法。它严格兼顾图形语言和语义两个方面，是一种基于状态的建模方法。

本文针对电力系统监控数据多点校核中存在的数据不一致问题提出一种基于Petri网的多点校核方法。该方法主要有以下3个贡献点：1)将电力系统监控数据多点校核系统(简称校核系统)的业务流程(如角色和事物处理)形式化为Petri网模型中的两大类型的节点，并进一步细化不同角色和事物处理逻辑为具有相同大类约束和各自特点约束的节点；2)通过工作流网模型对校核系统建模，提出了在校核系统业务基础上的工作流建模方法，构建了校核业务系统工作流的形式化模型。3)基于该模型，提出一种简化方法，对该复杂Petri模型进行化简，并对该化简的模型进行分析和验证[1-3]，从而证明了该模型的正确性和合理性。

1　Petri网及工作流网的定义

Petri[4-5]网的定义如下：

定义1：一个三元组N=(P,T;F)是Petri网，当且仅当：

1)P∪T≠Ø；

2)P∩T=Ø；

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

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

其中，1)式中指出了P和T是两个互不相交的集合(一般情况下假定为有限集)，它们构成Petri网的基本元素，P的元素被称为是库所，T的元素被称为是变迁。3)式中的F表示该网N的流关系，F中的元素被称为是弧，由库所指向变迁的弧被称为输入弧，由变迁指向库所的弧被称为输出弧。4)式中的dom(F)和cod(F)分别为F的定义域和值域，同时也表示了网中不存在孤立的节点。

Petri网可以被图形化，因此，当一个网用图形表示的时候，通常用一个小圆圈表示库所，用一个小矩形框(里面填充黑色)表示变迁，用带箭头的有向边来表示弧(输入弧或输出弧)。

定义2：设N=(P,T;F)是—个网，对x∈P∪T，记.x={y|y∈P∪T∧(y,x)∈F}称为x的前集；x.={y|y∈P∪T∧(x,y)∈F}称为x的后集；.x∪x.为元素x的外延。

工作流就是一系列相互衔接、自动进行的业务活动或任务，它可以被图形化的描述。而Petri网既有严格的数学表述方式，也有直观的图形表达方式，既有丰富的系统描述手段和系统行为分析技术，又为计算机科学提供坚实的概念基础。 加之研究领域趋向认为Petri网是所有流程定义语言之母，因此在Petri网的基础上，针对工作流的特点对其作了限制，产生了工作流Petri网，它能清晰地描述工作流状态的变化。(工作流网的图形表述)在建模时变迁代表工作流中的任务，库所代表工作流中任务执行的条件。

定义3：Petri网N=(P,T;F)是一个工作流网WF_net的充分必要条件是[6]：

1)∃i∈P，使得.i=Ø，这里的库所i被称为起始库所；

2)∃o∈P，使o.=Ø，这里的库所o被称为终止库所；

3)∀x∈P∪T都位于从i到o的一条路径上。

在上述3个充分必要条件中，条件1)和2)表示了一个工作流有始有终，从而限制了工作流网有且仅有一个起始库所和一个终止库所，一个工作过程的开始都是从起始库所开始，而一个工作过程的结束也都是在终止库所结束；条件3)表示了工作流网中没有孤立的状态和条件，在图形表示上，工作流网中不存在单独出来的库所或变迁，网中所有的库所和变迁都处在起始库所到终止库所的一条有向路径上。

2　数据多点校核业务工作流网建模

2.1业务流映射与系统建模

对电力系统监控数据多点校核系统来说，处理的业务流程有以下两个方面：

1)给定某一时间点的数据库备份文件和另外某一个时间点(该时间点有可能在该备份文件的时间点之前，也有可能在备份文件的时间点之后)，完成到给定时间点的数据库的回滚或恢复；

2)给定两个不同时间点的数据库备份文件，找出该段时间上数据库中呈现的不同点。

鉴于以上两项任务，表1显示了一般的业务流程与工作流网的映射关系，可以利用这种映射关系来刻画校核系统业务流程。

基于表1的映射关系，通过定义库所、变迁节点及其关联关系，模型可以有效地描述该流程中的业务环节，并反映它们之间的时序关系。如图1所示的工作流网模型就是一个具体的校核系统业务流程的Petri网模型。该模型主要描述了用户在数据校核过程中所涉及的信息处理、交互及文件操作等。在该模型中，有两个V1表示同一个角色，也就是说，后一个V1是前一个V1的副本，两个是完全相同的。

表1　一般业务流程与工作流网的映射关系

图1　数据校核的工作流Petri网模型

该模型中的库所节点具体的对应关系如表2所示。

表2　库所节点映射关系

表3则给出了工作流模型中的变迁节点具体的对应关系。

2.2模型的化简

图1模型较为复杂不适合对其进行计算机编程[1]，因此需要对该工作流模型进行相应的化简，来验证该模型的合理性，以显示对应任何工作流实例，在没有异常情况下，处理过程都能够终止。

表3　变迁节点映射关系

下面先给出工作流网的合理性定义：

定义4(合理性)：一个工作流网WF_net=(P,T;F)是合理的，当且仅当[6]：

1)对于每一个状态i可达的状态M，存在一个实施序列，使得状态M可达状态o，可以形式化的表示为：

2)状态o是从状态i可达的唯一最终状态，而且结束时其中至少会有—个标记，可以形式化的表示为：

3)在(N,i)中不存在死变迁，可以形式化的表示为：

该条件有效地将合理性问题转化为了对Petri网动态性质的分析和验证[2]。但性质判定方法可能会受到状态空间爆炸的约束，因此，在文献[7]中研究了基于结构的分析方法，如果一个自由选择扩展工作流网基于这些规则能将其化简为只包含一个库所和一个变迁的闭环网，则该工作流网是满足合理性的。因此本文基于化简技术对图1工作流网进行分析，并使用若干保持合理性的化简规则，即可得到等价于原模型的化简模型，并最后验证。

在文献[1]提供的化简规则基础上，扩充一条化简规则(f)(如图2所示)：

图2　化简规则f

在该图所示的网中包含一个非负线性相关的库所P，如果该网中去掉该库所P，在关系上去掉与P相关的弧，这个网仍然是连通的，因此，可以化简掉库所P。

针对图1所示的工作流网模型，利用文献[3]提供的化简规则，很容易验证工作流网的合理性，化简步骤如下：

鉴于以上的化简规则，工作流网WF_net的化简过程如下：

步骤1：两次应用化简规则(b)，化简掉符合该条规则所述的库所V2和alter2，合并变迁t5和t9为T1，合并变迁t8和t10为T2，得到化简后的工作流网WF_net1，如图3所示。

图3　WF_net1

步骤2：两次应用化简规则(a)，化简掉符合条件的变迁t6和t7，合并库所V3和time3为P1，合并库所V4和time4为P2，得到化简后的工作流网WF_net2，如图4所示。

图4　WF_net2

步骤3：应用化简规则(f)，化简掉库所V1和time2以及与其相关联的弧，得到化简后的工作流网WF_net3，如图5所示。

图5　WF_net3

步骤4：应用化简规则(c)，合并库所P1和P2为P3，得到化简后的工作流网WF_net4，如图6所示。

图6　WF_net4

步骤5：多次应用化简规则(b)，先化简掉符合规则(b)中的库所V1，time1，alter1，再合并变迁t1，t3，t4和T1为T2，然后化简掉库所P3，再合并变迁t2和t8为T3得到化简后的工作流网WF_net5，如图7所示。

步骤5：应用化简规则(d)，合并变迁T2和T3为T，最终化简为只有一个起始库所、一个终止库所和一个变迁的简单网WF_net6，如图8所示。

图7 WF_net5图8 WF_net6

通过上述化简过程，将工作流网WF_net 化简为只有一个起始库所、一个终止库所和一个变迁的简单网WF_net6，说明该工作流网是满足合理性的。

2.3模型的分析与验证

计算可达图可以根据Petri网中库所状态知道其托肯在网中的流动，判断是否只有一个终点库所有托肯。因此，基于Petri网的可达图，可以模拟和仿真系统的运行，从所有的可达状态，发现系统的动态特性和运行机理，从而测试出所涉及的工作流是否能够达到预期的目标。

根据可达图算法[9]，得到校核系统的可达图，如图9所示。

图中括号里面的编码顺序为(begin，V1，time2，V1，time1，alter1，V2，V3，V4，time3，time4，alter2，end)。上述可达图模拟了系统可达的状态，反应了校核系统运行的全过程，而且，通过该图可以看出该模型能够从初始库所开始，进行两项业务的操作，最终到达到终止库所，其间没有出现死锁，并且也没有出现循环，说明该网是结构合理的。因此，如图9所示的可达图验证了校核系统运行过程中的正确性以及该工作流网的有效性，表明了该工作流能够达到预期的目的。

3　结论

基于Petri网的相关理论，本文给出了校核系统工作流的Petri 网建模方法，构建了相应的形式化模型。利用该模型可以对校核系统工作流进行分析与验证。

本文的工作一方面为校核系统工作流进行了相应的映射，提供了理论分析与验证方法，从而为校核系统的应用提供了理论支持，更验证了所建模型的合理性和正确性；另一方面，也拓宽了Petri 网模型及其理论的应用领域。相应地，新的领域和应用也必将出现新的理论课题和挑战，这也为Petri 网理论的深入研究提出了要求，有助于丰富和发展Petri 网基础理论。

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

[2] 刘清华，李璐璐，万立熊，等．工作流的动态变更处理方法[J]．计算机辅助设计与图形学学报，2011，23(1)：331-338.

[3] 李海凌，史本山，刘克剑,等．基于Petri网的建设工程项目实施阶段工作流建模与仿真[J]．计算机应用，2011，31(10)：2828-2831.

[4] 吴哲辉．Petri网导论[M]．北京：机械工业出版社，2006.

[5] 袁崇义．Petri网原理与应用[M]．北京：电子工业出版社，2005.

[6] 郝玫，王道平,等．基于Petri网的工作流建模合理性验证算法[J]．计算机工程与应用，2008,44(13)：228-231.

[7] 李建强，范玉顺,等．基于Petri网化简方法的工作流模型验证[J]．信息与控制，2001,30(6)：492-497.

[8] 吴绍艳．工程项目工作流的Petri 网表示及模型建立[J]．计算机工程与应用，2009，45(30)：10-12.

[9] 刘铁铭，范玉顺,等．基于工作流的企业过程的建模和仿真技术研究[J]．清华大学学报(自然科学版)，2000，40(1)：107-111.

[10] 李慧芳，范玉顺,等．基于时间Petri网的工作流模型分析[J]．软件学报，2004,15(1)：17-26.

[11] 卢捍华，闵丽娟，王亚石,等．工作流主从实例处理方法及其Petri网建模[J]．通信学报，2010,31(1)：92-99.

[12] 张锐，李勇，杨嘉伟,等.电力系统稳定试验数据的自动校核与优化[J]．水电能源科学，2010，28(5)：139-143.

[13] 陶佳燕，李银红，石东源,等．EMS与继电保护定值校核系统实时数据匹配新方法[J]．电力系统自动化，2012，36(10)：79-84.

[14] 刘恒，丘建栋，方杰,等．基于联网收费数据的实时滑动、动态校核的高速公路交通预测方法研究[J]．公路，2014，12(12)：134-139.

[15] 付红军，孟远景，熊浩清，等．电网运行方式综合管理系统设计与应用[J]．电力自动化设备，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。

国家自然科学基金(U1204610)；河南省基础与前沿技术研究计划项目(152300410047)；中国地震局地球物理勘探中心青年基金项目(YFGEC2014004)。

张丹(1986-)，女，河南安阳人，硕士，助理工程师，主要从事智能系统建模、数据库工作方向的研究。

佘维(1977-)，男，湖南常德人，博士，副教授，硕士生导师，主要从事Petri网理论，复杂系统建模方向的研究。