Abstract: This paper presents a formal behavioural specification framework together with its applications in different contexts for specifying and verifying the correct behaviour of distributed Fractal components. Our framework allows us to build behavioural models for applications ranging from sequential Fractal components, to distributed objects, and finally distributed components. Our models are able to characterise both functional and non-functional behaviours, and the interaction between the two concerns. Finally, this work has resulted in the development of tools allowing the non-expert programmer to specify the behaviour of his components, and automatically, or semi-automatically verify properties of his application.  Key-words: Résumé : Cet article présente un modèle formel pour la spécification comportementale, ainsi que son applicationà différents contextes, permettant de spécifier et de vérifier le comportement de composants répartisà la Fractal. Notre méthode permet de construire des modèles comportementaux pour des applications allant des composants Fractal sèquentiels, aux objets répartis, jusqu'aux composants répartis. Nos modèles sont capables de représenterà la fois les comportements fonctionnels et les aspects non-fonctionnels, ainsi que l'interaction entre les deux. Par ailleurs, ce travail a donné lieu au développement d'outils logiciels permettantà un utilisateur non-expert de spécifier le comportement de ses composants, et de vérifier, automatiquement ou semiautomatiquement, leurs propriètès.
In REF , the authors present a formal framework for behavioural specification of distributed Fractal components.
Behavioural models for distributed fractal components
Proc. of the IEEE
Computer Science