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.

翻译：本文通过Maude形式化方法对去中心化重配置语言Concerto-D进行系统性综述。Concerto-D是对已发表的Concerto语言的扩展。相较于现有研究，该语言在两方面实现改进：其一，通过分布式协调多个局部重配置方案，避免边缘计算或信息物理系统（CPS）等不稳定网络环境中的单点故障；其二，基于Maude构建机械化形式语义，为语义可执行性提供理论保证。本文通过从实际CPS案例中提取的重配置实例，具体阐释Concerto-D语言及其语义特性。研究采用基于重写逻辑的Maude形式化规约语言，该语言天然适用于描述并发模型。