pdfreaders.org

HOL-OCL - A Formal Proof Environment for UML/OCL

by Achim D. Brucker and Burkhart Wolff

Cover for brucker.ea:hol-ocl:2008.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.

Keywords: HOL-OCL, UML, OCL, Formal Methods, Theorem Proving, Refinement
Categories: ,
Documents: (full text as PDF file) (slides) (handout)

QR Code for brucker.ea:hol-ocl:2008.Please cite this article as follows:
Achim D. Brucker and Burkhart Wolff. HOL-OCL - A Formal Proof Environment for UML/OCL. In Fundamental Approaches to Software Engineering (FASE08). Lecture Notes in Computer Science (4961), pages 97-100, Springer-Verlag, 2008.
Keywords: HOL-OCL, UML, OCL, Formal Methods, Theorem Proving, Refinement
(full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-540-78743-3_8) (Share article on LinkedIn. Share article on CiteULike. )

BibTeX
@InCollection{ brucker.ea:hol-ocl:2008,
abstract = {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.},
address = {Heidelberg},
author = {Achim D. Brucker and Burkhart Wolff},
booktitle = {Fundamental Approaches to Software Engineering {(FASE08)}},
doi = {10.1007/978-3-540-78743-3_8},
editor = {Jos{\'e} Fiadeiro and Paola Inverardi},
keywords = {HOL-OCL, UML, OCL, Formal Methods, Theorem Proving, Refinement},
language = {USenglish},
location = {Budapest, Hungary},
number = {4961},
pages = {97--100},
pdf = {https://www.brucker.ch/bibliography/download/2008/brucker.ea-hol-ocl-2008.pdf},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
talk = {brucker.ea:hol-ocl:2008},
title = {{HOL-OCL} -- {A Formal Proof Environment for {UML}/{OCL}}},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-hol-ocl-2008},
year = {2008},
}