pdfreaders.org

The HOL-OCL Book

Achim D. Brucker und Burkhart Wolff

Cover for brucker.ea:hol-ocl-book:2006.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

Schlüsselwörter: security, SecureUML, UML, OCL, HOL-OCL, model-transformation
Kategorien: ,
Dokumente: (Artikel als PDF Datei)

QR Code for brucker.ea:hol-ocl-book:2006.Bitte zitieren sie diesen Artikel wie folgt:
Achim D. Brucker und Burkhart Wolff. The HOL-OCL Book. ETH Zurich, Technical Report 525, 2006.
Schlüsselwörter: security, SecureUML, UML, OCL, HOL-OCL, model-transformation
(Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (Share article on LinkedIn. Share article on CiteULike.)

BibTeX
@TechReport{ brucker.ea:hol-ocl-book:2006,
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},
author = {Achim D. Brucker and Burkhart Wolff},
bibkey = {brucker.ea:hol-ocl-book:2006},
institution = {ETH Zurich},
keywords = {security, SecureUML, UML, OCL, HOL-OCL, model-transformation},
language = {USenglish},
number = {525},
pdf = {https://www.brucker.ch/bibliography/download/2006/brucker.ea-hol-ocl-book-2006.pdf},
title = {The {HOL-OCL} Book},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-hol-ocl-book-2006},
year = {2006},
}