Synchronous Formalism and Behavioral Substitutability in Component Frameworks

LES AUTEURS Sabine Moisan, Annie Ressouche et Jean Paul Rigault

RESUME:

When using a component framework, developers need to respect the behavior implemented by the components. Static information about the component interface is not sufficient. Dynamic information such as the description of valid sequences of operations is required. In this paper we propose a mathematical model obeying the Synchronous hypothesis and a formal language to describe the knowledge about behavior.
We focus on extension of components, owing to the notion of behavioral substitutability. A formal semantics for the language is defined and a compositionality result allows us to get modular model checking facilities. From the language and the model, we can draw practical design rules that are sufficient to preserve behavioral substitutability. Associated tools may ensure correct (re)use of
components, as well as automatic simulation and verification, code generation, and run-time checks.

Mots clé: component frameworks, protocol of use, behavioral substitutability, synchronous models,model-checking verification

Pour télécharger cet article, cliquez ici

BibTeX reference:

@InProceedings{MRR05,
  author =       {Moisan , S. and Ressouche, A. and Rigault, J-P.},
  title =        {{Synchronous Formalism and Behavioral Substitutability    in Component Frameworks}},
  editor =       "Maraninchi, F.",
  booktitle =    "Synchronous Languages Applications and Programming",
  year =         "2005",
  publisher    = {Elsevier Science },
  series       =  {LNCS},
}

Dernière mise à jour : 8/04/05
Catherine.Martin@sophia.inria.fr