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

David Garlan and Serge Khersonsky.


In Proceedings of the 10th International Workshop on Software Specification and Design (IWSSD-10), San Diego, CA, November 2000.

Online links: 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.  
@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}
}
    Created: 2006-08-22 13:44:05
Feedback: ABLE Webmaster
Last modified: Sat October 12 2019 16:15:32
        BibAdmin