Model checking publishsubscribe systems

Abstract. While publish-subscribe systems have good engineering prop-erties, they are difficult to reason about and to test. Model checking such systems is an attractive alternative. However, in practice coming up with an appropriate state model for a pub-sub system can be a dif-ficult and error-prone task. In this paper we address this problem by describing a generic pub-sub model checking framework. The key fea-ture of this framework is a reusable, parameterized state machine model that captures pub-sub run-time event management and dispatch pol-icy. Generation of models for specific pub-sub systems is then handled by a translation tool that accepts as input a set of pub-sub component descriptions together with a set of pub-sub properties, and maps them into the framework where they can be checked using off-the-shelf model checking tools.