Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5

By Achim D. Brucker, Frédéric Tuong, and Burkhart Wolff.

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.

Please cite this work as follows:
A. D. Brucker, F. Tuong, and B. Wolff, “Featherweight OCL: A proposal for a machine-checked formal semantics for OCL 2.5,” Archive of Formal Proofs, Jan. 2014. https://www.isa-afp.org/entries/Featherweight_OCL.shtml, Formal proof development. Author copy: http://logicalhacking.com/publications/brucker.ea-featherweight-2014/

BibTeX
@Article{ brucker.ea:featherweight:2014,
  author    = {Achim D. Brucker and Fr{\'e}d{\'e}ric Tuong and Burkhart
               Wolff},
  title     = {{Featherweight} {OCL}: A Proposal for a Machine-Checked
               Formal Semantics for {OCL} 2.5},
  journal   = {Archive of Formal Proofs},
  month     = {jan},
  year      = {2014},
  note      = {\url{https://www.isa-afp.org/entries/Featherweight_OCL.shtml},
               Formal proof development. 
               Author copy: \url{http://logicalhacking.com/publications/brucker.ea-featherweight-2014/}},
  issn      = {2150-914x},
  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.},
  filelabel = {Outline},
  file      = {download/2014/brucker.ea-featherweight-outline-2014.pdf},
  areas     = {formal methods, software},
}