An OCL Extension for Formulating Temporal Constraints

UML class diagrams are widely used to model the static structure of object-oriented software systems. The textual language OCL, which is part of the UML, is used for formulating constraints that can not be modeled by the diagrams. In this paper, we extend OCL with elements of linear temporal logic. With this extended OCL, which we call TOCL, we want to give software engineers a user-friendly means to specify constraints on the temporal evolution of the system structure as well as on the system behavior by stating temporal invariants and preand postconditions. We formally define syntax and semantics of the extended OCL.