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.

Modelling and Analysis of Cyber-Physical Systems using Deterministic Theatre

Libero Nigro
Membro del Collaboration Group
2020

Abstract

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.
modelling and analysis, cyber-physical systems, deterministic timed actors, timing constraints, model checking, Uppaal
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: http://hdl.handle.net/20.500.11770/305257
 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