This article describes a systematic translation of UML Class Diagrams into a formal specification to uncover most of the UML inconsistencies published to date. Examples of inconsistent UML class diagrams presented in previous research studies were used to validate the approach. The formal model obtained from UML class diagrams helped to uncover inconsistencies without any further proof. In order to relieve the user from writing a much rigorous and precise formalism, a tool that automatically generates the formal model from the UML class diagram was developed.
This article illustrated most frequent UML inconsistencies published so far using Anthony Hall’s model most of these are translated into contradictory predicates. In some ambiguous cases, UML must be supplemented by an additional formal semantic. Typically UML lacks a semantic for multiple inheritance of attributes with the same name. A prototype has been developed to automatically translate UML designs into their formal counterpart. The Z notation makes the formal translation of the design particularly suitable for further investigation in Z.