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.
|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.|
|Implicit invocation, Publish-subscribe, Model checking|
Last modified: 2/10/2003. For comments and problems, contact firstname.lastname@example.org.