Loupe: Verifying Publish-Subscribe Architectures with a Magnifying Lens

Abstract— The Publish-Subscribe (P/S) communication paradigm fosters high decoupling among distributed components. This facilitates the design of dynamic applications, but also impacts negatively on their verification, making it difficult to reason on the overall federation of components. In addition, existing P/S infrastructures offer radically different features to the applications, e.g., in terms of message reliability. This further complicates the verification, as its outcome depends on the specific guarantees provided by the underlying P/S system. Although model checking has been proposed as a tool for the verification of P/S architectures, existing solutions overlook many characteristics of the underlying communication infrastructure to avoid state explosion problems. To overcome these limitations, the Loupe domain-specific model checker adopts a different approach. The P/S infrastructure is not modeled on top of a general-purpose model checker. Instead, it is embedded wi...

• Type: Journal
• Year: 2011
• Where: TSE
• Authors: Luciano Baresi, Carlo Ghezzi, Luca Mottola
• Keywords: Loupe, Model Checker, State Explosion Problems, TSE 2011