TY - CHAP AU - Brucker, Achim D. AU - Wolff, Burkhart ED - Fiadeiro, José ED - Inverardi, Paola PY - 2008 DA - 2008// TI - HOL-OCL – A Formal Proof Environment for UML/OCL BT - Fundamental Approaches to Software Engineering (FASE08) T3 - Lecture Notes in Computer Science SP - 97 EP - 100 IS - 4961 PB - Springer-Verlag CY - Heidelberg KW - HOL-OCL, UML, OCL, Formal Methods, Theorem Proving, Refinement AB - 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. L1 - https://www.brucker.ch/bibliography/download/2008/brucker.ea-hol-ocl-2008.pdf UR - https://www.brucker.ch/bibliography/abstract/brucker.ea-hol-ocl-2008 UR - https://doi.org/10.1007/978-3-540-78743-3_8 DO - 10.1007/978-3-540-78743-3_8 LA - USenglish ID - brucker.ea:hol-ocl:2008 ER -