Behavioural Contracts for a Sound Assembly of Components

  • Cyril Carrez
  • Alessandro Fantechi
  • Elie Najm
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2767)


Component based design is a new methodology for the construction of distributed systems and applications. In this new setting, a system is built by the assembly of (pre)-existing components. Remains the problem of the compositional verification of such systems. We investigate methods and concepts for the provision of “sound” assemblies. We define an abstract, dynamic, multi-threaded, component model, encompassing both client/server and peer to peer communication patterns. We define a behavioural interface type language endowed with a (decidable) set of interface compatibilty rules. Based on the notion of compliance of components to their interfaces, we define the concepts of “contract” and “contract satisfaction”. This leads to the notion of sound assemblies of components, i.e., assemblies made of contracted components interacting through compatible interfaces. Sound assemblies possess interesting properties like “external deadlock freeness” and “message consumption”.


  1. [Bai02]
    Bailly, A.: Assume / Guarantee Contracts for Timed Mobile Objects. PhD thesis, ENST (December 2002) Google Scholar
  2. [dAH01]
    de Alfaro, L., Henzinger, T.A.: Interface automata. In: ESEC/FSE 2001, SOFTWARE ENGINEERING NOTES, vol. 26(5). ACM Press, New York (2001) Google Scholar
  3. [HR02]
    Hennessy, M., Riely, J.: Resource access control in systems of mobile agents. INFCTRL: Information and Computation (formerly Information and Control) 173 (2002)Google Scholar
  4. [Kob02]
    Kobayashi, N.: A type system for lock-free processes. INFCTRL: Information and Computation (formerly Information and Control) 177 (2002)Google Scholar
  5. [KPT99]
    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
  6. [LSW95]
    Larsen, K.G., Steffen, B., Weise, C.: A constraint oriented proof methodology based on modal transition sytems. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol. 1019. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  7. [Nie95]
    Nierstrasz, O.: Regular types for active objects. In: Object-Oriented Software Composition, pp. 99–121. Prentice-Hall, Englewood Cliffs (1995)Google Scholar
  8. [NNS99]
    Najm, E., Nimour, A., Stefani, J.-B.: Guaranteeing liveness in an object calculus through behavioral typing. In: Proc. of FORTE/PSTV 1999 (October 1999)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2003

Authors and Affiliations

  • Cyril Carrez
    • 1
  • Alessandro Fantechi
    • 2
    • 3
  • Elie Najm
    • 1
  1. 1.Département INFRESEcole Nationale Supérieure des TélécommunicationsParisFrance
  2. 2.Dipartimento di Sistemi e InformaticaUniversitá di FirenzeFirenzeItaly
  3. 3.ISTI – CNRPisaItaly

Personalised recommendations