A Petri-Net Model for the Publish-Subscribe Paradigm and Its Application for the Verification of the BonjourGrid Middleware
Leila Abidi, Christophe Cérin, Sami Évangelista · 2011
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.