Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

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

    Second International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2008)

    Leeds, UK, 2 - 3 July 2008


    Siwar Khelifi, Hatem Hadj kacem and Ahmed Hadj Kacem


    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.


    PDF filePDF Version of this Paper (103kb)