To cite the use of this formal theory, please use

  Achim D. Brucker, Frédéric Tuong, and Burkhart Wolff. Featherweight
  OCL: A Proposal for a Machine-Checked Formal Semantics for OCL
  2.5. In Archive of Formal Proofs,
  2014. http://www.isa-afp.org/entries/Featherweight_OCL.shtml, Formal
  proof development

A BibTeX entry for LaTeX users is

@Article{ brucker.ea:featherweight:2014,
      abstract  = {The Unified Modeling Language (UML) is one of the
                  few modeling languages that is widely used in
                  industry. While UML is mostly known as diagrammatic
                  modeling language (e.g., visualizing class models),
                  it is complemented by a textual language, called
                  Object Constraint Language (OCL). OCL is based on a
                  three-valued logic that turns UML into a formal
                  language. Unfortunately the semantics of this
                  specification language, captured in the "Annex A" of
                  the OCL standard, leads to different interpretations
                  of corner cases. We formalize the core of OCL:
                  denotational definitions, a logical calculus and
                  operational rules that allow for the execution of
                  OCL expressions by a mixture of term rewriting and
                  code compilation. Our formalization reveals several
                  inconsistencies and contradictions in the current
                  version of the OCL standard. Overall, this document
                  is intended to provide the basis for a
                  machine-checked text "Annex A" of the OCL standard
                  targeting at tool implementors.},
       author	= {Achim D. Brucker and Fr{\'e}d{\'e}ric Tuong and Burkhart Wolff},
       file	= {https://www.brucker.ch/bibliography/download/2014/brucker.ea-featherweight-outline-2014.pdf},
       filelabel= {Outline},
       issn	= {2150-914x},
       journal	= {Archive of Formal Proofs},
       month	= {jan},
       note	= {\url{http://www.isa-afp.org/entries/Featherweight_OCL.shtml}, Formal proof development},
       pdf	= {https://www.brucker.ch/bibliography/download/2014/brucker.ea-featherweight-2014.pdf},
       title	= {Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5},
       url	= {https://www.brucker.ch/bibliography/abstract/brucker.ea-featherweight-2014},
       year	= {2014},
}


An overview of the formalization is given in:

  Achim D. Brucker and Burkhart Wolff. Featherweight OCL: A study for
  the consistent semantics of OCL 2.3 in HOL. In Workshop on OCL and
  Textual Modelling (OCL 2012). , pages 19-24, 2012. The semantics for
  the Boolean operators proposed in this paper was adopted by the OCL
  2.4 standard.

A BibTeX entry for LaTeX users is

@InProceedings{ brucker.ea:featherweight:2012,
    abstract = {At its origins, OCL was conceived as a strict
                semantics for undefinedness, with the exception of the
                logical connectives of type Boolean that constitute a
                three-valued propositional logic. Recent versions of
                the OCL standard added a second exception element,
                which, similar to the null references in programming
                languages, is given a non-strict semantics.\\\\In this
                paper, we report on our results in formalizing the
                core of OCL in higher-order logic (HOL). This
                formalization revealed several inconsistencies and
                contradictions in the current version of the OCL
                standard. These inconsistencies and contradictions are
                reflected in the challenge to define and implement OCL
                tools (e.g., interpreters, code-generators, or theorem
                provers) in a uniform manner.},

    author   = {Achim D. Brucker and Burkhart Wolff},
    booktitle= {Workshop on OCL and Textual Modelling (OCL 2012)},
    doi      = {10.1145/2428516.2428520},
    isbn     = {978-1-4503-1799-3},
    keywords = {OCL, HOL-OCL, formal semantics},
    note     = {The semantics for the Boolean operators proposed in this paper
                was adopted by the OCL 2.4 standard.},
    pages    = {19--24},
    pdf      = {https://www.brucker.ch/bibliography/download/2012/brucker.ea-featherweight-2012.pdf},
    talk     = {talk:brucker.ea:featherweight:2012},
    title    = {Featherweight OCL: A study for the consistent semantics of OCL 2.3 in HOL},
    url      = {https://www.brucker.ch/bibliography/abstract/brucker.ea-featherweight-2012},
    year     = {2012},
}