Home   Research Publications Members Related Software
IndexBrowse   BibliographiesMy selection
 Search: in   (word length ≥ 3)
Publication no #74   Download bibtex file Type :   Html | Bib | Both
Add to my selection
Model Checking Publish-Subscribe Systems

David Garlan, Serge Khersonsky and Jung Soo Kim.

In Proceedings of The 10th International SPIN Workshop on Model Checking of Software (SPIN 03), Portland, OR, May 2003.

Online links: PDF   Bibtex entry   Plain Text

While publish-subscribe systems have good engineering properties, they are difficult to reason about and to test. Model checking such systems is an attractive alternative. However, in practice coming up with an appropriate state model for a pub-sub system can be a difficult and error-prone task. In this paper we address this problem by describing a generic pub-sub model checking framework. The key feature of this framework is a reusable, parameterized state machine model that captures pub-sub runtime event management and dispatch policy. Generation of models for specific pub-sub systems is then handled by a translation tool that accepts as input a set of pub-sub component descriptions together with a set of pub-sub properties, and maps them into the framework where they can be checked using off-the-shelf model checking tools.

Keywords: Model Checking, Publish Subscribe Systems.  
    Created: 2006-08-21 17:24:28
Feedback: ABLE Webmaster
Last modified: Mon February 12 2018 11:21:51