Model Checking Implicit-Invocation Systems

David Garlan, and Serge Khersonsky

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

Online links: Postscript PDF BIBTEX Citation

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 al-ternative. However, it is not clear what kinds of state models are best suited for this. In this paper we propose a struc-tural approach, which factors the model checking problem into two parts: behavior specific to a particular implicit in-vocation system, and reusable run-time infrastructure that handles event-based communication and delivery policies. The reusable portion is itself structured so that alternative run-time mechanisms may be experimented with.

Keywords

Implicit invocation, publish-subscribe, model checking, software architecture

For further information, please visit the home pages of the ABLE research project and Carnegie Mellon University's Composable Systems Group.

Last modified: 10/15/2001. For comments and problems, contact able-help@cs.cmu.edu.