A Proposal for a Formal OCL Semantics in Isabelle/HOL

By Achim D. Brucker and Burkhart Wolff.

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.

Keywords:
Isabelle, OCL, UML, Shallow Embedding, Testing

Please cite this work as follows:
A. D. Brucker and B. Wolff, “A proposal for a formal OCL semantics in Isabelle/HOL,” in Theorem proving in higher order logics (TPHOLs), V. A. Carreño, C. A. Muñoz, and S. Tahar, Eds. Heidelberg: Springer-Verlag, 2002, pp. 99–114. doi: 10.1007/3-540-45685-6_8. Author copy: https://logicalhacking.com/publications/brucker.ea-proposal-2002/

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.},
  keywords  = {Isabelle, OCL, UML, Shallow Embedding, Testing},
  location  = {Hampton, VA, USA},
  author    = {Achim D. Brucker and Burkhart Wolff},
  booktitle = {Theorem Proving in Higher Order Logics (TPHOLs)},
  editor    = {V{\'\i}ctor A. Carre{\~n}o and C{\'e}sar A. Mu{\~n}oz and
               Sophi{\`e}ne Tahar},
  language  = {USenglish},
  publisher = {Springer-Verlag },
  address   = {Heidelberg },
  series    = {Lecture Notes in Computer Science },
  number    = {2410},
  pages     = {99--114},
  doi       = {10.1007/3-540-45685-6_8},
  title     = {A Proposal for a Formal {OCL} Semantics in {Isabelle/HOL}},
  areas     = {formal methods, software},
  isbn      = {3-540-44039-9},
  issn      = {0302-9743},
  year      = {2002},
  note      = {Author copy: \url{https://logicalhacking.com/publications/brucker.ea-proposal-2002/}},
  pdf       = {https://logicalhacking.com/publications/brucker.ea-proposal-2002/brucker.ea-proposal-2002.pdf},
}