Formal specification of a self-sustainable holonic system for smart electrical micro-grids

Stand-alone micro-grids have emerged within the smart grids field, facing important challenges related to their proper and efficient operation. An example is the self-sustainability when the micro-grid is disconnected from the main utility, e.g., due to a failure in the main utility or due to geographical situations, which requires the efficient control of energy demand and production. This paper describes the formal specification of a holonic system architecture that is able to perform the automation control functions in electrical stand-alone micro-grids, particularly aiming to improve their self-sustainability. The system aims at optimizing the power flow among the different electrical players, both producers and consumers, to keep the micro-grid operating even under adverse situations. The behaviour of each individual holon and their coordination patterns were modelled, analysed and validated using the Petri net formalism, allowing the complete verification of the system correctness during the design phase.