A Formal Approach to the Verification of Protection Systems in Low-Voltage Distribution Grids

Power systems have mechanisms-so-called protection systems-to automatically disconnect parts of the electrical network when faults occur, to isolate the faulty part of the system. These mechanisms rely on devices, called circuit breakers, that automatically open when a fault is detected. The logic for opening circuit breakers is most commonly based on a combination of timing properties of the devices and current thresholds. The logic is configured at design time, and it is crucial that it achieves selectivity, that is, that it only disconnects the relevant part of the network, thus minimizing the amount of unfed load. In this paper, we present an approach to formally verify the correct configuration of the protection systems in a low-voltage (LV) distribution grid. In particular, the approach relies on a formal model, based on Timed Automata, of the relevant elements of an LV distribution grid. It also includes a mechanism to automatically generate and verify formal models starting from higher-level, JSON-based descriptions of electrical networks. The formal verification mechanism exploits the UPPAAL model checker. The paper presents some experimental results that show the promise of the proposed approach.