Model Checking Implicit-Invocation Systems

David Garlan, and Serge Khersonsky

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

Implicit invocation, Publish-subscribe, Model checking

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

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