Efficient Verification of Protection System Configuration of Electrical Distribution Grids

Protection systems are a crucial part of the electric power system. A tool has been developed to formally verify the correct configuration of protection systems in a low-voltage distribution grid. It uses a formal model, based on Timed Automaton, representing the relevant elements of a low-voltage distribution grid. The developed tool encountered several challenges related to the limited number of faults it could handle and the significant amount of time required for the verification process. Additionally, the verification output was hard to interpret, and in cases of multiple incorrectly configured circuit breakers, only the first one detected by the tool was presented to the user. This paper proposes a solution to address these challenges by implementing two versions of the procedure called Automatic Subdivision of Queries (ASQ) in the tool, namely ASQ<inf xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">α</inf> and ASQ<inf xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">Ω</inf>, to overcome these challenges.