A Formal Framework for Distributed Cyber-Physical Systems

TL;DR

This paper introduces an algebraic framework for modeling and reasoning about the composition and decomposition of cyber-physical systems, enabling better system design and analysis.

Contribution

It extends an algebraic component model with division operators to facilitate reasoning about system invariants and updates in cyber-physical systems.

Findings

Framework applied to robot system on shared field

Division operator used to identify desirable system updates

Enhanced reasoning about system invariants and decomposition

Abstract

Composition is an important feature of a specification language, as it enables the design of a complex system in terms of a product of its parts. Decomposition is equally important in order to reason about structural properties of a system. Usually, however, a system can be decomposed in more than one way, each optimizing for a different set of criteria. We extend an algebraic component-based model for cyber-physical systems to reason about decomposition. In this model, components compose using a family of algebraic products, and decompose, under some conditions, given a corresponding family of division operators. We use division to specify invariant of a system of components, and to model desirable updates. We apply our framework to design a cyber-physical system consisting of robots moving on a shared field, and identify desirable updates using our division operator.