An approach for the verification of UML models using B

Ninh Thuan Truong 1 Jeanine Souquières 1
1 DEDALE - Development of specifications
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This paper describes the formal verification of UML models using B abstract machines and a support tool (AtelierB). We transform the UML metamodel to B and automatically check proof obligations generated by using the B prover. The correctness of the properties of UML models is ensured by the well-formedness rules in the UML semantics which are transformed to B as the invariants of abstract machines. We address the class diagram and study the Core Package (Backbone and Relationships) of the UML metamodel as well as the well-formedness rules of these packages.
Type de document :
Communication dans un congrès
Proceedings of the 11th International Conference and Workshop on the Engineering of Computer-Based Systems - ECBS'04, 2004, Brno, Czech, IEEE Computer Society, pp.95-102, 2004
Liste complète des métadonnées

https://hal.inria.fr/inria-00110557
Contributeur : Publications Loria <>
Soumis le : lundi 30 octobre 2006 - 17:30:47
Dernière modification le : mardi 24 avril 2018 - 13:30:22

Identifiants

  • HAL Id : inria-00110557, version 1

Collections

Citation

Ninh Thuan Truong, Jeanine Souquières. An approach for the verification of UML models using B. Proceedings of the 11th International Conference and Workshop on the Engineering of Computer-Based Systems - ECBS'04, 2004, Brno, Czech, IEEE Computer Society, pp.95-102, 2004. 〈inria-00110557〉

Partager

Métriques

Consultations de la notice

69