Modelling and Analysis of Cyber-Physical Systems using Deterministic Theatre

This paper proposes an original variant of the Theatre actor system which is best suited to modelling analysis and implementation of cyber-physical systems (CPS). Novel in the proposal is the use of deterministic timed actors. More in particular, Deterministic Theatre is proposed which, although based on asynchronous message passing, adopts a deterministic precedence constraint technique which regulates the delivery order of simultaneous messages. Such provision proves effective for correctness analysis of CPS models through exhaustive model checking, and for transforming an analyzed model into a compliant implementation. The constrained delivery order improves the model checking performance by reducing the partial order otherwise existing in the timed transition system of the model. The paper introduces Deterministic Theatre and shows its concrete support on top of the Uppaal timed automata language and toolbox. A CPS modelling case study concerning a train-door controller is presented, which is used as a running analysis example throughout the paper. Finally, conclusions are drawn with an indication of ongoing and future work concerning Deterministic Theatre.