pdfreaders.org

Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5

by Achim D. Brucker, Frédéric Tuong, and Burkhart Wolff

Cover for brucker.ea:formal-semantics-ocl-2.5:2015.The Unified Modeling Language (UML) is one of the few modeling languages that is widely used in industry. While UML is mostly known as diagrammatic modeling language (e.g., visualizing class models), it is complemented by a textual language, called Object Constraint Language (OCL). OCL is a textual annotation language, originally based on a three-valued logic, that turns UML into a formal language. Unfortunately the semantics of this specification language, captured in the "Annex A" of the OCL standard, leads to different interpretations of corner cases. Many of these corner cases had been subject to formal analysis since more than ten years.

The situation complicated with the arrival of version 2.3 of the OCL standard. OCL was aligned with the latest version of UML: this led to the extension of the three-valued logic by a second exception element, called null. While the first exception element invalid has a strict semantics, null has a non strict interpretation. The combination of these semantic features lead to remarkable confusion for implementors of OCL compilers and interpreters.

In this paper, we provide a formalization of the core of OCL in HOL. It provides denotational definitions, a logical calculus and operational rules that allow for the execution of OCL expressions by a mixture of term rewriting and code compilation. Moreover, we describe a coding-scheme for UML class models that were annotated by code-invariants and code contracts. An implementation of this coding-scheme has been undertaken: it consists of a kind of compiler that takes a UML class model and translates it into a family of definitions and derived theorems over them capturing the properties of constructors and selectors, tests and casts resulting from the class model. However, this compiler is not included in this document.

Our formalization reveals several inconsistencies and contradictions in the current version of the OCL standard. They reflect a challenge to define and implement OCL tools in a uniform manner. Overall, this document is intended to provide the basis for a machine-checked text "Annex A" of the OCL standard targeting at tool implementors.

Keywords:
Categories: ,
Documents: (full text as PDF file)

QR Code for brucker.ea:formal-semantics-ocl-2.5:2015.Please cite this article as follows:
Achim D. Brucker, Frédéric Tuong, and Burkhart Wolff. Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5. LRI, Univ Paris Sud, CNRS, Centrale Supélec, Université Paris-Saclay, France, Technical Report 1582, 2015.
(full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (Share article on LinkedIn. Share article on CiteULike. )

BibTeX
@TechReport{ brucker.ea:formal-semantics-ocl-2.5:2015,
abstract = {The Unified Modeling Language (UML) is one of the few modeling languages that is widely used in industry. While UML is mostly known as diagrammatic modeling language (e.g., visualizing class models), it is complemented by a textual language, called Object Constraint Language (OCL). OCL is a textual annotation language, originally based on a three-valued logic, that turns UML into a formal language. Unfortunately the semantics of this specification language, captured in the ``Annex A'' of the OCL standard, leads to different interpretations of corner cases. Many of these corner cases had been subject to formal analysis since more than ten years.\\\\The situation complicated with the arrival of version 2.3 of the OCL standard. OCL was aligned with the latest version of UML: this led to the extension of the three-valued logic by a second exception element, called null. While the first exception element invalid has a strict semantics, null has a non strict interpretation. The combination of these semantic features lead to remarkable confusion for implementors of OCL compilers and interpreters.\\\\In this paper, we provide a formalization of the core of OCL in HOL. It provides denotational definitions, a logical calculus and operational rules that allow for the execution of OCL expressions by a mixture of term rewriting and code compilation. Moreover, we describe a coding-scheme for UML class models that were annotated by code-invariants and code contracts. An implementation of this coding-scheme has been undertaken: it consists of a kind of compiler that takes a UML class model and translates it into a family of definitions and derived theorems over them capturing the properties of constructors and selectors, tests and casts resulting from the class model. However, this compiler is not included in this document.\\\\Our formalization reveals several inconsistencies and contradictions in the current version of the OCL standard. They reflect a challenge to define and implement OCL tools in a uniform manner. Overall, this document is intended to provide the basis for a machine-checked text ``Annex A'' of the OCL standard targeting at tool implementors.},
author = {Achim D. Brucker and Fr{\'e}d{\'e}ric Tuong and Burkhart Wolff},
institution = {LRI, Univ Paris Sud, CNRS, Centrale Sup\'elec, Universit\'e Paris-Saclay, France},
language = {USenglish},
month = {sep},
num_pages = {196},
number = {1582},
pdf = {https://www.brucker.ch/bibliography/download/2015/brucker.ea-formal-semantics-ocl-2.5-2015.pdf},
title = {Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-formal-semantics-ocl-2.5-2015},
year = {2015},
}