CINECA IRIS Institutional Research Information System
IRIS è la soluzione IT che facilita la raccolta e la gestione dei dati relativi alle attività e ai prodotti della ricerca. Fornisce a ricercatori, amministratori e valutatori gli strumenti per monitorare i risultati della ricerca, aumentarne la visibilità e allocare in modo efficace le risorse disponibili.
EnglishThis 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.
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo
| Titolo: | Modelling and Analysis of Cyber-Physical Systems using Deterministic Theatre | |
| Autori: | ||
| Data di pubblicazione: | 2020 | |
| Handle: | http://hdl.handle.net/20.500.11770/305257 | |
| Appare nelle tipologie: | 4.1 Contributo in Atti di convegno |
File in questo prodotto:
Copyright © 2021