Towards fine-grained automated verification of Publish-Subscribe architectures

Abstract

The design and validation of distributed applications built on top of Publish-Subscribe infrastructures remain an open problem. Previous efforts adopted finite automata to specify the components' behavior, and model checking to verify global properties. However, existing proposals are far from being applicable in real contexts, as strong simplifications are needed on the underlying Publish-Subscribe infrastructure to make automatic verification feasible. To face this challenge, we propose a novel approach that embeds the asynchronous communication mechanisms of Publish-Subscribe infrastructures within the model checker. This way, Publish-Subscribe primitives become available to the specification of application components as additional, domain-specific, constructs of the modeling language. With this approach, one can develop a finegrained model of the Publish-Subscribe infrastructure without incurring in state space explosion problems, thus enabling the automated verification of application components on top of realistic communication infrastructures. © IFIP International Federation for Information Processing 2006.