@TechReport{	  brucker.ea:hol-ocl-book:2006,
  author	= {Achim D. Brucker and Burkhart Wolff},
  institution	= {ETH Zurich},
  language	= {USenglish},
  title		= {The {HOL-OCL} Book},
  classification= {unrefereed},
  areas		= {formal methods, software},
  categories	= {holocl},
  year		= {2006},
  number	= {525},
  abstract	= {HOL-OCL is an interactive proof environment for the Object
		  Constraint Language (OCL). It is implemented as a shallow
		  embedding of OCL into the Higher-order Logic (HOL) instance
		  of the interactive theorem prover Isabelle. HOL-OCL defines
		  a machine-checked formalization of the semantics as
		  described in the standard for OCL 2.0. This conservative,
		  shallow embedding of UML/OCL into Isabelle/HOL includes
		  support for typed, extensible UML data models supporting
		  inheritance and subtyping inside the typed lambda-calculus
		  with parametric polymorphism. As a consequence of
		  conservativity with respect to higher-order logic (HOL), we
		  can guarantee the consistency of the semantic model.
		  Moreover, HOL-OCL provides several derived calculi for
		  UML/OCL that allow for formal derivations establishing the
		  validity of UML/OCL formulae. Elementary automated support
		  for such proofs is also provided top },
  bibkey	= {brucker.ea:hol-ocl-book:2006},
  pdf		= {http://www.brucker.ch/bibliography/download/2006/brucker.ea-hol-ocl-book-2006.pdf},
  keywords	= {security, SecureUML, UML, OCL, HOL-OCL,
		  model-transformation},
  public	= {yes},
  url		= {http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-ocl-book-2006}
		  
}