
By Achim D. Brucker and Burkhart Wolff.
We present the theorem proving environment HOL-OCL that is integrated in an 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 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.
Further Reading: This presentation is based on the following publication: A. D. Brucker and B. Wolff, “HOL-OCL – A Formal Proof Environment for UML/OCL,” in Fundamental approaches to software engineering (FASE08), J. Fiadeiro and P. Inverardi, Eds. Heidelberg: Springer-Verlag, 2008, pp. 97–100. doi: 10.1007/978-3-540-78743-3_8. Author copy: https://logicalhacking.com/publications/brucker.ea-hol-ocl-2008/
Please cite this work as follows: A. D. Brucker and B. Wolff, “HOL-OCL – a formal proof environment for UML/OCL,” Budapest, Hungary, Mar. 31, 2008. Author copy: https://logicalhacking.com/publications/talk-brucker.ea-hol-ocl-2008/
@Unpublished{ talk:brucker.ea:hol-ocl:2008,
date = {2008-03-31},
title = {{HOL-OCL} -- A Formal Proof Environment for {UML/OCL}},
language = {USenglish},
address = {Budapest, Hungary},
author = {Achim D. Brucker and Burkhart Wolff},
lecturer = {Achim D. Brucker},
event = {Fundamental Approaches to Software Engineering {(FASE
2008)}},areas = {software, formal methods},
abstract = {We present the theorem proving environment HOL-OCL that is
integrated in an 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
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.},note = {Author copy: \url{https://logicalhacking.com/publications/talk-brucker.ea-hol-ocl-2008/}},
pdf = {https://logicalhacking.com/publications/talk-brucker.ea-hol-ocl-2008/talk-brucker.ea-hol-ocl-2008.pdf},
}