Annales Des Télécommunications

, Volume 60, Issue 7–8, pp 989–1022 | Cite as

Assembling components with behavioural contracts

  • Cyril Carrez
  • Alessandro Fantechi
  • Elie Najm


Component based design is a new paradigm to build distributed systems and applications. The problem of compositional verification of such systems is however still open. We investigate methods and concepts for the provision of “sound” assemblies. We define a behavioural interface type language endowed with a (decidable) set of interface compatibilty and subtyping rules. We define an abstract, dynamic, multi-threaded, component model, encompassing both client/server and peer to peer communication patterns. Based on the notion of compliance of components to their interfaces, we define the concepts of “contract” and “contract satisfaction”. This leads to sound assemblies of components, which possess interesting properties, such as “external deadlockfreeness” and “message consumption”.

Key words

System design Component Distributed system Peer to peer networking Client-server architecture Software engineering Type theory Formal language Compatibility Bank institution 

Assemblage de Composants Selon des Contrats Comportementaux


La conception basée composants est une nouvelle méthode de construction d’applications et de systèmes distribués. La vérification compositionnelle de ces systèmes reste cependant un problème ouvert. Nous étudions des méthodes et des concepts pour la construction d’assemblages « sains ». Nous définissons un langage de type d’interfaces comportementales, doté d’un ensemble de règles (décidables) de compatibilité d’interface et de sous-typage. Nous définissons un modèle de composant abstrait, dynamique et multi-tâche, qui englobe les modèles client/serveur et point-à-point. Basé sur la notion de conformité du composant par rapport à son interface, nous définissons les concepts de « contrat » et « respect de contrat ». Cela mène aux assemblages sains de composants qui possèdent des propriétés intéressantes, comme «l’absence d’interblocage externe » et «la consommation des messages».

Mots clés

Conception système Composant Système réparti Communication égal à égal Architecture client serveur Génie logiciel Théorie types Langage formel Compatibilité Banque 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Abadi (M.), Lamport (L.), Conjoining specifications.Acm Transactions on Programming Languages and Systems 17, 3 (May 1995), pp. 507–535.CrossRefGoogle Scholar
  2. [2]
    Carrez (C).Contrats Comportementaux pour Composants, PhD thesis,Enst, Paris, France, Dec. 2003.Google Scholar
  3. [3]
    Carrez (C),Fantechi (A.),Najm (E.), Behavioural contracts for a sound composition of components. InFORTE 2003, vol. 2767 ofLncs, Springer-Verlag, Sep. 2003.Google Scholar
  4. [4]
    Carrez (C),Fantechi (A.),Najm (E.), Contrats comportementaux pour un assemblage sain de composants. In Colloque Francophone sur l’Ingénierie des Protocoles (Cfip 2003) (Paris, France, Oct. 2003). French version of [3].Google Scholar
  5. [5]
    Colin (M.).Analyse Statique de la communication dans un langage d’acteur fonctionnel, PhDthesis, Instituqt National Polytechnique de Toulouse, Dec. 2002.Google Scholar
  6. [6]
    Colin (M.), TuiRloux (X.),Pantel (M.), Temporal logic based static analysis for non-uniform behaviours, InFmoods 2003, vol. 2884 ofLncs, Springer-Verlag, Nov. 2003.Google Scholar
  7. [7]
    De Alfaro (L.),Henzinger (T. A.). Interface automata. InEsec/fse-01 (2001), vol. 26,5 ofSOFTWARE ENGINEERING NOTES,Acm Press.Google Scholar
  8. [8]
    Flocft (J.).Towards Plug-and-Play Services: Design and Validation using Roles, PhD thesis,Ntnu, Trondheim, Norway, Feb. 2003.Google Scholar
  9. [9]
    Hennessy (M.),Riely (J.), Resource access control in systems of mobile agents,Infctrl: Information and Computation (formerly Information and Control) 173 (2002).Google Scholar
  10. [10]
    Henzinger (T. A.),Qadeer (S.),Rajamani (S. K.), Decomposing refinement proofs using Assume-Guarantee reasoning, In Computer Aided Design (Iccad-2000), Proceedings. (Nov. 2000),Ieee Computer Society Press.Google Scholar
  11. [11]
    Jiang (S.),Carrez (C),Aagesen (F. A.), Automatic translation of service specification to a behavioral type language for dynamic service verification, InRapid Integration of Software Engineering techniques RISE 2004, Proceedings (Luxembourg, Nov. 2004), pp. 31–40.Google Scholar
  12. [12]
    Kobayashi (N.), A type system for lock-free processes,Infctrl:Information and Computa-tion (fo merly Information and Control) 177 (2002).Google Scholar
  13. [13]
    Kobayashi (N.),Pierce (B. C),Turner (D. N.), Linearity and the Pi-Calculus,Acm Transactions on Programming Languages and Systems 21, 5 (1999).Google Scholar
  14. [14]
    Larsen (K.),Steffen (B.),Weise (C), A constraint oriented proof methodology based on modal transition sytem,. InTools and Algorithms for Construction and Analysis of Systems,Tacas’95 (1995), vol. 1019 ofLncs.Google Scholar
  15. [15]
    Liskov (B. H.), Wing (J. M.). A behavioral notion of subtyping,Acm Trans. Prog. Lang, and Sys. 16, 1 (Nov. 1994), pp. 1811–1841.CrossRefGoogle Scholar
  16. [16]
    Misra (J.), Chandy (K. M), Proofs of networks of processes,IeeeTransactions on Software Engineering 7, 4 (July 1981), pp. 417–426.MathSciNetGoogle Scholar
  17. [17]
    Najm (E.),Nimour (A.),Stefani (J.-B.), Infinite types for distributed objects interfaces, InFmoods’99 (Firenze, Italy, Feb. 1999), Kluwer.Google Scholar
  18. [18]
    Nierstrasz (O.), Regular types for active objects, InObject-Oriented Software Composition, Prentice-Hall, 1995, pp. 99–121.Google Scholar
  19. [19]
    Ravara (A.),Vasconcelos (V. T.), Typing non-uniform concurrent objects, InConcur 2000 (2000), vol. 1877 ofLncs, Springer, pp. 474–488.Google Scholar
  20. [20]
    Vasconcelos (V. T.),Ravara (A.),Gay (S.), Session types for functional multithreading, InConcur 2004 (Sep. 2004), vol. 3170 ofLncs, Springer-Verlag.Google Scholar

Copyright information

© Springer-Verlag France 2005

Authors and Affiliations

  • Cyril Carrez
    • 1
    • 2
  • Alessandro Fantechi
    • 3
    • 4
  • Elie Najm
    • 2
  1. 1.Department of TelematicsNorwegian University of Science and TechnologyTrondheimNorway
  2. 2.Département INFRESGET/Télécom ParisParisFrance
  3. 3.Dipartimento di Sistemi e InformaticaUniversita di FirenzeFirenzeItaly
  4. 4.ISTI-CNRPisaItaly

Personalised recommendations