Model Checking Actor-based Cyber-Physical Systems

Cyber-physical systems (CPSs) integrate continuous behavior of a physical controlled plant with discrete behavior provided by a controlling cyber (software) part. The integration is challenging because continuous, Newtonian time of the physical part needs be reconciled with discrete time of the cyber part. In this work, the event-based asynchronous actors of Theatre extended with continuous modes, are used for modelling and analyzing CPSs. Continuous modes capture the dynamic laws (ODEs) of variation of physical/environmental variables. Theatre is control-based and distributed. It is implemented in Java, which is used both as the modelling language and as the target implementation language. Specific control forms were developed for simulating a distributed CPS and for assessing its functional/temporal behavior. Continuous modes exploit suitable ODE solvers to predict the future values of selected variables at specific time points. Although classical actors depend on non-deterministic message passing, a Theatre model can be designed to have a deterministic behavior. A hybrid Theatre model can be analyzed by exhaustive model checking by having, for instance, that the computations of the ODE solvers are, preliminarily, offline collected and reused during verification. This paper describes Theatre, summarizes its operational semantics and illustrates a model reduction onto Uppaal timed automata. Then an automotive deterministic model based on both wired and Controller Area Network transmitted messages is presented and thoroughly analysed.