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 (automotive, avionics, energy supply, etc), their verification often relies on simulation test systems rather then formal methodologies. This is because there is still a lack of research on the modelling and the definition of formal semantics to compare non-trivial CPSs in terms of their runtime behaviours up to an acceptable tolerance. 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

Massimo Merro
;
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 (automotive, avionics, energy supply, etc), their verification often relies on simulation test systems rather then formal methodologies. This is because there is still a lack of research on the modelling and the definition of formal semantics to compare non-trivial CPSs in terms of their runtime behaviours up to an acceptable tolerance. 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
File in questo prodotto:
File Dimensione Formato  
mainIC.pdf

accesso aperto

Descrizione: Articolo principale.
Tipologia: Documento in Post-print
Licenza: Creative commons
Dimensione 591.94 kB
Formato Adobe PDF
591.94 kB Adobe PDF Visualizza/Apri

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/11562/983257
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 24
  • ???jsp.display-item.citation.isi??? 10
social impact