An Overview of the Decentralized Reconfiguration Language Concerto-D through its Maude Formalization

TL;DR

This paper presents a formal Maude-based semantics for Concerto-D, a decentralized reconfiguration language designed for edge computing and cyber-physical systems, ensuring reliable and executable reconfiguration plans.

Contribution

It introduces Concerto-D, an extension of Concerto with decentralized coordination and formal semantics, validated through a real-world CPS case study.

Findings

Decentralized coordination avoids single points of failure.

Maude formalization guarantees executability of reconfiguration plans.

Application to a real CPS demonstrates practical relevance.

Abstract

We propose an overview of the decentralized reconfiguration language Concerto-D through its Maude formalization. Concerto-D extends the already published Concerto language. Concerto-D improves on two different parameters compared with related work: the decentralized coordination of numerous local reconfiguration plans which avoid a single point of failure when considering unstable networks such as edge computing, or cyber-physical systems (CPS) for instance; and a mechanized formal semantics of the language with Maude which offers guarantees on the executability of the semantics. Throughout the paper, the Concerto-D language and its semantics are exemplified with a reconfiguration extracted from a real case study on a CPS. We rely on the Maude formal specification language, which is based on rewriting logic, and consequently perfectly suited for describing a concurrent model.