Skip to Main content Skip to Navigation

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.
Document type :
Complete list of metadata
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 9:41:08 AM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM


  • HAL Id : inria-00099777, version 1



Ninh Thuan Truong, Jeanine Souquières. An approach for the verification of UML models using B. [Intern report] A03-R-444 || truong03a, 2003. ⟨inria-00099777⟩



Record views