HOL-OCL

HOL-OCL enables the formal analysis of UML/OCL models by addressing two key issues: first, it provides a formal semantics that aims for standard compliance (e.g., a four-valued logic) and, second, it is verification environment for UML/OCL.

HOL-OCL

HOL-OCL is both a formal semantics of the Object Constraint Language (OCL) and UML class models expressed in terms of higher-order logic (i.e., as a shallow embedding in Isabelle/HOL) and an interactive proof environment for UML/OCL.

Analysing a simple bank example using HOL-OCL 2.0.

HOL-OCL is jointly developed by the Software Assurance & Security Research Team at the University of Sheffield, UK and the Verified Algorithms, Languages and Systems team at the LRI (CNRS and University of Paris-Sud), France.

HOL-OCL is free software. For more information, please visit the HOL-OCL home page.

In the context of HOL-OCL we provide a collection of UML/OCL examples as well as su4sml, an SML repository for managing (Secure)UML/OCL models. Both are available in the HOL-OCL organization of our code repository.

Important Publications

[1]
A. D. Brucker, “An interactive proof environment for object-oriented specifications,” PhD thesis, ETH Zurich, 2007.
[2]
A. D. Brucker and B. Wolff, “An extensible encoding of object-oriented data models in HOL,” Journal of Automated Reasoning, vol. 41, pp. 219–249, 2008, doi: 10.1007/s10817-008-9108-3.
[3]
A. D. Brucker and B. Wolff, “Semantics, calculi, and analysis for object-oriented specifications,” Acta Informatica, vol. 46, no. 4, pp. 255–284, Jul. 2009, doi: 10.1007/s00236-009-0093-8.
[4]
A. D. Brucker, F. Tuong, and B. Wolff, “Featherweight OCL: A proposal for a machine-checked formal semantics for OCL 2.5,” Archive of Formal Proofs, Jan. 2014,