Verification of behavioural elements of UML models using B
Ninh-Thuan Truong, Jeanine Souquières · 2005
This paper describes the formal verification of behavioural elements of UML models using B abstract machines. We transform the UML metamodel of behavioural diagrams to B and automatically check proof obligations generated by using the B prover. The correctness of the properties of behavioural elements 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 collaboration diagrams, state-chart diagrams of UML models and study the Behavioural Elements package (Collaboration and State Machine) of the UML metamodel as well as well-formedness rules of these packages. We illustrate our approach by a case study.