Runtime Composition Of Systems of Interacting Cyber-Physical Components

TL;DR

This paper presents a transition system framework for cyber-physical systems that supports compositional specification and implementation, demonstrated through a case study using Maude rewriting logic.

Contribution

It introduces a compositional transition system algebra for cyber-physical systems with conditions for correct product execution, implemented in Maude.

Findings

Successful compositional specification in a case study

Conditions for correct lazy expansion of system products

Implementation of the algebra in Maude rewriting logic

Abstract

We introduce a transition system based specification of cyber-physical systems whose semantics is compositional with respect to a family of algebraic products. We give sufficient conditions for execution of a product to be correctly implemented by a lazy expansion of the product construction. The transition system algebra is implemented in the Maude rewriting logic system, and we report a simple case study illustrating compositional specification.