%0 Book Section
%T HOL-OCL ? A Formal Proof Environment for UML/OCL
%A Brucker, Achim D.
%A Wolff, Burkhart
%E Fiadeiro, José
%E Inverardi, Paola
%B Fundamental Approaches to Software Engineering (FASE08)
%D 2008
%N 4961
%I Springer-Verlag
%C Heidelberg
%G USenglish
%F brucker.ea:hol-ocl:2008
%X We present the theorem proving environment HOL-OCL that is integrated in a MDE framework. HOL-OCL allows to reason over UMLclass 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.
%K HOL-OCL, UML, OCL, Formal Methods, Theorem Proving, Refinement
%U http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-ocl-2008
%U http://www.brucker.ch/bibliography/download/2008/brucker.ea-hol-ocl-2008.pdf
%U http://dx.doi.org/10.1007/978-3-540-78743-3_8
%P 97-100