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.

Abstract: An increasingly essential aspect of many critical software systems is the ability to quickly diagnose and locate faults so that appropriate corrective measures can be taken. Large, complex software systems fail unpredictably and pinpointing the source of the failure is a challenging task. In this paper we explore how our recently developed technique for automatic diagnosis performs in the automatic detection of failures and fault localization in a critical manufacturing control system of Samsung Electronics, where failures can result in large financial and schedule losses. We show how our approach can scale to such systems to diagnose intermittent faults, connectivity problems, protocol violations, and timing failures. We propose a set of measures of accuracy and performance that can be used to evaluate run-time diagnosis. We present lessons learned from this work including how instrumentation limitations may impair diagnosis accuracy: without overcoming these, there is a limit to the kinds of faults that can be detected.