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.

Verification of a Smart Power Control System using Hybrid Actors

Libero Nigro
Membro del Collaboration Group
;
Paolo F. Sciammarella
Membro del Collaboration Group
2019

Abstract

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.
Cyber-physical systems, formal modelling, actors, hybrid automata, Statistical Model Checking, Uppaal, smart power micro grid.
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: https://hdl.handle.net/20.500.11770/295157
 Attenzione

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

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