Verification of UML Model Elements Using B

Ninh Thuan Truong (1) , Jeanine Souquières (1)

1 DEDALE - Development of specifications

This paper describes the formal verification of UML model elements using B abstract machines. We study the UML metamodel of class diagrams, collaboration diagrams and state-chart diagrams as well as their well-formedness rules. Each element of UML models which is an instance of a metaclass, is transformed into a B abstract machine. The relationship between abstract machines is organised using the abstract syntax of UML class diagram of the UML metamodel. B specifications are proved by a B prover which generates automatically proof obligations, allowing UML model elements to be verified. The correctness of the UML model elements is ensured by the well-formedness rules which are transformed to B invariants. We illustrate our approach by a simple case study, the printing system.

Mots clés: B method; UML models; UML metamodel; formal verification; well-formedness rules

Domaines: Génie logiciel [cs.SE]

Ninh Thuan Truong, Jeanine Souquières. Verification of UML Model Elements Using B. Journal of Information Science and Engineering, 2006, 22, pp.357-373. ⟨hal-00097566⟩