11th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems (ECBS'04)
An Approach for the Verification of UML Models Using B
Brno, Czech Republic
May 24-May 27
ISBN: 0-7695-2125-8
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.
Citation:
Ninh-Thuan Truong, Jeanine Souquieres, "An Approach for the Verification of UML Models Using B," ecbs, pp.195, 11th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems (ECBS'04), 2004