A Calculus of Cyber-Physical Systems
Ruggero Lanotte, Massimo Merro
TL;DR
This paper introduces a hybrid process calculus tailored for cyber-physical systems, enabling formal modeling, reasoning, and verification of their behaviors through bisimulation semantics and compositional analysis.
Contribution
It presents a novel calculus for CPS that combines process algebra with physical dynamics, supporting formal verification and reasoning.
Findings
Defined a labelled transition system for the calculus
Proved run-time properties for CPS models
Validated the approach with a non-trivial case study
Abstract
We propose a hybrid process calculus for modelling and reasoning on cyber-physical systems (CPS{s}). 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 support compositional reasonings. Finally, we prove run-time properties and system equalities for a non-trivial case study.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Petri Nets in System Modeling · Embedded Systems Design Techniques