Tutorial: Analyzing UML/OCL Models with HOL-OCL

By Achim D. Brucker and Burkhart Wolff.

In this tutorial, we present the theorem proving environment HOL-OCL. The HOL-OCL system is an interactive proof environment for UML/OCL specifications that is integrated in a Model-driven Engineering (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 of 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.

Supplementary material:
[  Examples  ]

Please cite this work as follows:
A. D. Brucker and B. Wolff, “Tutorial: Analyzing UML/OCL models with HOL-OCL,” presented at the MoDELS 2008, Toulouse, France, Sep. 28, 2008. Author copy: https://logicalhacking.com/publications/talk-brucker.ea-analyzing-2008/

BibTeX
@Unpublished{ talk:brucker.ea:analyzing:2008,
  date            = {2008-09-28},
  title           = {Tutorial: Analyzing {UML/OCL} Models with {HOL-OCL}},
  author          = {Achim D. Brucker and Burkhart Wolff},
  lecturer        = {Achim D. Brucker},
  day             = {28},
  eventtitle      = {MoDELS 2008},
  month           = {sep},
  year            = {2008},
  venue           = {Toulouse, France},
  abstract        = {In this tutorial, we present the theorem proving environment
                     HOL-OCL. The HOL-OCL system is an interactive proof
                     environment for UML/OCL specifications that is integrated in a
                     Model-driven Engineering (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 of 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.},
  areas           = {formal methods, software},
  supplementary01 = {/publications/talk-brucker.ea-analyzing-2008/talk-brucker.ea-analyzing-examples-2008.tar.gz},
  supplabel01     = {Examples},
  note            = {Author copy: \url{https://logicalhacking.com/publications/talk-brucker.ea-analyzing-2008/}},
  pdf             = {https://logicalhacking.com/publications/talk-brucker.ea-analyzing-2008/talk-brucker.ea-analyzing-2008.pdf},
}