@InProceedings{Kim2003,
      AUTHOR = {Garlan, David and Khersonsky, Serge and Kim, Jung Soo},
      TITLE = {Model Checking Publish-Subscribe Systems},
      YEAR = {2003},
      MONTH = {May},
      BOOKTITLE = {Proceedings of The 10th International SPIN Workshop on Model Checking of Software (SPIN 03)},
      ADDRESS = {Portland, OR},
      PDF = {http://www.cs.cmu.edu/afs/cs/project/able/ftp/SPIN03/SPIN03.pdf},
      ABSTRACT = {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}
}