Int. J. of Information Technology, Communications and Convergence   »   2012 Vol.2, No.3

 

 

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

 

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

 

Available online: 14 Nov 2012

 

 

Editors Full text accessAccess for SubscribersPurchase this articleComment on this article