Engineering MDA into Compositional Reasoning for Analyzing Middleware-Based Applications

  • Mauro Caporuscio
  • Davide Di Ruscio
  • Paola Inverardi
  • Patrizio Pelliccione
  • Alfonso Pierantonio
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3527)


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.


Model Check Linear Temporal Logic Common Object Request Broker Architecture Model Drive Architecture Transaction Manager 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Emmerich, W.: Software engineering and middleware: a roadmap. In: Proceedings of the conference on The future of Software engineering (ICSE 2000) - Future of SE Track, Limerick, Ireland, pp. 117–129. ACM Press, New York (2000)CrossRefGoogle Scholar
  2. 2.
    Garlan, D., Khersonsky, S., Kim, J.S.: Model Checking Publish/Subscribe Systems. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 166–180. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  3. 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
  4. 4.
    Kaveh, N., Emmerich, W.: Validating distributed object and component designs. In: Bernardo, M., Inverardi, P. (eds.) SFM 2003. LNCS, vol. 2804, pp. 63–91. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  5. 5.
    Grumberg, O., Long, D.E.: Model Checking and Modular Verification. ACM Transaction on Programming Languages and Systems 16, 846–872 (1994)CrossRefGoogle Scholar
  6. 6.
    Long, D.: Model Checking, Abstraction and Compositional Reasoning. PhD thesis, Carnegie Mellon University (1993)Google Scholar
  7. 7.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2001)Google Scholar
  8. 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. 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. 10.
    Object Management Group (OMG): OMG/Model Driven Architecture - A Technical Perspective OMG Document: ormsc/01-07-01 (2001)Google Scholar
  11. 11.
    Börger, E., Stärk, R.: Abstract State Machines - A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)zbMATHGoogle Scholar
  12. 12.
    Object Management Group: (Common Object Request Broker Architecture (CORBA/IIOP), v3.0.3) OMG document formal/04-03-01Google Scholar
  13. 13.
    Object Management Group: MOF 2.0 Query/View/Transformation RFP OMG document ad/02-04-10 (2002)Google Scholar
  14. 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
  15. 15.
    Börger, E.: High level system design and analysis using abstract state machines. In: Hutter, D., Traverso, P. (eds.) FM-Trends 1998. LNCS, vol. 1641, pp. 1–43. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  16. 16.
    ITU-T Recommendation Z.120.: Message Sequence Charts (ITU Telecommunication Standardisation Sector)Google Scholar
  17. 17.
    Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems. Springer-Verlag New York, Inc., Heidelberg (1992)Google Scholar
  18. 18.
    Anlauff, M.: XASM – An Extensible, Component-Based Abstract State Machines Language. In: Gurevich, Y., Kutter, P.W., Odersky, M., Thiele, L. (eds.) ASM 2000. LNCS, vol. 1912, pp. 69–90. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  19. 19.
    Caporuscio, M., Di Ruscio, D., Inverardi, P., Pelliccione, P., Pierantonio, A.: Tranformation rules (2004), Available at

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Mauro Caporuscio
    • 1
  • Davide Di Ruscio
    • 1
  • Paola Inverardi
    • 1
  • Patrizio Pelliccione
    • 1
  • Alfonso Pierantonio
    • 1
  1. 1.Dipartimento di InformaticaUniversità degli Studi di L’AquilaL’AquilaItaly

Personalised recommendations