HOL-OCL - A Formal Proof Environment for UML/OCL
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: (article) (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
(article) (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}, | |
| = | {http://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 | = | {http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-ocl-2008}, | |
| year | = | {2008}, |