HOL-OCL – A Formal Proof Environment for UML/OCL

By Achim D. Brucker and Burkhart Wolff.

We present the theorem proving environment HOL-OCL that is integrated in an MDE framework. HOL-OCL allows to reason over UML class models annotated with OCL specifications. Thus, HOL-OCL strengthens a crucial part of the UML to an object-oriented formal method. HOL-OCL provides several derived proof calculi that allow for formal derivations establishing the validity of UML/OCL formulae. These formulae arise naturally when checking the consistency of class models, when formally refining abstract models to more concrete ones or when discharging side-conditions from model-transformations.

Keywords:
HOL-OCL, UML, OCL, Formal Methods, Theorem Proving, Refinement

Supplementary material:
[ Slides  ]

Please cite this work as follows:
A. D. Brucker and B. Wolff, “HOL-OCL – A Formal Proof Environment for UML/OCL,” in Fundamental approaches to software engineering (FASE08), J. Fiadeiro and P. Inverardi, Eds. Heidelberg: Springer-Verlag, 2008, pp. 97–100. doi: 10.1007/978-3-540-78743-3_8. Author copy: https://logicalhacking.com/publications/brucker.ea-hol-ocl-2008/

BibTeX
@InCollection{ brucker.ea:hol-ocl:2008,
  abstract  = {We present the theorem proving environment HOL-OCL that is
               integrated in an MDE framework. HOL-OCL allows to reason over
               UML class models annotated with OCL specifications. Thus,
               HOL-OCL strengthens a crucial part of the UML to an
               object-oriented formal method. HOL-OCL provides several
               derived proof calculi that allow for formal derivations
               establishing the validity of UML/OCL formulae. These formulae
               arise naturally when checking the consistency of class models,
               when formally refining abstract models to more concrete ones
               or when discharging side-conditions from
               model-transformations.},
  keywords  = {HOL-OCL, UML, OCL, Formal Methods, Theorem Proving,
               Refinement},
  location  = {Budapest, Hungary},
  author    = {Achim D. Brucker and Burkhart Wolff},
  booktitle = {Fundamental Approaches to Software Engineering {(FASE08)}},
  language  = {USenglish},
  publisher = {Springer-Verlag },
  address   = {Heidelberg },
  series    = {Lecture Notes in Computer Science },
  number    = {4961},
  doi       = {10.1007/978-3-540-78743-3_8},
  pages     = {97--100},
  editor    = {Jos{\'e} Fiadeiro and Paola Inverardi},
  title     = {{HOL-OCL} -- {A Formal Proof Environment for {UML}/{OCL}}},
  areas     = {formal methods, software},
  year      = {2008},
  note      = {Author copy: \url{https://logicalhacking.com/publications/brucker.ea-hol-ocl-2008/}},
  pdf       = {https://logicalhacking.com/publications/brucker.ea-hol-ocl-2008/brucker.ea-hol-ocl-2008.pdf},
}