We propose a hybrid process calculus for modelling and rea- soning on cyber-physical systems (CPSs). The dynamics of the calculus is expressed in terms of a labelled transition system in the SOS style of Plotkin. This is used to define a bisimulation-based behavioural semantics which allows us compositional reasonings. Finally, we prove run-time properties and system equalities for a non-trivial case study.

A Calculus of Cyber-Physical Systems

MERRO, Massimo
2017-01-01

Abstract

We propose a hybrid process calculus for modelling and rea- soning on cyber-physical systems (CPSs). The dynamics of the calculus is expressed in terms of a labelled transition system in the SOS style of Plotkin. This is used to define a bisimulation-based behavioural semantics which allows us compositional reasonings. Finally, we prove run-time properties and system equalities for a non-trivial case study.
2017
978-3-319-53732-0
Cyber-physical system, formal methods, semantics
File in questo prodotto:
File Dimensione Formato  
main-camera-ready.pdf

accesso aperto

Descrizione: Articolo definitivo.
Tipologia: Documento in Post-print
Licenza: Accesso ristretto
Dimensione 626.78 kB
Formato Adobe PDF
626.78 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/959378
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 26
  • ???jsp.display-item.citation.isi??? 17
social impact