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

《基于IEC 61850的智能电子设备交互模型形式化描述与验证-论文.pdf》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、第36卷第17期电力系统自动化Vo1．36No．172012年9月i0日AutomationofElectricPowerSystemsSept．10，2012基于IEC61850的智能电子设备交互模型形式化描述与验证张其林，王先培，杜双育，赵宇(武汉大学电子信息学院，湖北省武汉市430079)摘要：IEC61850将变电站智能电子设备(1ED)的功能抽象成若干逻辑节点，以达到信息交换的目的。lED及其逻辑节点之间的交互关系复杂，如何正确地设计并实现这种复杂的行为是IEC61850实施的关键。形式化方法为此提供了良好的途径。提出采用进程代数方法对各种功能

2、在1ED之间、IED内部逻辑节点之间的交互关系、系统行为进行严谨地描述并进行自动验证，以保证分布式功能的正确性。以定时过电流保护功能为例，建立了基于IEC61850的IED交互模型，采用在通信顺序进程(CSP)上加入时间相关操作形成的形式化语言TimedCSP描述其交互功能及系统行为，在验证工具——进程分析工具包(PAT)环境中进行了验证。结果表明，所提出的方法能有效地检测出描述中潜在的缺陷，有利于指导IED交互系统的设计并节约开发成本。关键词：IEC61850；智能电子设备；形式化；通信顺序进程0引言很抽象。文献[7]研究了基于IEC61850的变压器

3、lED的设计，以模块化的方法设计了IED嵌入式软随着数字化变电站的发展，基于IEC61850的件。文献[8]基于面向对象的方法对线路电流差动变电站自动化是一种必然趋势[1]。电网结构日趋复保护IED进行设计。文献[9]依据IEC61850，建立杂、容量不断扩大、实时信息传送量成倍增多，对变了牵引变电站线路保护IED的对象模型。文电站智能电子设备(IED)提出了更高的要求。新开献[1O]N用配置文档动态地生成IED的模型。文发的IED必须具备高效快速的处理能力，以满足大献[11]研究利用可编程逻辑语言的与门、或门对量信息传输的实时性、可靠性和多任务性。目前

4、，新lED内部的LN之间关系进行可视化设计，但未能型的lED多采用数字信号处理器(DSP)+ARM完整地描述和严谨地设计IED之间和IED内部各(advancedRISCmachines)双中央处理器(CPU)结LN之间的逻辑关系。电力系统lED是一种系统行构_2]，甚至出现了集成多功能的集中式IED[3]。随为与时间紧密相关的嵌入式系统，其设计、实现与验着硬件可靠性的提高，IED的可靠性越来越依赖嵌证比较复杂。已有文献中，IED的开发过程缺乏对入式软件的质量。IEC61850为变电站内IED之间系统行为的有效建模，以及在设计阶段对系统关键的互操作提供途

5、径，其应用的关键在于利用标准的行为进行分析与检验等方面的研究工作。模型对实际的IED进行建模，将其功能抽象成若干通信顺序进程(CSP)l_1是Hoare于1978年建逻辑节点(LN)，以达到信息交换的目的¨4]。为了更立的一种适合于分布式并发软件规格和设计的形式好地实现分布式功能在IED上的标准化设计，需要化方法，已经广泛地应用于软件的行为建模。它以事先对各种功能在IED之间和lED内部LN之间进程的方式刻画系统的动态行为，具有强大的描述的交互关系、系统行为进行严谨描述与验证，以保证能力。已有基于CSP的验证工具——进程分析工分布式功能的正确性_5]。具

6、包(PAT)口。]可以对系统中的死锁、活锁、可达性已有相关文献研究了基于IEC61850的各种等安全问题进行自动化验证。在CSP基础上加入lED的设计开发方法。文献[1]研究了IEC61850时间相关操作而形成的一种形式化语言Timed下间隔层lED软件设计方案，分析了IED的功能模CSP_1，能够对实时的并发系统进行良好的描述。型。文献[63给出了保护功能一般性建模方法，但仍本文采用TimedCSP对IED内各LN的交互关系、收稿日期：2O1l一11-24；修回日期：2012-03-08。系统行为进行描述并验证，进而指导lED的软件设国家自然科学基金资

7、助项目(50677047)；湖北省自然科学基计和互操作测试实验。金资助项目(2010CDZ051)；湖北省教育厅基金资助项目(D20092505)。·研制与开发·张其林，等基于IEC61850的智能电子设备交互模型形式化描述与验证1TimedCSP简介P⋯Q：异步并发，进程所执行的每个事件为进程P或Q中的～个事件。TimedCSP中最基本的概念是事件和时间。X·F(X)：X是一个进程变量，A—aX，F(X)通常用小写字母a，b，C或自定义字符串表示事件。称为包含进程变量X的一个前缀表达式，且该递归事件的序列形成进程，通常用大写字母P，Q或自定方程具有事件

8、符号集A上的唯一解。义字符串表示。√是一种特殊的事件，表示进程正t1t0￡q常终