This paper introduces Hybrid Theatre, an actor-based language and runtime system suited to the modelling, analysis and implementation of cyber-physical systems (CPSs). Hybrid Theatre separates in a clear way the aspects of a CPS model concerning the dynamical laws of the external environment, expressed by continuous modes, and their interaction with the discrete-time, discrete-event actor-based controlling software. The paper highlights the modelling language of Hybrid Theatre, clarifies its operational semantics, and demonstrates its practical application through a CPS modelling example referring to the automotive domain, where selected actors communicate through a Controller Area Network (CAN) serial bus, whereas other actors rest on wire connections. For property checking a Hybrid Theatre model is reduced on to the Uppaal Statistical Model Checker which is then exploited for the assessment of functional and temporal behavior of the chosen model. The paper concludes by discussing problems about how a Hybrid Theatre model can be transitioned without distortions toward its synthesis, and by giving indications of further work.

Statistical Model Checking of Cyber-Physical Systems using Hybrid Theatre

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

Abstract

This paper introduces Hybrid Theatre, an actor-based language and runtime system suited to the modelling, analysis and implementation of cyber-physical systems (CPSs). Hybrid Theatre separates in a clear way the aspects of a CPS model concerning the dynamical laws of the external environment, expressed by continuous modes, and their interaction with the discrete-time, discrete-event actor-based controlling software. The paper highlights the modelling language of Hybrid Theatre, clarifies its operational semantics, and demonstrates its practical application through a CPS modelling example referring to the automotive domain, where selected actors communicate through a Controller Area Network (CAN) serial bus, whereas other actors rest on wire connections. For property checking a Hybrid Theatre model is reduced on to the Uppaal Statistical Model Checker which is then exploited for the assessment of functional and temporal behavior of the chosen model. The paper concludes by discussing problems about how a Hybrid Theatre model can be transitioned without distortions toward its synthesis, and by giving indications of further work.
Actors, Asynchronous Message Passing, Cyber-Physical Systems, Hybrid Automata, Statistical Model Checking, Timing Constraints, Controller Area Network.
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/289607
 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