HpC: A Calculus for Hybrid and Mobile Systems -- Full Version

TL;DR

This paper introduces HpC, a formal calculus extending the pi-calculus to model and analyze hybrid, mobile, and physical systems like IoT infrastructures, ensuring correctness in dynamic environments.

Contribution

It presents a minimal extension of the pi-calculus, called HpC, that captures mobility, time, and physics, enabling formal reasoning about hybrid and mobile systems.

Findings

HpC effectively models a realistic handover protocol.

The extension preserves key theoretical properties like bisimulation.

It provides a formal foundation for analyzing IoT and cyber-physical systems.

Abstract

Networked cybernetic and physical systems of the Internet of Things (IoT) immerse civilian and industrial infrastructures into an interconnected and dynamic web of hybrid and mobile devices. The key feature of such systems is the hybrid and tight coupling of mobile and pervasive discrete communications in a continuously evolving environment (discrete computations with predominant continuous dynamics). In the aim of ensuring the correctness and reliability of such heterogeneous infrastructures, we introduce the hybrid {\pi}-calculus (HpC), to formally capture both mobility, pervasiveness and hybridisation in infrastructures where the network topology and its communicating entities evolve continuously in the physical world. The {\pi}-calculus proposed by Robin Milner et al. is a process calculus that can model mobile communications and computations in a very elegant manner. The HpC we propose is a conservative extension of the classical {\pi}-calculus, i.e., the extension is ``minimal'', and yet describes mobility, time and physics of systems, while allowing to lift all theoretical results (e.g. bisimulation) to the context of that extension. We showcase the HpC by considering a realistic handover protocol among mobile devices.