Assembling components with behavioural contracts

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 com-munication 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 intersting properties, such as "external deadlock freeness " 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 compositionelle de ces systèmes reste cependant un problème. 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 compa-tibilité 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 d