[. Fiadeiro, Interconnecting objects via contracts, Proceedings Technology of Object-Oriented Languages and Systems. TOOLS 38, 1999.
DOI : 10.1109/TOOLS.2001.911771
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.7483

[. Allen and D. Garlan, The wright architectural specication language. Rapport technique CMU-CS-96-TBD, 1996.

M. Y. Vardi, Alternating renement relations, Lecture Notes in Computer Science, vol.1466, p.163178, 1998.

M. Abadi and L. Lamport, Composing specifications, ACM Transactions on Programming Languages and Systems, vol.15, issue.1, pp.73-132, 1993.
DOI : 10.1145/151646.151649
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.33.1637

M. Abadi and L. Lamport, Conjoining specifications, ACM Transactions on Programming Languages and Systems, vol.17, issue.3, pp.507-535, 1995.
DOI : 10.1145/203095.201069
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.33.4928

R. J. Allen, A Formal Approach to Software Architecture

[. Abramsky and G. Mccusker, Game Semantics, H. Schwichtenberg et U. Berger, éditeurs : Logic and Computation : Proceedings of the 1997 Marktoberdorf Summer School
DOI : 10.1007/978-3-642-58622-4_1

[. Ábrahám-mumm, F. S. De-boer, W. De-roever, and M. Steffen, A hoare logic for monitors in java, 2003.

I. A. Agha, S. F. Mason, . Smith, and L. Carolyn, Talcott : A foundation for actor computation, Journal of Functional Programming, vol.7, issue.1, p.172, 1993.

J. Adamek and F. Plasil, Behavior protocols capturing errors and updates, Proceedings of the Second International Workshop on Unanticipated Software Evolution (USE 2003), ETAPS, 2003.

A. Bailly, Assume / Guarantee Contracts for Timed Mobile Objects, Thèse de doctorat, ENST, 2002.

L. Burdy, Y. Cheon, D. Cok, M. Ernst, J. Kiniry et al., Leino et Erik Poll : An overview of jml tools and applications, Thomas Arts et Wan Fokkink, éditeurs : Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS '03), volume 80 de Electronic Notes in Theoretical Computer Science, p.7389, 2003.

C. [. Brookes and A. W. Hoare, Roscoe : A theory of communicating sequential processes, Journal of the ACM (JACM), issue.3, p.31560599, 1984.

A. Beugnard, J. Jézéquel, N. Plouzeau, and D. Watkins, Making components contract aware, Computer, vol.32, issue.7, p.3845, 1999.
DOI : 10.1109/2.774917

[. Brörkens and M. Möller, Jassda trace assertions, runtime checking the dynamic of java programs, Trends in Testing Communicating Systems, International Conference on Testing of Communicating Systems, p.3948, 2002.

G. Boudol, Typing the use of resources in a concurrent calculus
DOI : 10.1007/3-540-63875-X_56

G. Boudol, The pi-calculus in direct style, Conference Record of POPL '97, p.228241, 1997.

]. R. Bry95 and . Bryant, Binary decision diagrams and beyond : Enabling technologies for formal verication, International Conference on Computer Aided Design, p.236245, 1995.

E. Cariou, Contribution à un processus de réication d'abstractions de communications, Thèse de doctorat, 2003.

[. Cariou, A. B. , E. Cariou, A. Beugnard, and J. Jézéquel, The specication of uml collaborations as interactions components An architecture and a process for implementing distributed collaborations, Fifth International Conference on the Unied Modeling Language 6th IEEE International Enterprise Distributed Object Computing Conference Ecole Polytechnique Fédérale de Lausanne (EPFL), 2002.

A. Chakrabarti, T. A. Luca-de-alfaro, M. Henzinger, . Jurdzi«ski, Y. C. Freddy et al., Mang : Interface compatibility checking for software modules, Lecture Notes in Computer Science, vol.02, p.428441, 2002.
DOI : 10.1007/3-540-45657-0_35
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.7.403

[. Chakrabarti, T. A. Luca-de-alfaro, . Henzinger, Y. C. Freddy, K. G. Brinksma et al., Mang : Synchronous and bidirectional component interfaces, Lecture Notes in Computer Science, vol.02, p.414427, 2002.
DOI : 10.1007/3-540-45657-0_34
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.126.266

A. Carrez, M. Fantechi-et-elie-najm-hartmut-könig, A. Heiner, and . Wolisz, Behavioural contracts for a sound composition of components, éditeurs : 23rd IFIP International Conference on Formal Techniques for Networked and Distributed Systems volume 2767 de LNCS, p.111126, 2003.

A. Carrez, E. Fantechi, and . Najm, Contrats comportementaux pour un assemblage sain de composants, Colloque Francophone sur l'Ingénierie des Protocoles (CFIP 2003)

. Carrez, Arnaud Georgin et Alexandre Tauveron : Spécication du prol uml d'assemblage cible ejb (version 2), Projet RNTL Accord, 2003.

R. H. Campbell and A. N. Habermann, The specication of process synchronization by path expressions, Lecture Notes in Computer Science, vol.16, p.89102, 1974.

[. Caron and A. Muller, Spécication du prol uml d'assemblage cible ccm (version 2), Projet RNTL Accord, 2003.

J. Colaço, Analyses Statiques d'un calcul d'Acteurs par typage, Thèse de doctorat, 1997.

M. Colin, Analyse Statique de la communication dans un langage d'acteur fonctionnel, Thèse de doctorat, 2002.

J. Colaço, M. Pantel, F. Dagnat, and P. Sallé, Safety analysis for non-uniform service availability in ac- Bibliographie tors. Dans Formal Methods for Open Object-based Distributed Systems (FMOODS'99), 1999.

[. Colin, X. Thirioux, and M. Pantel, Temporal logic based static analysis for non-uniform behaviours. Dans Elie Najm, Uwe Nestmann et Perdita Stevens, éditeurs : Formal Methods for Open Object-Based Distributed Systems, volume 2884 de LNCS, 2003.

. Luca-de-alfaro, A. T. Thomas, C. M. Henzinger, and . Kirsch, Henzinger : Interface theories for component-based design éditeurs : EMSOFT 01 : Embedded Software, volume 2211 de Lecture Notes in Computer Science, DPCS00] Fabien Dagnat, Marc Pantel, Matthias Colin et Patrick Sallé : Typing concurrent objects and actors. L'OBJET, p.148165, 2000.

D. Desmond, A. Souza, and . Wills, Objets, Components and Frameworks with UML The Catalysis approach, ECM02a] Common Language Infrastructure (CLI). ECMA TC39/TG3, p.335, 1998.

D. Fla03-]-gérard-florin-fabrice-legond-aubry and . Enselme, Modèle abstrait d'assemblage de composants par contrats, Projet RNTL Accord, 2003.

[. Findler, M. Latendresse, and M. Felleisen, Behavioral software contracts Rapport technique TR02-402, Flo67] R. W. Floyd : Assigning meaning to programs, 2002.

É. Schwartz, Mathematical aspects of computer science, Proc. American Mathematics Soc. symposia, p.19
DOI : 10.1090/psapm/019

R. Providence, E. Fontaine, M. Najm, and . Ruffin, Une approche de la composition de services par contrats de collaboration, CFIP'02 Colloque Francophone sur l'Ingénierie des Protocoles, 1967.

[. Février, E. Najm, and J. Stefani, Contracts for odp. Dans Transformation-Based Reactive Systems Development, 4th Internatio nal AMAST Workshop on Real-Time Systems and Concurrent and Distribute d Software, ARTS'97, Lecture Notes in Computer Science, vol.1231, p.216232, 1997.

J. Simon, M. Gay, and . Hole, Types and subtypes for clientserver interactions, European Symposium on Programming, p.7490, 1999.

M. [. Gay and . Hole, Types and subtypes for correct communication in client-server systems, 2003.

[. Gamma, R. Helm, R. Johnson, and J. Vlissides, Design Patterns : Elements of Reusable Object-Oriented Software

[. Helm, I. M. Holland, and D. Gangopadhyay, Contracts : Specing behaviorial compositions in object-oriented systems, Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'90), Proceedings, p.169180, 1990.

]. C. Hoa69 and . Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, p.576580, 1969.

A. Thomas, S. Henzinger, . Qadeer, K. Sriram, and . Rajamani, You assume, we guarantee : Methodology and case studies, J

M. Y. Hu and . Vardi, Computer-Aided Verication, Lecture Notes in Computer Science, vol.98, issue.1427, p.440451

A. Thomas, S. Henzinger, . Qadeer, and K. Sriram, Rajamani : Decomposing renement proofs using Assume-Guarantee reasoning

[. Honda, T. Vasco, M. Vasconcelos, and . Kubo, Language primitives and type disciplines for structured communicationbased programming, Chris Hankin, éditeur : Programming Languages and Systems : Proceedings of the 7th European Symposium on Programming (ESOP'98), volume 1381 de LNCS, p.22138

A. Igarashi and N. Kobayashi, A generic type system for the Pi-calculus A full version will be published as a, ACM SIGPLAN Notices, vol.36, issue.3, p.128141, 2001.

M. Jackson, Guide de l'amateur de Malt Whisky. Solar, 4è édition, 2000.

N. Kobayashi, A type system for lock-free processes. INFC- TRL : Information and Computation (formerly Information and Control), pp.122-159, 2002.

[. Kesten, L. Pnueli, E. Raviv, and . Shahar, Model checking with strong fairness Rapport technique MCS01-07 : Linearity and the Pi-Calculus, Mathematics & Bibliographie Computer Science Weizmann Institute Of Science ACM Transactions on Programming Languages and Systems, vol.21, issue.5, p.914947, 1999.

D. Laef03a-]-fabrice-legond-aubry, G. Enselme, and . Florin, Assembling contracts for components, 2003.

D. Laef03b-]-fabrice-legond-aubry, G. Enselme, and . Florin, Contrat d'assemblage de composants, Proceedings, 2003.

D. J. Lehmann, A. Pnueli, and J. Stavi, Impartiality, justice and fairness: The ethics of concurrent termination, éditeurs : Automata, Languages and Programming, 8th Colloquium, pp.264277-1317, 1981.
DOI : 10.1007/3-540-10843-2_22

L. Lamport and F. B. Schneider, The ``Hoare Logic'' of CSP, and All That, ACM Transactions on Programming Languages and Systems, vol.6, issue.2, p.281296, 1984.
DOI : 10.1145/2993.357247

K. G. Larsen, B. Steffen-et-carsten-weise-brinksma, R. Cleaveland, K. G. Larsen, T. Margaria et al., A constraint oriented proof methodology based on modal transition sytems éditeurs : Tools and Algorithms for Construction and Analysis of Systems, First International Workshop, TACAS'95, Proceedings, volume 1019 de Lecture Notes in Computer Science, p.1740, 1995.

A. Nancy, . Lynch, R. Mark, and . Tuttle, Hierarchical correctness proofs for distributed algorithms, éditeur : Proceedings of the 6th Annual ACM Symposium on Principles of Distributed Computing, p.137151, 1987.

A. Edward, Y. Lee, and . Xiong, System-level types for component-based design, Proofs of networks of processes, p.417426, 1981.

L. Kenneth and . Mcmillan, Circular compositional reasoning about liveness. Rapport technique, 1999.

N. [. Magee, S. Dulay, J. Eisenbach, and . Kramer, Specifying distributed software architectures, Schafer et P. Botella, éditeurs : Proc. 5th European Software Engineering Conf. (ESEC 95, p.137153, 1995.
DOI : 10.1007/3-540-60406-5_12
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.7933

J. Magee, N. Dulay, and J. Kramer, Regis: a constructive development environment for distributed programs, Distributed Systems Engineering, vol.1, issue.5
DOI : 10.1088/0967-1846/1/5/005

B. Meyer, Eiel : The Language, 1991.

[. Meyer, Applying 'design by contract', Computer, vol.25, issue.10, p.254051, 1992.
DOI : 10.1109/2.161279
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.72.7831

B. Meyer, What to compose. Software Development, mars, 2000.

. Microsoft, Shared source cli (codename : Rotor)

. Berlin-heidelberg, Also see S-V's LNCS, 1980.

]. R. Mil93, F. L. Milner, W. Bauer, and H. Brauer, The polyadic pi-calculus : a tutorial Schwichtenberg, éditeurs : Logic and Algebra of Specication Available also as Technical Repost ECS-LFCS-91-180, p.203246, 1991.

[. Meolic, Tatjana Kapus et Zmago Brezo£nik : Testing equivalence with binary decision diagrams

[. Möller, Specifying and checking java using CSP. Dans Workshop on Formal Techniques for Java-like Programs -FTf, 2002.

[. Medvidovic and R. N. Taylor, A classication and comparison framework for software architecture description languages, IEEE Transactions on Software Engineering, vol.26, issue.1, p.7093, 2000.

[. Ng and J. Kramer, Automated support for distributed software design, Proceedings Seventh International Workshop on Computer-Aided Software Engineering, 1995.
DOI : 10.1109/CASE.1995.465296

E. Najm, A. Nimour, and J. Stefani, Guaranteeing Liveness in an Object Calculus Through Behavioral Typing, Kluwer, éditeur : Proceedings of FORTE/PSTV'99, 1999.
DOI : 10.1007/978-0-387-35578-8_12

E. Najm, A. Nimour, and J. Stefani, Innite types for distributed objects interfaces, Proceedings of third IFIP conference on Formal Methods for Open Object-based Distributed Systems -FMOODS'99, 1999.
DOI : 10.1007/978-0-387-35562-7_28

[. Puntigam and C. Peter, Changeable interfaces and promised messages for concurrent components, Proceedings of the 1999 ACM symposium on Applied computing , SAC '99, 1999.
DOI : 10.1145/298151.298223

C. Benjamin, D. Pierce, and . Sangiorgi, Typing and subtyping for mobile processes, Proceedings 8th IEEE Logics in Computer Science, p.376385, 1993.

F. Puntigam, Coordination requirements expressed in types for active objects, European Conference on Object-Oriented Programming (ECOOP'97), volume 1241 de Lecture Notes in Computer Science, p.367387, 1997.
DOI : 10.1007/BFb0053387

[. Amestoy, Non-regular process types, Proceedings of the 5th European Conference on Parallel Processing (Euro-Par'99), numéro 1685 dans LNCS ?, 1999.

[. Plasil and S. Vi²novský, Behavior protocols for software components, IEEE Transactions on Software Engineering, vol.28, issue.11, 2002.
DOI : 10.1109/TSE.2002.1049404
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.23.9185

P. [. Ravara, V. Resende, and . Vasconcelos, An Algebra of Behavioural Types, Information and Computation, vol.212, pp.1049-1050, 2002.
DOI : 10.1016/j.ic.2011.12.005

[. Vasconcelos, Typing nonuniform concurrent objects, Palamidessi, éditeur : 11th International Conference on Concurrency Theory, CONCUR 2000, Proceedings., volume 1877 de Lecture Notes in Computer Science, p.474488, 2000.

J. Soucé and L. Duchien, État de l'art sur les langages de description d'architecture. Rapport technique Livrable 1.1- 2, Projet RNTL Accord, 2002.

M. Shaw and D. Garlan, Software Architecture : Perspective on an Emerging Discipline, 1996.

J. Stefani, A calculus of higher-order distributed components . Rapport technique 4692, INRIA, SARDES project, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00071894

C. Szyperski, Component Software Beyond Object-Oriented Programming, 2002.

[. Takeuchi, K. Honda, and M. Kubo, An interactionbased language and its typing system, Proc. of PARLE'94, numéro 817 dans Lecture Notes in Computer Science, p.398413, 1994.
DOI : 10.1007/3-540-58184-7_118
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.45.1431

J. Talpin and P. Jouvelot, The type and eect discipline, Seventh Annual IEEE Symposium on Logic in Computer Science, p.162173, 1992.

S. Vi²novský, Modeling Software Components Using Behavior Protocols, Thèse de doctorat, 2002.

G. H. Wright, Deontic logic. Mind, p.60115, 1951.

T. Vasco, M. Vasconcelos, and . Tokoro, A typing system for a calculus of objects, Object Technologies for Advanced Software, First JSSST International Symposium, p.460474

[. Vallecillo and T. Vasco, Vasconcelos et António Ravara : Typing the behavior of objects and components using session types

. Ximian, Projet mono. http://www.go-mono.com

N. Yoshida, Type-based liveness guarantee in the presence of nonterminatio n and nondeterminism, MCS, 2002.