Formal validation of supervisory energy management systems for microgrids

An energy management system of a microgrid (MG) has several basic objectives; e.g. to maximize the utilization of renewable energy resources (RES), to protect the internal components from overloading, and to ensure that the MG operates reliably under any operating conditions. Although many control techniques are available in the literature to monitor and control the energy flows among distributed RES in MGs, formal verification of those techniques was not proposed yet. The emphasis of this paper is to design and validate energy management system for a MG which consists of a solar photovoltaic (PV) array, a pair of battery energy storage systems (BESes), a diesel generator (DG) and a load (LD). The physics and dynamics of the MG are defined as energy flow invariants and the designed behaviours are abstracted, modelled and validated in this work. Therefore, we have considered an invariant based flow technique to manage the energy flow in an MG. The results are validated and verified with UPPAAL, a powerful industrial tool which is commonly used to verify the correctness of real-time systems like supervisory controllers, communication protocols and others.