Specification and verification of the structural and behavioral properties of Publish/Subscribe architectures

Distributed applications are dynamically built as federations of components that join and leave the cooperation. Publish/Subscribe paradigm is a promising infrastructure to support these applications. However this paradigm complicates the intuitive interpretation and subsequent validation of these systems. It is easy to understand what each component does, but it is hard to understand what the global federation achieves. In this paper, we describe an approach to support the modeling and validation of Publish/Subscribe architecture style. We integrate a functional and a structural approach based on automata with multiplicities. The aim is to express dynamism while offering a simple modeling which can be easy to understand. To ensure that the system is evolving correctly, we validate the whole system through model checking using SPIN which permits to specify some properties concerning the dynamic behavior of a system.