Verification of a Smart Power Control System using Hybrid Actors

This paper proposes an approach to modelling and analysis of time-critical cyber-physical systems (CPSs). The approach combines discrete-time actors with continuous modes which reproduce the dynamical laws by which some external variables change their value. In particular, the article introduces Hybrid Theatre which is an original actor formalism and an implementation framework in Java, for the development of CPSs. A Hybrid Theatre model is mapped onto Uppaal hybrid timed automata for property assessment by statistical model checking. A smart power control system in a micro grid is presented as a case study to demonstrate the usefulness of the proposed approach.