HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Consistency checking of UML static diagrams 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 transformation of UML static diagrams into B for verifying the consistency of UML properties. Class diagrams, object diagrams and OCL constraints are transformed into B abstract machines which are then combined into a complete B specification. UML object diagrams provide the data, meanwhile constraints on associations in class diagrams and constraints expressed by OCL give invariants for the B specification. Proof obligations automatically generated by the support tool (AtelierB) are used to check the consistency of UML specifications.
Document type :
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 10:15:44 AM
Last modification on : Friday, February 26, 2021 - 3:28:07 PM


  • HAL Id : inria-00100225, version 1



Ninh Thuan Truong, Jeanine Souquières. Consistency checking of UML static diagrams using B. [Intern report] A04-R-268 || truong04e, 2004, 14 p. ⟨inria-00100225⟩



Record views