Checking Component Composability

  • Christian Attiogbé
  • Pascal André
  • Gilles Ardourel
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4089)


Component-Based Software Engineering (CBSE) is one of the approaches to master the development of large scale software. In this setting, the verification concern is still a challenge. The current work addresses the composability of components and their services. A component model (Kmelia) is introduced; an associated formalism, simple but expressive is introduced; it describes the services as extended LTSs and their structuring as components. The composability of components is defined on the basis of the composability of services. To ensure the correctness of component composition, we check that an assembly is possible via the checking of the composability of the linked services, and their behavioural compatibility. In order to mechanize our approach, the services and the components are translated into the Lotos formalism. Finally the Lotos CADP toolbox is used to perform experiments.


Components Services Behavioural Interface Description Composability Behavioural Verification 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Allen, R., Garlan, D.: A Formal Basis for Architectural Connection. ACM Transactions on Software Engineering and Methodology 6(3), 213–249 (1997)CrossRefGoogle Scholar
  2. 2.
    André, P., Ardourel, G., Attiogbé, C.: Behavioural Verification of Service Composition. In: ICSOC/Workshop on Engineering Service Compositions, WESC 2005 (2005)Google Scholar
  3. 3.
    André, P., Ardourel, G., Attiogbé, C., Habrias, H., Stoquer, C.: A Service-Based Component Model: Formalism, Analysis and Mechanization. Technical Report RR05.08, LINA (December 2005)Google Scholar
  4. 4.
    Attie, P.C., Lorenz, D.H.: Correctness of Model-based Component Composition without State Explosion. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol. 2743. Springer, Heidelberg (2003)Google Scholar
  5. 5.
    Attie, P.C., Lorenz, D.H.: Establishing Behavioral Compatibility of Software Components without State Explosion. Technical Report NU-CCIS-03-02, College of Computer and Information Science, Northeastern University (2003)Google Scholar
  6. 6.
    Bergner, K., Rausch, A., Sihling, M., Vilbig, A., Broy, M.: A Formal Model for Componentware. In: Leavens, G.T., Sitaraman, M. (eds.) Foundations of Component-Based Systems, pp. 189–210. Cambridge University Press, New York (2000)Google Scholar
  7. 7.
    Bracciali, A., Brogi, A., Canal, C.: A Formal Approach to Component Adaptation. Journal of Systems and Software 74(1), 45–54 (2005)CrossRefGoogle Scholar
  8. 8.
    de Alfaro, L., Henzinger, T.A.: Interface Automata. In: Proceedings of the Ninth Annual Symposium on Foundations of Software Engineering (FSE), pp. 109–120. ACM Press, New York (2001)Google Scholar
  9. 9.
    Fernandez, J.-C., Garavel, H., Kerbrat, A., Mateescu, R., Mounier, L., Sighireanu, M.: CADP: A Protocol Validation and Verification Toolbox. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 437–440. Springer, Heidelberg (1996)Google Scholar
  10. 10.
    Giannakopoulou, D., Kramer, J., Cheung, S.C.: Behaviour Analysis of Distributed Systems Using the Tracta Approach. ASE 6(1), 7–35 (1999)Google Scholar
  11. 11.
    Gschwind, T., Aßmann, U., Nierstrasz, O. (eds.): SC 2005. LNCS, vol. 3628. Springer, Heidelberg (2005)Google Scholar
  12. 12.
    Heineman, G.T., Crnković, I., Schmidt, H.W., Stafford, J.A., Szyperski, C.A., Wallnau, K. (eds.) CBSE 2005. LNCS, vol. 3489. Springer, Heidelberg (2005)Google Scholar
  13. 13.
    Inverardi, P., Wolf, A.L., Yankelevich, D.: Static Checking of System Behaviors using Derived Component Assumptions. ACM Transactions on Software Engineering and Methodology 9(3), 239–272 (2000)CrossRefGoogle Scholar
  14. 14.
    ISO LOTOS: A Formal Description Technique Based on The Temporal Ordering of Observational Behaviour. International Organisation for Standardization - Information Processing Systems - Open Systems Interconnection, Geneva (1988)Google Scholar
  15. 15.
    Medvidovic, N., Taylor, R.N.: A Classification and Comparison Framework for Software Architecture Description Languages. IEEE Transactions on Software Engineering 26(1), 70–93 (2000)CrossRefGoogle Scholar
  16. 16.
    Pavel, S., Noyé, J., Poizat, P., Royer, J.C.: A Java Implementation of a Component Model with Explicit Symbolic Protocols. In: Gschwind et al. (eds.) [11], pp. 115–124Google Scholar
  17. 17.
    Plasil, F., Visnovsky, S.: Behavior Protocols for Software Components. IEEE Transactions on SW Engineering 28(9) (2002)Google Scholar
  18. 18.
    Südholt, M.: A Model of Components with Non-regular Protocols. In: Gschwind et al. (eds.) [11], pp. 99–113Google Scholar
  19. 19.
    Szyperski, C.: Component Software: Beyond Object-Oriented Programming. Addison Wesley Publishing Company, Reading (1997)Google Scholar
  20. 20.
    Xie, F., Browne, J.C.: Verified Systems by Composition from Verified Components. In: ESEC/FSE-11: Proc. of the 9th European software engineering conference, New York, NY, USA, pp. 277–286. ACM Press, New York (2003)Google Scholar
  21. 21.
    Yellin, D.M., Strom, R.E.: Protocol Specifications and Component Adaptors. ACM Transactions on Programming Languages and Systems 19(2), 292–333 (1997)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Christian Attiogbé
    • 1
  • Pascal André
    • 1
  • Gilles Ardourel
    • 1
  1. 1.LINA CNRS FRE 2729University of NantesNantesFrance

Personalised recommendations