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

Achim D. Brucker und 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.

Schluesselwörter: HOL-OCL, UML, OCL, Formal Methods, Theorem Proving, Refinement
Kategorien: Formale Methoden, Softwaretechnik

Bitte zitieren sie diesen Artikel wie folgt:
Achim D. Brucker und 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.
Schluesselwörter: HOL-OCL, UML, OCL, Formal Methods, Theorem Proving, Refinement
(PDF) (BibTeX) (Endnote) (RIS) (doi:10.1007/978-3-540-78743-3_8) (Share article on LinkedIn. Share article on CiteULike. Share article on Connotea.)