Engineering MDA into Compositional Reasoning for Analyzing Middleware-Based Applications
Behavioral analysis of middleware-based applications typically requires the analysis of the middleware and the application, in a monolithic 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 verification approach which decomposes the system in accordance with its Software Architecture. The architectural decomposability theorem we defined in previous work decomposes the system into three logical layer: (i) application components, (ii) proxies and, (iii) middleware. This logical separation allows for reducing the global system validation to the verification of local behaviors.
In this paper, we engineer the architectural decomposability theorem to the analysis of middleware-based applications by automatically generating 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 State Machine formalism, we describe a set of transformation rules that allow for deriving correct proxies for using CORBA. By means of the proposed transformations, the correctness of the proxy behavioral models is guaranteed without the need to validate them with respect to the assumptions posed by the theorem.
KeywordsModel Check Linear Temporal Logic Common Object Request Broker Architecture Model Drive Architecture Transaction Manager
Unable to display preview. Download preview PDF.
- 3.Bradbury, J., Dingel, J.: Evaluating and Improving the Automatic Analysis of Implicit Invocation Systems. In: European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2003), Helsinki, Finland. ACM Press, New York (2003)Google Scholar
- 6.Long, D.: Model Checking, Abstraction and Compositional Reasoning. PhD thesis, Carnegie Mellon University (1993)Google Scholar
- 7.Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2001)Google Scholar
- 8.Caporuscio, M., Inverardi, P., Pelliccione, P.: Compositional verification of middleware-based software architecture descriptions. In: Proceedings of the International Conference on Software Engineering (ICSE 2004), Edinburgh (2004)Google Scholar
- 9.Perry, D.E., Wolf, A.L.: Foundations for the study of software architecture. SIGSOFT Software Engineering Notes 17, 40–52 (1992)Google Scholar
- 10.Object Management Group (OMG): OMG/Model Driven Architecture - A Technical Perspective OMG Document: ormsc/01-07-01 (2001)Google Scholar
- 12.Object Management Group: (Common Object Request Broker Architecture (CORBA/IIOP), v3.0.3) OMG document formal/04-03-01Google Scholar
- 13.Object Management Group: MOF 2.0 Query/View/Transformation RFP OMG document ad/02-04-10 (2002)Google Scholar
- 14.Börger, E.: The origins and the development of the asm method for high level system design and analysis. Journal of Universal Computer Science 8, 2–74 (2002)Google Scholar
- 16.ITU-T Recommendation Z.120.: Message Sequence Charts (ITU Telecommunication Standardisation Sector)Google Scholar
- 17.Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems. Springer-Verlag New York, Inc., Heidelberg (1992)Google Scholar
- 19.Caporuscio, M., Di Ruscio, D., Inverardi, P., Pelliccione, P., Pierantonio, A.: Tranformation rules (2004), Available at http://www.di.univaq.it/diruscio