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

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