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.

Further Reading:
This presentation is based on the following publication:
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/

Please cite this work as follows:
A. D. Brucker and B. Wolff, “HOL-OCL – a formal proof environment for UML/OCL,” Budapest, Hungary, Mar. 31, 2008. Author copy: https://logicalhacking.com/publications/talk-brucker.ea-hol-ocl-2008/

BibTeX
@Unpublished{ talk:brucker.ea:hol-ocl:2008,
  date     = {2008-03-31},
  title    = {{HOL-OCL} -- A Formal Proof Environment for {UML/OCL}},
  language = {USenglish},
  address  = {Budapest, Hungary},
  author   = {Achim D. Brucker and Burkhart Wolff},
  lecturer = {Achim D. Brucker},
  event    = {Fundamental Approaches to Software Engineering {(FASE
              2008)}},
  areas    = {software, formal methods},
  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.},
  note     = {Author copy: \url{https://logicalhacking.com/publications/talk-brucker.ea-hol-ocl-2008/}},
  pdf      = {https://logicalhacking.com/publications/talk-brucker.ea-hol-ocl-2008/talk-brucker.ea-hol-ocl-2008.pdf},
}