Formal specification and verification of a distributed fault localization,isolation and supply restoration algorithm

Abstract

Distributed fault localization, isolation and supply restoration (FLISR) algorithm only uses local topology information to improve system reliability in electric power enterprises. It has better adaptability than traditional centralized control architecture. To verify the correctness and reliability of the distributed FLISR algorithm which applied to complex distribution network is very important in the operation of distribution network. A formal method for the specification and verification of the distributed FLISR algorithm which uses linear temporal logic (LTL) language is presented in this paper. In addition, the correctness of the algorithm in interference-free situation and the security of the algorithm in some uncertain interference such as switch action failure, communication failure and other confounding factors are proved mathematically.

Keywords

Fault localization isolation and supply restoration distribution network linear temporal logic formal specification and verification

References

Lin

C.-H.

, Chen

C.-S.

, Ku

T.-T.

et al., A multiagent-based distribution automation system for service restoration of fault contingencies, European Transactions on Electrical Power 21(1) (2011), 239-253.

Higgins

, Vyatkin

, Nair

N.K.C.

et al., Distributed power system automation with IEC 61850, IEC 61499, and intelligent control, Systems, Man, and Cybernetics, Part C: Applications and Reviews 41(1) (2010), 81-92.

Wang

, Ma

and Gao

, A multi-agent based approach to the distributed feeder automation system, Automation of Electric Power Systems 34(6) (2010), 54-57.

, Xie

and Li

, Research of feeder automation system based on multi-agent, 2008 3rd IEEE Conference on Industrial Electronics and Applications (ICIEA 2008), Singapore, (2008), 538-541.

Kröger

and Merz

, Temporal logic and state systems, Springer, 2008.

Banach

, Formal methods, Journal of Universal Computer Science 13(5) (2007), 593-601.

Maier

, Intuitionistic LTL and a new characterization of safety and liveness, Computer Science Logic, Springer Berlin Heidelberg, (2004), 295-309.

Alice

, Alastair

and Muffy

, Symmetry in temporal logic model checking, ACM Computer Surveys 38(3) (2006), 136-152.

Tabuada

and Pappas

G.J.

, Linear time logic control of discrete - time linear systems, IEEE Transactions Automatic Control 51(12) (2006), 1862-1877.

10.

Roychoudhury

, Embedded systems and software validation, Morgan Kaufmann, 2009.

11.

Weng

, Liu

et al., A feeder automation simulation test environment based on parallel computation, Automation of Electric Power Systems 33(7) (2009), 43-46, 51.

12.

Ling

, Liu

and Liu

, The evaluation method of feeder automation algorithm robustness under the condition of communication failures, 2010 China International Conference on Electricity Distribution (CICED 2010), Nanjing, China, (2010).