Abstract
We present the theorem proving environment holocl that is integrated in a Model-driven Engineering (mde) framework. holocl allows to reason over uml class models annotated with ocl specifications. Thus, holocl strengthens a crucial part of the uml to an object-oriented formal method. holocl 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.
Chapter PDF
Similar content being viewed by others
Keywords
References
Brucker, A.D.: An Interactive Proof Environment for Object-oriented Specifications. Ph.d. thesis, ETH Zurich (March 2007), ETH Dissertation No. 17097, http://www.brucker.ch/bibliography/abstract/brucker-interactive-2007
Brucker, A.D., Wolff, B.: The HOL-OCL book. Technical Report 525, ETH Zurich (2006), http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-ocl-book-2006
Brucker, A.D., Doser, J., Wolff, B.: An MDA framework supporting OCL. Electronic Communications of the EASST, 5 (2006), ISSN 1863-2122, http://www.brucker.ch/bibliography/abstract/brucker.ea-mda-2006-b
Object Management Group. UML 2.0 OCL specification, October 2003, Available as OMG document ptc/03-10-14
Object Management Group. Unified modeling language specification (version 1.5) (March 2003), Available as OMG document, formal/03-03-01
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brucker, A.D., Wolff, B. (2008). HOL-OCL: A Formal Proof Environment for uml/ocl . In: Fiadeiro, J.L., Inverardi, P. (eds) Fundamental Approaches to Software Engineering. FASE 2008. Lecture Notes in Computer Science, vol 4961. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78743-3_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-78743-3_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78742-6
Online ISBN: 978-3-540-78743-3
eBook Packages: Computer ScienceComputer Science (R0)