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.
|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.|
|Implicit invocation, publish-subscribe, model checking, software architecture|
Last modified: 10/15/2001. For comments and problems, contact firstname.lastname@example.org.