Tutorial: Analyzing UML/OCL Models with HOL-OCL

@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{http://logicalhacking.com/publications/talk-brucker.ea-analyzing-2008/}},
}