A formal framework for distributed cyber-physical systems

Journal of Logical and Algebraic Methods in Programming, vol. 128, pp. 100795

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.

Authors 3

1. Benjamin Lion corresponding Aachen

   Leiden University

   Affiliation as printed

   Leiden University, Leiden, the Netherlands

2. Farhad Arbab Aachen

   Leiden University · Centrum Wiskunde & Informatica

   Affiliation as printed

   CWI, Amsterdam, the Netherlands

   Leiden University, Leiden, the Netherlands

3. Carolyn Talcott

   SRI International

   Affiliation as printed

   SRI International, CA, USA