Sciweavers

Share
ROOM
2000

Checking the Consistency of UML Class Diagrams Using Larch Prover

8 years 7 months ago
Checking the Consistency of UML Class Diagrams Using Larch Prover
The Unified Modeling Language (UML) has been designed to be a full standard notation for Object-Oriented Modelling. UML is a rather complete set of notations, but it lacks of formal semantics. This article introduces formal s for UML based on algebraic abstract data types. We currently consider only class and object diagrams. These diagrams include class structures, associations, multiplicities, constraints, instances as well as specialization relationships. We give a formal semantics for each of these elements by interpreting the structure of a class as an data type, associations as values of type Association, and specialization as structural projection. We show that a tool like Larch Prover is able to support proofs over UML diagrams. We use the critical pair computation to find out inconsistencies. Several different inconsistencies of class diagrams are shown on a library example.
Pascal André, Annya Romanczuk, Jean-Claude
Added 01 Nov 2010
Updated 01 Nov 2010
Type Conference
Year 2000
Where ROOM
Authors Pascal André, Annya Romanczuk, Jean-Claude Royer
Comments (0)
books