摘要：

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

关键词: 馈线自动化, 形式化模型, 自动验证, 模型检测, 时间自动机

Abstract:

Testing and simulation are main technologies used to ensure the proper running of distribution feeder automation system.But they both refer to the low-level details of electrical equipment so that the computing resources are scattered,affecting the verification efficiency and the coverage of system paths.For this problem,a new verification method for distribution feeder automation system is proposed.The formal model of the feeder automation algorithm is built by abstracting the actions and features of electrical equipment.Then,the automatic model checking technology is used to verify the correctness of the algorithm.Test results show that,this verification method focuses computing resources on the verification of action logic of algorithm by separating the low-level details.So it has higher verification efficiency and covers all system paths,and it can also reduce the cost of bug fixing.

Key words: feeder automation, formal model, automatic verification, model checking, timed automata

中图分类号: 

• TP311