In software modeling, the Object Constraint Language (OCL) is an important language to specify properties that a model has to satisfy. The design of OCL reflects the structure of MOF-based modeling languages like UML and its tight integration results in an intuitive usability. But OCL allows to express properties only in the context of a single instance model and not with respect to a sequence of instance models that capture the execution of the system. 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 formally introduce syntax and semantics of our OCL extension cOCL. The properties specified with our OCL extension can be verified with our explicit state space model checking framework, called MocOCL. In a case study, we illustrate the expressiveness and usability of our approach and evaluate the performance of our implementation.
CITATION STYLE
Bill, R., Gabmeyer, S., Kaufmann, P., & Seidl, M. (2014). Model checking of CTL-extended OCL specifications. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 8706, 221–240. https://doi.org/10.1007/978-3-319-11245-9_13
Mendeley helps you to discover research relevant for your work.