A Proposal for a Formal OCL Semantics in Isabelle/HOL

Achim D. Brucker und Burkhart Wolff

Cover for brucker.ea:proposal:2002.We present a formal semantics as a conservative shallow embedding of the Object Constraint Language (OCL). OCL is currently under development within an open standardization process within the OMG; our work is an attempt to accompany this process by a proposal solving open questions in a consistent way and exploring alternatives of the language design. Moreover, our encoding gives the foundation for tool supported reasoning over OCL specifications, for example as basis for test case generation.

Schlüsselwörter: Isabelle, OCL, UML, shallow embedding, testing
Kategorien: ,
Dokumente: (Artikel als PDF Datei) (Extended Version)

QR Code for brucker.ea:proposal:2002.Bitte zitieren sie diesen Artikel wie folgt:
Achim D. Brucker und Burkhart Wolff. A Proposal for a Formal OCL Semantics in Isabelle/HOL. In Theorem Proving in Higher Order Logics (TPHOLs). Lecture Notes in Computer Science (2410), pages 99-114, Springer-Verlag, 2002.
Schlüsselwörter: Isabelle, OCL, UML, shallow embedding, testing
(Artikel als PDF Datei) (Extended Version) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/3-540-45685-6_8) (Share article on LinkedIn. Share article on CiteULike.)

BibTeX
@InCollection{ brucker.ea:proposal:2002,
abstract = {We present a formal semantics as a conservative shallow embedding of the Object Constraint Language (OCL). OCL is currently under development within an open standardization process within the OMG; our work is an attempt to accompany this process by a proposal solving open questions in a consistent way and exploring alternatives of the language design. Moreover, our encoding gives the foundation for tool supported reasoning over OCL specifications, for example as basis for test case generation.},
address = {Heidelberg},
author = {Achim D. Brucker and Burkhart Wolff},
booktitle = {Theorem Proving in Higher Order Logics (TPHOLs)},
doi = {10.1007/3-540-45685-6_8},
editor = {V{\'\i}ctor A. Carre{\~n}o and C{\'e}sar A. Mu{\~n}oz and Sophi{\`e}ne Tahar},
file = {https://www.brucker.ch/bibliography/download/2002/brucker.ea-proposal-extended-2002.pdf},
filelabel = {Extended Version},
isbn = {3-540-44039-9},
issn = {0302-9743},
keywords = {Isabelle, OCL, UML, shallow embedding, testing},
language = {USenglish},
location = {Hampton, VA, USA},
number = {2410},
pages = {99--114},
pdf = {https://www.brucker.ch/bibliography/download/2002/brucker.ea-proposal-2002.pdf},
project = {CSFMDOS},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
title = {A Proposal for a Formal {OCL} Semantics in {Isabelle/HOL}},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-proposal-2002},
year = {2002},
}