Formal Analysis of UML/OCL Models

By Achim D. Brucker.

In this talk, 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 an MDE framework. HOL-OCL allows to reason over UML class models annotated with OCL specifications. Moreover, 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.

Please cite this work as follows:
A. D. Brucker, “Formal analysis of UML/OCL models,” presented at the Computer science colloquium at the university bremen, Bremen, Germany, Oct. 31, 2008. Author copy: http://logicalhacking.com/publications/talk-brucker-formal-2008/

BibTeX
@Unpublished{ talk:brucker:formal:2008,
  date       = {2008-10-31},
  title      = {Formal Analysis of {UML/OCL} Models},
  author     = {Achim D. Brucker},
  eventtitle = {Computer Science Colloquium at the University Bremen},
  venue      = {Bremen, Germany},
  abstract   = {In this talk, 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
                an MDE framework. HOL-OCL allows to reason over UML class
                models annotated with OCL specifications. Moreover, 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.},
  note       = {Author copy: \url{http://logicalhacking.com/publications/talk-brucker-formal-2008/}},
}