In this tutorial, we present the theorem proving environment HOL-OCL. The HOL-OCL system (http://www.brucker.ch/projects/hol-ocl/) 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.
For a preliminary version of the the slides, please have a look on the tutorial given MoDELS 2008..