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.
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo
|Titolo:||Statistical Model Checking of Cyber-Physical Systems using Hybrid Theatre|
NIGRO, Libero [Membro del Collaboration Group] (Corresponding)
SCIAMMARELLA, PAOLO FRANCESCO [Membro del Collaboration Group]
|Data di pubblicazione:||2019|
|Appare nelle tipologie:||4.1 Contributo in Atti di convegno|