Cyber-Physical Systems (CPSs) are integrations of networking and distributed computing systems with physical processes, where feedback loops allow physical processes to affect computations and vice versa. Although CPSs can be found in several real-world domains, their verification often relies on simulation test systems rather than formal methodologies. We propose a hybrid probabilistic process calculus for modelling and reasoning on CPSs. The dynamics of the calculus is expressed in terms of a probabilistic labelled transition system in the SOS style of Plotkin. This is used to define a bisimulation-based probabilistic behavioural semantics which supports compositional reasonings. For a more careful comparison between CPSs, we provide two compositional probabilistic metrics to formalise the notion of behavioural distance between systems, also in the case of bounded computations. Finally, we provide a non-trivial case study, taken from an engineering application, and use it to illustrate our definitions and our compositional behavioural theory for CPSs.

A Probabilistic Calculus of Cyber-Physical Systems

Lanotte, Ruggero;Tini ,Simone
2021-01-01

Abstract

Cyber-Physical Systems (CPSs) are integrations of networking and distributed computing systems with physical processes, where feedback loops allow physical processes to affect computations and vice versa. Although CPSs can be found in several real-world domains, their verification often relies on simulation test systems rather than formal methodologies. We propose a hybrid probabilistic process calculus for modelling and reasoning on CPSs. The dynamics of the calculus is expressed in terms of a probabilistic labelled transition system in the SOS style of Plotkin. This is used to define a bisimulation-based probabilistic behavioural semantics which supports compositional reasonings. For a more careful comparison between CPSs, we provide two compositional probabilistic metrics to formalise the notion of behavioural distance between systems, also in the case of bounded computations. Finally, we provide a non-trivial case study, taken from an engineering application, and use it to illustrate our definitions and our compositional behavioural theory for CPSs.
2021
Cyber-physical system; Hybrid probabilistic process calculus; Probabilistic metric semantics
Lanotte, Ruggero; Merro, Massimo; Tini, Simone
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: https://hdl.handle.net/11383/2073449
 Attenzione

L'Ateneo sottopone a validazione solo i file PDF allegati

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 26
  • ???jsp.display-item.citation.isi??? 10
social impact