Rigorous Automated Verification of Protection Systems in LV Distribution Grids

In power systems protection, selectivity is a key property that must be guaranteed. It ensures the minimum amount of load is unfed when a fault occurs and it reduces the time needed to restore service. Selectivity is achieved through coordination of circuit breakers (CBs), whose logic is most commonly determined by a combination of time and current thresholds. Verifying the correctness of CBs' settings is crucial when designing power system protections and may become a challenging task for big networks. This paper proposes an approach for the rigorous verification of the correct configuration of protection systems in low-voltage (LV) distribution grids. The method utilized depends on a precise model that employs Timed Automata (TA) to represent the crucial elements of an LV distribution grid. Additionally, it incorporates a system for producing and validating formal models from higher-level JSON-based depictions of electrical networks, taking advantage of the Uppaalmodel checker. The effectiveness of the approach has been tested on several realistic power systems.