Architectural Verification of Black-Box Component-Based Systems

  • Antonia Bertolino
  • Henry Muccini
  • Andrea Polini
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4401)


We introduce an original approach, which combines monitoring and model checking techniques into a comprehensive methodology for the architectural verification of Component-based systems. The approach works by first capturing the traces of execution via the instrumented middleware; then, the observed traces are reverse engineered into Message Sequence Charts, which are then checked for compliance to the Component-based Software Architecture, using a model checker. The methodology has been conceived for being applied indifferently for validating the system in house before deployment and for continuous validation in the field following evolution. A case study for the first case is here illustrated.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    An Approach for Tracing and Understanding Asynchronous Systems. ISR Tech. Report UCI-ISR-02-7 (2002)Google Scholar
  2. 2.
    CHARMY Project. Charmy Web Site (2004),
  3. 3.
    Fujaba Project. U.Paderborn, Sw Eng. Group (2005),
  4. 4.
    Rapid System Development via Product Line Architecture Implementation, Heraklion Crete, Greece, LNCS (September 2005)Google Scholar
  5. 5.
    Allen, R., Garlan, D.: A Formal Basis for Architectural Connection. ACM Trans. on Software Engineering and Methodology 6(3), 213–249 (1997)CrossRefGoogle Scholar
  6. 6.
    Bernardo, M., Donatiello, L., Ciancarini, P.: Performance Evaluation of Complex Systems: Techniques and Tools. In: Calzarossa, M.C., Tucci, S. (eds.) Performance 2002. LNCS, vol. 2459, pp. 236–260. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  7. 7.
    Bucchiarone, A., et al.: Model-Checking plus Testing: from Software Architecture Analysis to Code Testing. In: Núñez, M., et al. (eds.) FORTE 2004. LNCS, vol. 3236, pp. 351–365. Springer, Heidelberg (2004)Google Scholar
  8. 8.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking, 2nd edn. MIT Press, Cambridge (2000)Google Scholar
  9. 9.
    Crnkovic, I., Larsson, M. (eds.): Building Reliable Component-based Software Systems. Artech House (July 2002)Google Scholar
  10. 10.
    Elbaum, S., Diep, M.: Profiling Deployed Software: Assessing Strategies and Testing Opportunities. IEEE Trans. on Software Engineering 31(8), 1–16 (2005)CrossRefGoogle Scholar
  11. 11.
    Garlan, D.: Software Architecture: a Roadmap. In: ACM ICSE 2000, The Future of Software Engineering, pp. 91–101. ACM Press, New York (2000)CrossRefGoogle Scholar
  12. 12.
    Garlan, D.: Formal Modeling and Analysis of Software Architecture: Components, Connectors, and Events. In: Bernardo, M., Inverardi, P. (eds.) SFM 2003. LNCS, vol. 2804, pp. 1–24. Springer, Heidelberg (2003)Google Scholar
  13. 13.
    Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (Sept. 2003)Google Scholar
  14. 14.
    Inverardi, P., Muccini, H., Pelliccione, P.: CHARMY: An Extensible Tool for Architectural Analysis. In: ACM Proc. European Software Engineering Conference/the Foundations of Software Engineering (ESEC/FSE), September 2005, ACM Press, New York (2005)Google Scholar
  15. 15.
    Kiviluoma, K., Koskinen, J., Mikkonen, T.: Run-time monitoring of architecturally significant behaviors using behavioral profiles and aspects. In: Proceedings of the International Symposium on Software Testing and Analysis (ISSTA’06), Portland, Maine, USA, July 17-20, 2006, pp. 181–190 (2006)Google Scholar
  16. 16.
    Magee, J., Kramer, J., Giannakopoulou, D.: Behaviour Analysis of Software Architectures. In: I Working IFIP Conf. Sw Architecture, WICSA1 (1999)Google Scholar
  17. 17.
    Mariani, L., Pezze, M.: Behavior Capture and Test: Automated Analysis of Component Integration. In: IEEE Computer Society (ed.) 10th IEEE International Conference on Engineering of Complex Computer Systems, Shangai, China, 16-20 June, 2005, IEEE Computer Society Press, Los Alamitos (2005)Google Scholar
  18. 18.
    Muccini, H., Bertolino, A., Inverardi, P.: Using Software Architecture for Code Testing. IEEE Trans. on Software Engineering 30(3), 160–171 (2003)CrossRefGoogle Scholar
  19. 19.
    Pelliccione, P.: CHARMY: A framework for Software Architecture Specification and Analysis. PhD thesis, Computer Science Dept., U. L’Aquila (May 2005)Google Scholar
  20. 20.
    Szyperski, C.: Component Software. Beyond Object Oriented Programming. Addison-Wesley, Reading (1998)Google Scholar

Copyright information

© Springer Berlin Heidelberg 2007

Authors and Affiliations

  • Antonia Bertolino
    • 1
  • Henry Muccini
    • 2
  • Andrea Polini
    • 1
  1. 1.Istituto di Scienza e Tecnologie della Informazione “Alessandro Faedo”, Consiglio Nazionale delle Ricerche, via Moruzzi, 1 – 56124 PisaItaly
  2. 2.Dipartimento di Informatica, University of L’Aquila, Via Vetoio, 1 - L’AquilaItaly

Personalised recommendations