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.

Using Deterministic Theatre for Energy Management in Smart Environments

Franco Cicirelli;Libero Nigro
2020

Abstract

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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/20.500.11770/307916
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact