@InProceedings{Garlan2000,
      AUTHOR = {Garlan, David and Khersonsky, Serge},
      TITLE = {Model Checking Implicit-Invocation Systems},
      YEAR = {2000},
      MONTH = {November},
      BOOKTITLE = {Proceedings of the 10th International Workshop on Software Specification and Design (IWSSD-10)},
      ADDRESS = {San Diego, CA},
      PDF = {http://www.cs.cmu.edu/afs/cs/project/able/ftp/iwssd10/iwssd10.pdf},
      ABSTRACT = {While implicit invocation (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, it is not clear what kinds of state models are best suited for this. In this paper we propose a structural approach, which factors the model checking problem into two parts: behavior specific to a particular implicit invocation system, and reusable runtime infrastructure that handles event-based communication and delivery policies. The reusable portion is itself structured so that alternative runtime mechanisms may be experimented with. },
      KEYWORDS = {Model Checking, Publish Subscribe Systems}
}