Application of formal verification theory to microgrid protection systems

Microgrids are typically low-voltage electrical distribution systems to which distributed energy resources and controllable loads are connected. They are able to operate both connected to the medium voltage network or in island. The microgrid concept aims to move from the “fit and forget” philosophy (typical of today's distribution networks) to a massive integration of distributed generation through the implementation of control logics able to guarantee the stability and the equilibrium of the microgrid under every operating condition. Coordination and control of distributed generation and loads is the key feature that distinguishes microgrids from dimple distribution feeders. However, their implementation poses major technical challenges, such as microgrid protection from faults or undesired operation. Distributed generation, connected to island-operated microgrids, can cause protections selectivity and sensitivity issues in case of fault. The aim of this thesis is to study and define a tool based on the theory of formal verification. This tool is able to highlight issues and flaws caused by incorrect design of the protection logics or due to a mismatch between the settings of the protection logics with respect to the real status of the network. This objective has been achieved by implementing a series of logical-temporal models, able to simulate the real dynamics of a protection system and to demonstrate, by means of formal tests, whether the model violates or not the properties for which the verification is required. This goal has been achieved by relying on different standards (i.e., UML, CIM, XLM-RDF), logical-languages (TRIO), and by using some dedicated support software (i.e., CIMDraw and Zot).

Le microreti sono, tipicamente, sistemi elettrici di distribuzione in bassa tensione a cui sono connesse risorse energetiche distribuite e carichi controllabili. Sono in grado di funzionare sia collegate alla rete di media tensione che in isola. Il concetto di microrete mira a passare dalla filosofia “fit and forget” (tipica delle reti di distribuzione odierne) verso un'integrazione più massiccia della generazione distribuita attraverso l’implementazione di logiche di controllo in grado di garantire la stabilità e l’equilibrio della microrete in ogni condizione operativa. Coordinazione e controllo della generazione distribuita e dei carichi è la caratteristica fondamentale che distingue le microreti dalle linee di distribuzione. Tuttavia, la loro implementazione pone grandi sfide tecniche, come la protezione dai guasti e da funzionamenti anomali. La generazione distribuita, combinata alla gestione in isola della microrete può far emergere problemi di selettività e sensibilità delle protezioni in caso di guasto. Lo scopo di questa prima fase di ricerca ha come obiettivo quello di studiare e definire un possibile strumento di analisi basato sulla teoria della verifica formale. Tale strumento è in grado di mettere in evidenza eventuali criticità o malfunzionamenti causati da un’errata progettazione delle logiche di protezione o a causa di una mancata corrispondenza tra la configurazione delle logiche di protezione con lo stato reale della rete. Tale obiettivo è stato raggiunto implementando una serie di modelli logico temporali, in grado di simulare le dinamiche reali di un sistema di protezione arrivando a dimostrare, per mezzo di test formali, se il modello realizzato viola o meno le proprietà che si intende verificare. Il raggiungimento di tale obiettivo è stato reso possibile facendo riferimento ad alcuni standard (UML, CIM, XLM-RDF) e grazie all’utilizzo di linguaggi logici (TRIO) ed alcuni software di supporto (CIMDraw e Zot).