The design of complex systems usually starts with a natural language specification which serves as the basis for the ongoing implementation. To deal with the increasing complexity, these informal specifications are extended by means of formal modeling languages such as the Unified Modeling Language (UML) and the Object Constraint Language (OCL). They enable to check the specification for conceptual errors and inconsistencies before a precise implementation is available. This paper presents methods which make use of these possibilities. It is illustrated which errors can already exist in specifications and how they can be detected automatically.
