馈线自动化算法的形式化建模与验证

摘要

分布式馈线自动化系统能否正确运作,目前主要是通过测试与仿真技术来保证,但这2类方法都要涉及电气设备的底层细节,会分散计算资源,影响验证效率,且难以覆盖足够的系统路径.针对该问题,提出一种馈线自动化算法的验证方法.通过对电气设备行为与特征的抽象,建立馈线自动化算法的形式化模型,在此基础上,使用自动化模型检测技术验证算法的正确性.测试结果表明,该方法将计算资源集中在动作逻辑验证上,实现了与底层细节的分离,从而能够获得较高的验证效率,完整覆盖系统路径,并有效降低缺陷修正的代价.