Abstract
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”.
Résumé
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».
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Abadi (M.), Lamport (L.), Conjoining specifications.Acm Transactions on Programming Languages and Systems 17, 3 (May 1995), pp. 507–535.
Carrez (C).Contrats Comportementaux pour Composants, PhD thesis,Enst, Paris, France, Dec. 2003.
Carrez (C),Fantechi (A.),Najm (E.), Behavioural contracts for a sound composition of components. InFORTE 2003, vol. 2767 ofLncs, Springer-Verlag, Sep. 2003.
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].
Colin (M.).Analyse Statique de la communication dans un langage d’acteur fonctionnel, PhDthesis, Instituqt National Polytechnique de Toulouse, Dec. 2002.
Colin (M.), TuiRloux (X.),Pantel (M.), Temporal logic based static analysis for non-uniform behaviours, InFmoods 2003, vol. 2884 ofLncs, Springer-Verlag, Nov. 2003.
De Alfaro (L.),Henzinger (T. A.). Interface automata. InEsec/fse-01 (2001), vol. 26,5 ofSOFTWARE ENGINEERING NOTES,Acm Press.
Flocft (J.).Towards Plug-and-Play Services: Design and Validation using Roles, PhD thesis,Ntnu, Trondheim, Norway, Feb. 2003.
Hennessy (M.),Riely (J.), Resource access control in systems of mobile agents,Infctrl: Information and Computation (formerly Information and Control) 173 (2002).
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.
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.
Kobayashi (N.), A type system for lock-free processes,Infctrl:Information and Computa-tion (fo merly Information and Control) 177 (2002).
Kobayashi (N.),Pierce (B. C),Turner (D. N.), Linearity and the Pi-Calculus,Acm Transactions on Programming Languages and Systems 21, 5 (1999).
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.
Liskov (B. H.), Wing (J. M.). A behavioral notion of subtyping,Acm Trans. Prog. Lang, and Sys. 16, 1 (Nov. 1994), pp. 1811–1841.
Misra (J.), Chandy (K. M), Proofs of networks of processes,IeeeTransactions on Software Engineering 7, 4 (July 1981), pp. 417–426.
Najm (E.),Nimour (A.),Stefani (J.-B.), Infinite types for distributed objects interfaces, InFmoods’99 (Firenze, Italy, Feb. 1999), Kluwer.
Nierstrasz (O.), Regular types for active objects, InObject-Oriented Software Composition, Prentice-Hall, 1995, pp. 99–121.
Ravara (A.),Vasconcelos (V. T.), Typing non-uniform concurrent objects, InConcur 2000 (2000), vol. 1877 ofLncs, Springer, pp. 474–488.
Vasconcelos (V. T.),Ravara (A.),Gay (S.), Session types for functional multithreading, InConcur 2004 (Sep. 2004), vol. 3170 ofLncs, Springer-Verlag.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Carrez, C., Fantechi, A. & Najm, E. Assembling components with behavioural contracts. Ann. Télécommun. 60, 989–1022 (2005). https://doi.org/10.1007/BF03219957
Received:
Accepted:
Issue Date:
DOI: https://doi.org/10.1007/BF03219957
Key words
- System design
- Component
- Distributed system
- Peer to peer networking
- Client-server architecture
- Software engineering
- Type theory
- Formal language
- Compatibility
- Bank institution