TY  - CHAP
AU  - Brucker, Achim D.
AU  - Wolff, Burkhart
ED  - Fiadeiro, José
ED  - Inverardi, Paola
PY  - 2008//
TI  - HOL-OCL ? A Formal Proof Environment for UML/OCL
BT  - Fundamental Approaches to Software Engineering (FASE08)
T3  - Lecture Notes in Computer Science
SP  - 97
EP  - 100
IS  - 4961
PB  - Springer-Verlag
CY  - Heidelberg
KW  - HOL-OCL, UML, OCL, Formal Methods, Theorem Proving, Refinement
N2  - 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.
UR  - http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-ocl-2008
L1  - http://www.brucker.ch/bibliography/download/2008/brucker.ea-hol-ocl-2008.pdf
UR  - http://dx.doi.org/10.1007/978-3-540-78743-3_8
ID  - brucker.ea:hol-ocl:2008
ER  -