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

TL;DR

The paper addresses the fragility of centralized reconfiguration by introducing Concerto-D, a decentralized extension of the Concerto language. It provides a Maude-based formalization of Concerto-D's semantics, enabling executable models, interpreters, and model-checking capabilities for distributed CPS reconfiguration. Through a wildlife-monitoring CPS case study, it illustrates decentralized coordination, asynchronous inter-node communication, and local node autonomy. The work lays groundwork for formal verification and future enhancements, including partial-order reduction, symbolic model checking, and a choreography-based compilation from Concerto to Concerto-D.

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.

Figures (2)

• Figure 1: Full overview of the CPS use case with $2+n$ nodes hosting database, system, $n$listeners, and $n$sensors.
• Figure 2: Control components of listener$_\text{i}$ on $\mathit{node}_2$ and sensor$_\text{i}$ from $\mathit{node}_{2+i}$. State example when applying the reconfiguration plans of Listings \ref{['lst:nodeListeners']} and \ref{['lst:site:i']}.