@Phdthesis{Richters:2002:DISS,
  author =       "Mark Richters",
  title =        "A Precise Approach to Validating {UML} Models and {OCL}
                  Constraints",
  school =       "Universit{\"a}t Bremen",
  year =         "2002",
  address =      "Logos Verlag, Berlin, BISS Monographs, No. 14",
  isbn =         "3-89722-842-4",
  abstract =     "We present a precise approach that allows an analysis and
                  validation of UML models and OCL constraints. We focus on
                  models and constraints specified in the analysis and
                  early design stage of a software development process. For
                  this purpose, a suitable subset of UML corresponding to
                  information that is usually represented in class diagrams
                  is identified and formally defined. This basic modeling
                  language provides a context for all OCL constraints. We
                  define a formal syntax and semantics of OCL types,
                  operations, expressions, invariants, and
                  pre-/postconditions. We also give solutions for problems
                  with the current OCL definition and discuss possible
                  extensions.  A metamodel for OCL is introduced that
                  defines the abstract syntax of OCL expressions and the
                  structure of types and values. The metamodel approach
                  allows a seamless integration with the UML metamodeling
                  architecture and makes the benefits of a precise OCL
                  definition easier accessible. The OCL metamodel also
                  allows to define context-sensitive conditions for
                  well-formed OCL expressions more precisely. These
                  conditions can now be specified with OCL whereas they
                  previously were specified only informally. In order to
                  demonstrate the practical applicability of our work, we
                  have realized substantial parts of it in a tool
                  supporting the validation of models and constraints.
                  Design specifications can be ``executed'' and animated
                  thus providing early feedback in an iterative development
                  process. Our approach offers novel ways for checking user
                  data against specifications, for automating test
                  procedures, and for checking CASE tools for standards
                  conformance. Therefore, this work contributes to the goal
                  of improving the overall quality of software systems by
                  combining theoretical and practical techniques.",
}