OCL meets CTL: Towards CTL-Extended OCL Model Checking.
Robert G. Bill, Sebastian Gabmeyer, Petra Radeljak Kaufmann, Martina Seidl · 2013
Abstract. In software modeling, the Object Constraint Language (OCL) is an important tool to specify properties that a model has to satisfy. The design of OCL reflects the structure of MOF-based modeling languages like UML and the tight integration results in an intuitive usability. However, OCL allows to express properties in the context of the current state of an instance model only but not with respect to its evolution. In this paper, we show how OCL can be extended with CTL-based temporal operators to express properties over the lifetime of an instance model. We explain syntax and semantics of our OCL extension and provide a prototypical implementation of our MocOCL model checker. 1