Formal analysis of architectural patterns

Architectural patterns characterize and specify structural and behavioral properties of (sub)systems, thus allowing the provision of solutions for classes of problems. In this paper we show the use of architectural patterns as an abstraction to carry on, and reuse, formal reasoning on systems whose configuration can dynamically change. This kind of systems is hard to model and to reason about due to the fact that we cannot simply build a model with fixed topology (i.e. fixed number of components and connectors) and validate properties of interest on it. The work presented in this paper proposes an approach that given an architectural pattern which expresses a class of systems configurations and a set of properties of interest (i) selects, if any, a minimal configuration for which the specified properties make sense, (ii) an abstraction of the chosen architectural model erformed, in order to reduce the complexity of the verification phase. In this stage, abstractions are driven by the properties of interest. The output of this abstraction step can be model-checked, tested and analyzed by using a standard model-checking framework. (iii) The verification results obtained in the previous step are lifted to generic configurations by performing manual reasoning driven by the constraints posed by the architectural pattern. The approach will be applied by using an event-based architectural pattern to a publish/subscribe system, the SIENA middleware, in order to validate its features and its mobility extension.