Using Deterministic Theatre for Energy Management in Smart Environments

This chapter introduces a deterministic version of the Theatre actor system, suited to modelling, analysis and implementation of time-critical cyber-physical systems (CPS). A Theatre model can be composed of discrete-time actors and continuous-time hybrid modes which act as an interface to continuous evolving variables of an external environment. A Theatre model can be reduced onto the Timed Automata (TA) and Hybrid TA of the Uppaal toolbox, to be property checked by the statistical model checker. The chapter develops a significant case study concerning energy management in a smart environment, like a smart home or a smart industrial plant. The goal is to orchestrates a collection of electrical appliances, which can be suspended and reactivated, so as to exploit to a largest extent the power generated by a local source of energy, like a photovoltaic panel, a wind turbine etc. The system, though, is also able to use energy from an exter-nal provider, with a control policy to avoid extra costs, when the local power generator sharply reduces its production. The chapter describes the case study and presents an experimental analysis aimed at comparing different power load scheduling strategies.