Utilisation de B pour la vérification de spécifications UML et le développement formel orienté objet
Résumé
The coupling of object-oriented approaches with the B method makes improvement the activities of software specification and development. The B method provides notations for the specification and powerful tools, allowing to specify and verify models. The object-oriented approaches provide interesting mechanisms for the structuring and the development of large systems. The contribution of this thesis deals with the activities of coupling between these two formalisms by using the B provers to validate and verify UML specifications.
By extending the derivation of UML to B of preceding works realised in the Dedale research group, we propose an approach of the derivation to B of the UML meta-models, the static diagrams and the dynamic diagrams. The aim of this proposition is to check semantics and coherence between different diagrams of UML specification.
Our thesis brings also a contribution to the development of objects oriented specifications using B. The first proposition concerns the taking into account some types of association between classes during the derivation to B. The second relates the validation of object-oriented specifications described by UML2.0 sequence diagrams.
By extending the derivation of UML to B of preceding works realised in the Dedale research group, we propose an approach of the derivation to B of the UML meta-models, the static diagrams and the dynamic diagrams. The aim of this proposition is to check semantics and coherence between different diagrams of UML specification.
Our thesis brings also a contribution to the development of objects oriented specifications using B. The first proposition concerns the taking into account some types of association between classes during the derivation to B. The second relates the validation of object-oriented specifications described by UML2.0 sequence diagrams.
Le couplage des approches orientées objets avec la méthode B est une piste pour l'amélioration de l'activité de spécification et de développement de logiciels. La méthode B fournit des notations et des outils supports puissants permettant de modéliser et de vérifier des modèles. Les approches objets fournissent des mécanismes intéressants pour la structuration et le développement de gros systèmes. L'apport de notre travail de thèse contribue aux activités de couplage entre ces deux formalismes en utilisant le prouveur de B pour valider et vérifier des spécifications UML.
En étendant les schémas de dérivation d'UML vers B proposés dans des travaux précédents réalisés dans l'équipe de recherche Dédale, nous proposons une approche de dérivation en B de méta-modèles UML, de diagrammes statiques et de diagrammes dynamiques. L'objectif de cette proposition est de vérifier la sémantique et la cohérence entre différents diagrammes de spécifications UML.
Notre thèse apporte aussi une contribution au développement de spécifications objets en utilisant la méthode B. La première proposition concerne la prise en compte de certains types d'associations entre classes lors de la dérivation en B. La deuxième proposition concerne la validation de spécifications orientées objets décrites à l'aide de diagrammes de séquence UML2.0.
En étendant les schémas de dérivation d'UML vers B proposés dans des travaux précédents réalisés dans l'équipe de recherche Dédale, nous proposons une approche de dérivation en B de méta-modèles UML, de diagrammes statiques et de diagrammes dynamiques. L'objectif de cette proposition est de vérifier la sémantique et la cohérence entre différents diagrammes de spécifications UML.
Notre thèse apporte aussi une contribution au développement de spécifications objets en utilisant la méthode B. La première proposition concerne la prise en compte de certains types d'associations entre classes lors de la dérivation en B. La deuxième proposition concerne la validation de spécifications orientées objets décrites à l'aide de diagrammes de séquence UML2.0.