An Approach to Model and Validate Publish/Subscribe Architectures
Luciano Baresi, Carlo Ghezzi, Luca Zanolin · Virtual Community of Pathological Anatomy (University of Castilla La Mancha) · 2003
Distributed applications are increasingly built as federations of components that join and leave the cooperation dynamically. Publish/subscribe middleware is a promising infrastructure to support these applications, but unfortunately complicates the understanding and 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 architectures. Since the complexity is mainly constrained in the middleware, we supply it as a predefined parametric component. Besides setting these parameters, the designer must provide the other components as UML statechart diagrams. The required global properties of the federation are then given in terms of live sequence charts (LSCs) and the validation of the whole system is achieved through model checking using SPIN. Instead of using the property language of SPIN (linear temporal logic), we render properties as automata; this allows us to represent more complex properties and conduct more thorough validation of our systems.