A Petri-Net Model for the Publish-Subscribe Paradigm and Its Application for the Verification of the BonjourGrid Middleware
2013 IEEE International Conference on Services Computing (2011)
Washington, DC USA
July 4, 2011 to July 9, 2011
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SCC.2011.42
In this article we focus on the modelization of the Bonjour Grid protocol which is based on the Publish-Subscribe (Pub-Sub) paradigm, a paradigm for asynchronous communication that is useful for implementing some approaches in distributed programming. The aim of this paper is to isolate the generic mechanisms of construction for the publish-subscribe approach then to model and verify, based on those mechanisms, the Bonjour Grid protocol that allows the coordination of multiple instances of desktop grid middleware. We produce models using colored Petri nets in order to describe a specific modeling approach for the Pub-Sub paradigm. Such models are important, first, to formally verify the adequacy of Bonjour Grid in the coordination of resources in desktop grids - for example by proving the absence of a deadlock in the Bonjour Grid protocol, and second, to offer a 'composition'mechanism for integrating any protocol based on the Pub-Sub paradigm. These ideas are illustrated along the Bonjour Gridcase study and they constitute a methodology of building Pub-Sub systems.
Principles of services, Service models, Grid Computing Middleware, Publish-Subscribe paradigm, BonjourGrid, Formal Models, Colored Petri Nets
Sami Evangelista, Christophe Cérin, Leila Abidi, "A Petri-Net Model for the Publish-Subscribe Paradigm and Its Application for the Verification of the BonjourGrid Middleware", 2013 IEEE International Conference on Services Computing, vol. 00, no. , pp. 496-503, 2011, doi:10.1109/SCC.2011.42