An approach for the verification of UML models using B

We describe 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 proven 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.