Title: A formal approach to model and verify the behaviour of publish/subscribe architectural style

Authors: Hatem Hadj Kacem; Imen Loulou; Ahmed Hadj Kacem

Addresses: ReDCAD Research Unit, FSEG, University of Sfax, B.P. 1088, 3018 Sfax, Tunisia. ' ReDCAD Research Unit, FSEG, University of Sfax, B.P. 1088, 3018 Sfax, Tunisia. ' ReDCAD Research Unit, FSEG, University of Sfax, B.P. 1088, 3018 Sfax, Tunisia

Abstract: Publish/subscribe system is now largely acknowledged as one of the most interesting paradigms for distributed interactions. Its main purpose is the dissemination of published events to concerned entities. This dissemination must be achieved by taking into account structural and behavioural constraints. In this paper, we extend P/S-CoM, as a formal approach supporting the correct modelling of publish/subscribe architectural style with respect to structural properties. We consider the behavioural properties, which are related to event dissemination and have to be respected during the lifetime system. Published events have to be spread to concerned entities explicitly with neither duplication nor loss and with respect to their publication order. We propose using the automata with multiplicities (or weighted automata) as a formalism for specification. This tool will be used here to ensure that the system is correctly evolving with respect to its architectural style. A tool is developed to support the proposed approach.

Keywords: correctness; publish-subscribe; Pub/Sub; architectural style; behavioural properties; SPIN; weighted automata; communication modelling; event-based communication; distributed interactions.

DOI: 10.1504/IJITCC.2012.050412

International Journal of Information Technology, Communications and Convergence, 2012 Vol.2 No.3, pp.234 - 252

Published online: 16 Aug 2014 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article