Abstract: The backbone of most software architectures and component integration frameworks is one or more architectural styles that provide a domain-speci?c design vocabulary and a set of constraints on how that vocabulary is used. Today's architectural styles are increasingly complex, involving rich vocabularies and numerous constraints. Hence, designing a sound and appropriate style becomes an intellectually challenging activity. Unfortunately, although there are numerous tools to help in the analysis of architectures for individual systems, relatively less work has been done on tools to help in the design of architectural styles. In this paper we address this gap by showing how to map an architectural style, expressed formally in an architectural description language, into a relational model that can then be checked for properties, such as whether a style is consistent, whether a style satis?es some predicates over its architectural structure, and whether two styles are compatible for composition.

Abstract: The backbone of many architectures is an architectural style that provides a domain-specific design vocabulary and set of constraints on how that vocabulary can be used. Hence, designing a sound and appropriate architectural style becomes an important and intellectually challenging activity. Unfortunately, although there are numerous tools to help in the analysis of individual architectures, relatively less work has been done on tools to help the style designer. In this paper we show how to map an architectural style, expressed formally in an architectural description language, into a relational model that can be automatically checked for properties such as whether a style is consistent, whether a style satisfies some predicate over the architectural structure, whether two styles are compatible for composition, and whether one style refines another.

Abstract: While 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, in practice coming up with an appropriate state model for a pub-sub system can be a difficult and error-prone task. In this paper we address this problem by describing a generic pub-sub model checking framework. The key feature of this framework is a reusable, parameterized state machine model that captures pub-sub runtime event management and dispatch policy. 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.