Local Reasoning and Attribute-Based Memory Updates for Enforcing Global Invariants in Collective Adaptive Systems

We address the problem of enforcing global invariants, i.e., system-level properties, in Collective Adaptive Systems, such as distributed and decentralized Internet of Things (IoT) solutions. In particular, we propose a novel approach adopting Attribute-based memory Updates (AbU), a calculus modeling declarative, event-driven systems with attribute-based communication. Our methodology leverages a combination of precise node-level scheduling and local reasoning, with local invariants derived from the system-level property to guarantee. This distributed and decentralized approach promotes efficient enforcing while ensuring desired system-wide behavior, without the need for a central controlling authority.