基于IEC 61850的智能电子设备交互模型形式化描述与验证

Formal Specification and Verification of Intelligent Electronic Device Interaction Model Based on IEC 61850

IEC 61850将变电站智能电子设备(IED)的功能抽象成若干逻辑节点,以达到信息交换的目的。IED及其逻辑节点之间的交互关系复杂,如何正确地设计并实现这种复杂的行为是IEC 61850实施的关键。形式化方法为此提供了良好的途径。提出采用进程代数方法对各种功能在IED之间、IED内部逻辑节点之间的交互关系、系统行为进行严谨地描述并进行自动验证,以保证分布式功能的正确性。以定时过电流保护功能为例,建立了基于IEC 61850的IED交互模型,采用在通信顺序进程(CSP)上加入时间相关操作形成的形式化语言Timed CSP描述其交互功能及系统行为,在验证工具——进程分析工具包(PAT)环境中进行了验证。结果表明,所提出的方法能有效地检测出描述中潜在的缺陷,有利于指导IED交互系统的设计并节约开发成本。

In IEC 61850,functions of substation intelligent electronic devices（IEDs） can be divided into several logic nodes in order to achieve the purpose of information exchange.There are complex interactive relationships among IEDs and their internal logic nodes（LNs）.How to design and implement this kind of complex behaviors is a key for application of IEC 61850.Formal method may provide a good way.The rigorous description and automatic verification with process algebra for the interaction functions and system behaviors among IEDs and the internal LNs of IEDs are put forward in order to guarantee correction of distribute functions.The IEDs interaction model based on IEC 61850 for time over-current protection is established and the interaction functions and system behaviors are described with Timed communicating sequential processes（CSP）,then automatic verification is done on process analysis toolkit（PAT） platform.Test results show that the method proposed can effectively detect potential defects in specification so as to guide the design of interactive systems of IEDs and save development costs.