Engineering MDA into Compositional Reasoning for Analyzing Middleware-based Applications

Abstract. Behavioral analysis of middleware-based applications typi-cally requires to analyze the middleware and the application, in a mono-lithic way. In terms of model-checking, this is a complex task and may result in the well known \state-explosion " problem. These considerations led us to investigate a compositional verication approach which decom-poses the system in according to its Software Architecture. The architec-tural decomposability theorem we dened in previous work decomposes the system into three logical layer: (i) application components, (ii) prox-ies and, (iii) middleware. This logical separation allows for reducing the global system validation to local behaviors verication. In this paper, we engineer the architectural decomposability theorem to the analysis of middleware-based applications by automatically generat-ing the proxies needed by the components in order to properly interact with each other via the middleware. In particular, following the Model Driven Architecture approach and by making use of the Abstract Stat