Automated formal verification for microgrids protection systems

Generated distribution units are becoming increasingly present thanks to economic benefits deriving from their installment, yet they bring specific problems, e.g. network instability and protection system errors. The goal of this work is creating a software for formal verification of specific desirable characteristics of a protection system applied to a microgrid. Such a software must cover three functions. First, it must be able to graphically represent an electric network, including the capability to load and save it as a file. Then it must be able to automatically generate a model for formal verification of the analyzed network, including the specification to be checked. Lastly, it must be able to formally verify the model, giving a feedback to the user. In this work, RSE’s CIMDraw, a software for graphic representation of electric networks, is extended to include missing required components for this work. Then, a formal model able to capture the peculiarities of microgrids is proposed in TRIO and Zot languages and used to efficiently analyze case studies. Lastly, a software capable of automatic generating code for Zot based on a CIMDraw output is presented.

La generazione distribuita si sta diffondendo, anche grazie alle agevolazioni economiche nell’installazione di micro-impianti ad energie rinnovabili, tuttavia porta con sé alcuni specifici problemi, come instabilità della rete ed errori del sistema di protezioni. L’obiettivo di questo lavoro è creare un software per la verifica formale di specifiche caratteristiche desiderabili in un sistema di protezione applicato a una microrete. Un software completo per questa finalità deve ricoprire tre funzioni. Dapprima deve poter permettere la rappresentazione grafica di reti elettriche, inclusa la possibilità di caricarle e salvarle sotto forma di file. Tale software deve poi poter generare automaticamente un modello per la verifica formale della rete analizzata, includendo la specifica che si vuole verificare. Infine, deve essere effettuata la verifica formale fornendo un feedback all’utilizzatore. In questo lavoro viene esteso CIMDraw, un software di RSE per la rappresentazione grafica di reti elettriche, così da includere componenti necessarie. Poi viene proposto un modello formale capace di catturare le peculiarità delle microreti, presentandolo in linguaggio TRIO e in linguaggio Zot, usato per analizzare efficacemente dei casi studio. Infine, viene presentato un software capace di generare automaticamente il modello per Zot a partire dal file di output di CIMDraw.