Note publique d'information : La conception basée composants est une nouvelle méthode de construction d'applications
et de systèmes distribués. Cette conception par composition pose cependant plusieurs
problèmes, dûs aux services non uniformes (dépendants d'un contexte) et aux liens
dynamiques d'interconnexion entre les composants. Nous proposons un cadre formel pour
la vérification compositionelle de tels systèmes.Nous définissons un langage de type
d'interfaces comportementales, qui constitue un contrat comportemental pour le composant
et son environnement. Le composant doit respecter ce contrat; cette vérification est
basée sur un modèle de composant abstrait, dynamique et multi-tâche. Une deuxième
analyse, à l'assemblage des composants, étudie la compatibilité entre les contrats
mis en jeu, au moyen de règles de compatibilité d'interface et de sous-typage. Cette
double vérification nous permet de garantir que tout message envoyé sera consommé,
ainsi que l'absence d'interblocage externe entre les composants.
Note publique d'information : Component based design is a new methodology for the construction of distributed systems
and applications. This conception by composition gives rise to several problems, due
to non uniform services (depending on a context) and to dynamic interconnection links
between components. Our goal is to provide a formal framework for compositional verification
of those systems.We define a behavioural interface type language, which forms a behavioural
contract for the component and its environment. The component must honour its contract;
this verification is based on an abstract, dynamic and multi-threaded component model.
A second analysis, during the assembly of the components, studies compatibility of
contracts brought into play, using decidable interface compatibility and subtyping
rules. This double verification ensures that every sent message will be consumed,
and there will be no external deadlock between components.
paprika.idref.fr
data.idref.fr
Documentation
