Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    Checking the Consistency of UML Class Diagrams Using Larch Prover

    Rigorous Object-Oriented Methods 2000

    York, UK. 17 January 2000


    P. Andre, A. Romanczuk & J.C. Royer


    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 semantics 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 abstract 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.


    PDF filePDF Version of this Paper (75kb)