Statistical Model Checking of Cyber-Physical Systems Using Hybrid Theatre

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 wired 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.