IoT and smart systems frequently rely on publish-subscribe (pub/sub) middlewares like MQTT or DDS. However, current coordination solutions often lack formal rigour, posing risks in mission-critical applications, or suffer from excessive complexity, hindering practical deployment and increasing the likelihood of errors. This paper addresses these challenges by integrating AbU, a recently introduced formal model based on Event-Condition-Action (ECA) rules and attribute-based communication, with standard pub/sub middlewares. We present a synchronization protocol that leverages pub/sub primitives to implement AbU’s transactional communication semantics. We prove the correctness of this protocol, demonstrating that it accurately reflects the underlying system dynamics. This integration of a formal ECA-based programming model with pub/sub offers a compelling balance between rigorous guarantees and practical applicability for coordinating IoT and smart systems.
