Formal Semantics of Static and Temporal State-Oriented OCL Constraints

The textual Object Constraint Language (OCL) is primarily intended to specify restrictions over UML class diagrams, in particular class invariants, operation pre-, and postconditions. Based on several improvements in the definition of the language concepts in last years, a proposal for a new version of OCL has recently been published [43]. That document provides an extensive OCL semantic description that constitutes a tight integration into UML. However, OCL still lacks a semantic integration of UML Statecharts, although it can already be used to refer to states in OCL expressions. This article presents an approach that closes this gap and introduces a formal semantics for such integration through a mathematical model. It also presents the definition of a temporal OCL extension by means of a UML Profile based on the metamodel of the latest OCL proposal. Our OCL extension enables modelers to specify behavioral state-oriented real-time constraints. It provides an intuitive understanding and readability at application level since common OCL syntax and concepts are preserved. A well-defined formal semantics is given through the mapping of temporal OCL expressions to temporal logics formulae.