论文部分内容阅读
摘要：就目前来看，我国智能配电网呈现良好的发展趋势。形式化校验技术在只能配电网自愈中的应用范围逐步扩展，具有广阔的发展前景，主要在于形式化验技术在智能配电网系统中能够实现逻辑控制与验证。本文主要针对形式化校验技术原理与智能配电网自愈技术进行深入分析，探究形式化校验技术在智能配电网自愈中的发展应用。
关键词：形式化校验技术；智能配电网；自愈；发展；应用
一、前言
根据智能配电网自愈控制系统具备的功能，将其划分为三个结构层，即决策层、支撑层以及执行层。决策层，主要代表的具有决策功能的配电系统；支撑层，主要代表的是具有支撑能力的电网系统；执行层，主要代表的是具有执行功能的智能电子设备。现阶段，随着智能电网的快速发展，在自动化方面提出了更高的要求，现有技术已经能够有效实现分布式决策，有利于电网处理环节的减少与自动控制功能的实现，还能够在很大程度上降低人为操作失误现象的发生率。但是，智能配电网中的执行设备较为复杂，所以智能配电网在自愈执行问题上存在限制，针对这一实际问题，在智能配电网自愈中应当重视形式化校验技术的合理应用。
二、形式化校验技术的原理分析
形式化校验技术，实质上就是在系统功能中实现数学的一种保证程序，在防崩溃操作系统、核心算法、安全问题、航天探测以及安全协议等多个方面的均有所应用，在配电网中的应用范围正在逐渐扩展。现阶段，智能配电网模型检测方面，形式化校验技术已经实现了安全协议、控制系统、硬件以及通信协议的应用；形式化校验技术的使用控制，主要是通过搜索，对全自动控制系统的程序进行规范设计。当无法实现搜索的时候，能够将原有指令结束，并且给出合理的指示，形式化校验技术可以有效解决系统设计过程中存在的差异问题，有利于排除智能配电网自愈中的障碍。目前，我国电网科研机构，已经实现了形式化校验技术的可操作性，能够确保电网模型检测自愈自动化的实现，其中含有的SPIN程序，是以现代计算机技术为基础实现的一项形式化校验技术，对于系统逻辑性与分析验证的有机结合具有十分重要的作用。
SPIN程序，主要是通过对系统执行完成进行模拟，利用优先的深度体验，以此保证系统探测状态的稳定，对系统属性是否正常进行校验处理，若是发现不正常状况，能够通过系统运行轨迹，将配电网中程序发生错误的状况显示出来。
如图1所示，SPIN的建模语言为Promela，用线性时态逻辑（LTL）公式刻画系统的时候，应当满足相应的性质。验证过程中，若是模型与LTL公式刻画出现的属性相符，那么就代表该模型存在一定缺陷，SPIN会将反例呈现出来。
SPIN程序下，Promela建模语言提供的自动机制，对于电网系统的运行存在不确定性，主要通过以下几个步骤实现模拟检验：①通过Promela建模语言校验检测系统，重点在于抽象模拟电网系统，以此有效的解决状态爆炸问题。②根据已经建立完成的模型，通过LTL公式刻画需要对其进行验证处理的属性，LTL公式可以将所关心的性质完整、正确的刻画出来，是保证验证结果合理化的基础；通常情况下，应当包含对系统安全性进行验证的LTL公式与对系统正确性进行验证的LTL公式。③模型验证，通过SPIN校验LTL公式，实质上就是在有限状态空间中的一个穷举搜索过程，若是模型无法满足公式的验证要求，SPIN就会呈现出相应的反例与执行轨迹，以此对错误出现的位置进行定位，并且找出算法存在的缺陷。
三、形式化校验技术在智能配电网自愈中的应用分析
智能配电网自愈中，形式化校验技术的应用，主要包括故障修复、故障诊断、故障提示三个方面。
1、故障修复
在故障修复过程中，应当加大测试的维护力度，这样能够在很大程度上提高系统的稳定性；就目前来看，测试只会在定位系统中完成输入，所以形式化校验系统能够促进非针对性电网系统自愈故障维护的实现，并且确保系统的实际行为与期望行为处于一致状态。对可以输入测试电网中存在的故障进行维护时，应当采用形式仿真技术，以此确保电网故障行为的控制符合预期标准，因为负荷过程中分布式电源存在不确定性，如电网机械故障、信号干扰等一系列因素，均会对电网系统的执行能力造成影响，因此形式仿真技术存在局限性。确保智能配电网自愈控制的合理性，应当拓展传统技术，以此在执行保护方面保证系统操作的安全性、稳定性；同时，形式化校验技术，可以为电网系统的执行行为提供保障。维护过程中，形式化校验技术可以通过静态分析实现，形式化校验技术不仅可以保证电网验证算法与功能要求相符合，还能够通过故障的反例完成维护分析，对于协议、算法存在一定程度的缺失补充，通过不断整合电网模型，以此满足相应算法、协议的需求。
2、故障诊断
智能电网在处于故障装药下运行时，能够通过形式的因果关系，迅速确定发生故障的主要原因。通常采用的方法，主要为LTL公式及智能配电网故障模拟信息借用高压输电线故障诊断，该方法适合在配电网运行故障原因无法明确的情况下应用，还有配电网在不具备任何条件的情况下进行变量检测，以此找出发生故障的原因，对于准确、迅速排出故障，保障配电网系统处于一个正常的运行状态具有十分重要的意义。
3、故障提示
配电网发生故障的时间与故障影响之间存在密切的联系，可以通过时序逻辑对配电网故障发生原因进行分析与研究，智能配电网在运行过程中，主要依赖于决策层、执行层以及支撑层三者之间互相独立与联系，确保通信体系处于一个完整的状态。通信元件发生故障之后，配电网系统可能会出现非正常运行状况，所以配电系统故障提示就显得尤为重要。通过形式化校验技术具备的建模语言，能够迅速的找到配电网系统运行过程中出现的故障，配电网系统也能够在最短时间内对整个操作流程作出相应的提示，在故障发生的一瞬间立即报警，在很大程度上避免了配电网系统由警戒状态转变为故障状态，有效降低了配电网系统故障造成的经济损失，也为相关维护工作的开展争取了足够的时间。
四、结语
SPIN的建模语言为Promela，可以将其在分布式系统的逻辑验证中进行应用，该模型检测方法的效果十分显著。通过形式化校验技术，能够建立一个实时反映配电网系统运行结果与职能配电网自愈控制元件实效序列之间关系的因果数据库，并且将其应用于配电网系统处于正常运行状态下的风险分析与处于警戒状态下的预防性处理过程中的故障诊断与故障预警。智能配电网处于故障状态的时候，对于一些核心控制算法，如快速处理等，可以通过形式化化验技术进行模型验证，能够保证核心算法的合理性、有效性以及运行条件未确定时的安全性，为智能配电网自愈提供一个安全、有效的技术保障。同时，在智能配电网自愈中应用形式化校验技术，有利于配电网故障修复、故障诊断以及故障提示的实现；所以，应当重视形式化校验技术的整合发展，特别是协议与算法之间的综合利用，重视形式化校验技术发展的不断革新。
参考文献：
[1]刘健，崔琪.一种快速自愈的分布智能馈线自动化系统[J].电力系统自动化，2010（04）：62-63.
[2]周学斌，段斌，吴义方.基于IEC无缝通信体系的电网自愈控制研究[J].华东电力，2010（07）：1028-1029.
[3]凌万水，刘东，洪俊.形式化校验技术在智能配电网自愈中的应用[J].电力系统自动化，2012（18）.
[4]南周羽.形式化校验技术在智能配电网自愈中的应用[J].农网智能化，2014（01）.
关键词：形式化校验技术；智能配电网；自愈；发展；应用
一、前言
根据智能配电网自愈控制系统具备的功能，将其划分为三个结构层，即决策层、支撑层以及执行层。决策层，主要代表的具有决策功能的配电系统；支撑层，主要代表的是具有支撑能力的电网系统；执行层，主要代表的是具有执行功能的智能电子设备。现阶段，随着智能电网的快速发展，在自动化方面提出了更高的要求，现有技术已经能够有效实现分布式决策，有利于电网处理环节的减少与自动控制功能的实现，还能够在很大程度上降低人为操作失误现象的发生率。但是，智能配电网中的执行设备较为复杂，所以智能配电网在自愈执行问题上存在限制，针对这一实际问题，在智能配电网自愈中应当重视形式化校验技术的合理应用。
二、形式化校验技术的原理分析
形式化校验技术，实质上就是在系统功能中实现数学的一种保证程序，在防崩溃操作系统、核心算法、安全问题、航天探测以及安全协议等多个方面的均有所应用，在配电网中的应用范围正在逐渐扩展。现阶段，智能配电网模型检测方面，形式化校验技术已经实现了安全协议、控制系统、硬件以及通信协议的应用；形式化校验技术的使用控制，主要是通过搜索，对全自动控制系统的程序进行规范设计。当无法实现搜索的时候，能够将原有指令结束，并且给出合理的指示，形式化校验技术可以有效解决系统设计过程中存在的差异问题，有利于排除智能配电网自愈中的障碍。目前，我国电网科研机构，已经实现了形式化校验技术的可操作性，能够确保电网模型检测自愈自动化的实现，其中含有的SPIN程序，是以现代计算机技术为基础实现的一项形式化校验技术，对于系统逻辑性与分析验证的有机结合具有十分重要的作用。
SPIN程序，主要是通过对系统执行完成进行模拟，利用优先的深度体验，以此保证系统探测状态的稳定，对系统属性是否正常进行校验处理，若是发现不正常状况，能够通过系统运行轨迹，将配电网中程序发生错误的状况显示出来。
如图1所示，SPIN的建模语言为Promela，用线性时态逻辑（LTL）公式刻画系统的时候，应当满足相应的性质。验证过程中，若是模型与LTL公式刻画出现的属性相符，那么就代表该模型存在一定缺陷，SPIN会将反例呈现出来。
SPIN程序下，Promela建模语言提供的自动机制，对于电网系统的运行存在不确定性，主要通过以下几个步骤实现模拟检验：①通过Promela建模语言校验检测系统，重点在于抽象模拟电网系统，以此有效的解决状态爆炸问题。②根据已经建立完成的模型，通过LTL公式刻画需要对其进行验证处理的属性，LTL公式可以将所关心的性质完整、正确的刻画出来，是保证验证结果合理化的基础；通常情况下，应当包含对系统安全性进行验证的LTL公式与对系统正确性进行验证的LTL公式。③模型验证，通过SPIN校验LTL公式，实质上就是在有限状态空间中的一个穷举搜索过程，若是模型无法满足公式的验证要求，SPIN就会呈现出相应的反例与执行轨迹，以此对错误出现的位置进行定位，并且找出算法存在的缺陷。
三、形式化校验技术在智能配电网自愈中的应用分析
智能配电网自愈中，形式化校验技术的应用，主要包括故障修复、故障诊断、故障提示三个方面。
1、故障修复
在故障修复过程中，应当加大测试的维护力度，这样能够在很大程度上提高系统的稳定性；就目前来看，测试只会在定位系统中完成输入，所以形式化校验系统能够促进非针对性电网系统自愈故障维护的实现，并且确保系统的实际行为与期望行为处于一致状态。对可以输入测试电网中存在的故障进行维护时，应当采用形式仿真技术，以此确保电网故障行为的控制符合预期标准，因为负荷过程中分布式电源存在不确定性，如电网机械故障、信号干扰等一系列因素，均会对电网系统的执行能力造成影响，因此形式仿真技术存在局限性。确保智能配电网自愈控制的合理性，应当拓展传统技术，以此在执行保护方面保证系统操作的安全性、稳定性；同时，形式化校验技术，可以为电网系统的执行行为提供保障。维护过程中，形式化校验技术可以通过静态分析实现，形式化校验技术不仅可以保证电网验证算法与功能要求相符合，还能够通过故障的反例完成维护分析，对于协议、算法存在一定程度的缺失补充，通过不断整合电网模型，以此满足相应算法、协议的需求。
2、故障诊断
智能电网在处于故障装药下运行时，能够通过形式的因果关系，迅速确定发生故障的主要原因。通常采用的方法，主要为LTL公式及智能配电网故障模拟信息借用高压输电线故障诊断，该方法适合在配电网运行故障原因无法明确的情况下应用，还有配电网在不具备任何条件的情况下进行变量检测，以此找出发生故障的原因，对于准确、迅速排出故障，保障配电网系统处于一个正常的运行状态具有十分重要的意义。
3、故障提示
配电网发生故障的时间与故障影响之间存在密切的联系，可以通过时序逻辑对配电网故障发生原因进行分析与研究，智能配电网在运行过程中，主要依赖于决策层、执行层以及支撑层三者之间互相独立与联系，确保通信体系处于一个完整的状态。通信元件发生故障之后，配电网系统可能会出现非正常运行状况，所以配电系统故障提示就显得尤为重要。通过形式化校验技术具备的建模语言，能够迅速的找到配电网系统运行过程中出现的故障，配电网系统也能够在最短时间内对整个操作流程作出相应的提示，在故障发生的一瞬间立即报警，在很大程度上避免了配电网系统由警戒状态转变为故障状态，有效降低了配电网系统故障造成的经济损失，也为相关维护工作的开展争取了足够的时间。
四、结语
SPIN的建模语言为Promela，可以将其在分布式系统的逻辑验证中进行应用，该模型检测方法的效果十分显著。通过形式化校验技术，能够建立一个实时反映配电网系统运行结果与职能配电网自愈控制元件实效序列之间关系的因果数据库，并且将其应用于配电网系统处于正常运行状态下的风险分析与处于警戒状态下的预防性处理过程中的故障诊断与故障预警。智能配电网处于故障状态的时候，对于一些核心控制算法，如快速处理等，可以通过形式化化验技术进行模型验证，能够保证核心算法的合理性、有效性以及运行条件未确定时的安全性，为智能配电网自愈提供一个安全、有效的技术保障。同时，在智能配电网自愈中应用形式化校验技术，有利于配电网故障修复、故障诊断以及故障提示的实现；所以，应当重视形式化校验技术的整合发展，特别是协议与算法之间的综合利用，重视形式化校验技术发展的不断革新。
参考文献：
[1]刘健，崔琪.一种快速自愈的分布智能馈线自动化系统[J].电力系统自动化，2010（04）：62-63.
[2]周学斌，段斌，吴义方.基于IEC无缝通信体系的电网自愈控制研究[J].华东电力，2010（07）：1028-1029.
[3]凌万水，刘东，洪俊.形式化校验技术在智能配电网自愈中的应用[J].电力系统自动化，2012（18）.
[4]南周羽.形式化校验技术在智能配电网自愈中的应用[J].农网智能化，2014（01）.