Model Checking Cyber-Physical Energy Systems

Cyber-Physical Systems (CPS) integrates computing and physical processing: their behaviour is dictated by both computation and physical components. In this paper, we present a Model Checking approach for the automatic verification of the correctness of the system at hand. The strengths of our approach are the followings. First, we have implemented the CPS using the modelling and simulation based software JModelica to exploit its modular and parametrizables components. Second, we have verified the system's properties with a model-checking technique to exploit the automaticity of this approach and the completeness of the exploration of all the states of the CPS. In fact, with very few basic notions of the field to investigate, it is possible to design a complete model of a CPS. The system we model, for our proof of concept, is a Distributed Maximum Power Point Tracking (DMPPT) for photovoltaic systems, which relies on a control software to manage the system in every condition imposed by the environment (e.g. irradiation, temperature). We have parameterized the main physical inputs to carry out an automatic verification of a thorough simulation of the circuit under a large number of operational conditions, to deeply investigate the critical aspects of the system. The final goal of our study has been to design a tool to enable automatic verification using a model-checking approach in order to ensure the system correctness with respect to given requirements provided by the designer.