-
A Formal Framework for Distributed Cyber-Physical Systems
Authors:
Benjamin Lion,
Farhad Arbab,
Carolyn Talcott
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 mode…
▽ More
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.
△ Less
Submitted 3 July, 2022;
originally announced July 2022.
-
A Rewriting Framework for Interacting Cyber-Physical Agents
Authors:
Benjamin Lion,
Farhad Arbab,
Carolyn Talcott
Abstract:
The analysis of cyber-physical systems (CPS) is challenging due to the large state space and the continuous changes occurring in their constituent parts. Design practices favor modularity to help reducing this complexity. In a previous work, we proposed a discrete semantic model for CPS that captures both cyber and physical aspects as streams of discrete observations, which ultimately form the beh…
▽ More
The analysis of cyber-physical systems (CPS) is challenging due to the large state space and the continuous changes occurring in their constituent parts. Design practices favor modularity to help reducing this complexity. In a previous work, we proposed a discrete semantic model for CPS that captures both cyber and physical aspects as streams of discrete observations, which ultimately form the behavior of a component. This semantic model is denotational and compositional, where each composition operator algebraically models an interaction between a pair of components. In this paper, we propose a specification of components as rewrite systems. The specification is operational and executable, and we study conditions for its semantics as components to be compositional. We demonstrate our framework by modeling a coordination of robots moving on a shared field. We show that our system of robots can be coordinated by a protocol in order to exhibit a desired emerging behavior. We use an implementation of our framework in Maude to give practical results.
△ Less
Submitted 2 August, 2022; v1 submitted 8 June, 2022;
originally announced June 2022.
-
Runtime Composition Of Systems of Interacting Cyber-Physical Components
Authors:
Benjamin Lion,
Farhad Arbab,
Carolyn Talcott
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 c…
▽ More
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.
△ Less
Submitted 25 May, 2022;
originally announced May 2022.
-
A Semantic Model for Interacting Cyber-Physical Systems
Authors:
Benjamin Lion,
Farhad Arbab,
Carolyn Talcott
Abstract:
We propose a component-based semantic model for Cyber-Physical Systems (CPSs) wherein the notion of a component abstracts the internal details of both cyber and physical processes, to expose a uniform semantic model of their externally observable behaviors expressed as sets of sequences of observations. We introduce algebraic operations on such sequences to model different kinds of component compo…
▽ More
We propose a component-based semantic model for Cyber-Physical Systems (CPSs) wherein the notion of a component abstracts the internal details of both cyber and physical processes, to expose a uniform semantic model of their externally observable behaviors expressed as sets of sequences of observations. We introduce algebraic operations on such sequences to model different kinds of component composition. These composition operators yield the externally observable behavior of their resulting composite components through specifications of interactions of the behaviors of their constituent components, as they, e.g., synchronize with or mutually exclude each other's alternative behaviors. Our framework is expressive enough to allow articulation of properties that coordinate desired interactions among composed components within the framework, also as component behavior. We demonstrate the usefulness of our formalism through examples of coordination properties in a CPS consisting of two robots interacting through shared physical resources.
△ Less
Submitted 1 October, 2021;
originally announced October 2021.
