OCL meets CTL: Towards CTL-Extended OCL Model Checking

R. Bill,S. Gabmeyer, P. Kaufmann, M. Seidl:
"OCL meets CTL: Towards CTL-Extended OCL Model Checking";
Vortrag: 13th International Workshop on OCL, Model Constraint and Query Languages (OCL 2013), Miami, USA; 30.09.2013; in:"Proceedings of the MODELS 2013 OCL Workshop", CEUR Workshop Proceedings, Vol-1092 (2013), ISSN: 1613-0073; S. 13 - 22.

[ Publication Database ]


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.