by Achim D. Brucker and Burkhart Wolff
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)
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) (
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}, | |
= | {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}, |