@inproceedings{39069,
  abstract     = {{We present the syntax and semantics of a past- and future-oriented temporal extension of the Object Constraint Language (OCL). Our extension supports designers to express time-bounded properties over a state-oriented UML model of a system under development. The semantics is formally defined over the system states of a mathematical object model. Additionally, we present a mapping to Clocked Linear Temporal Logic (Clocked LTL) formulae, which is the basis for further application in verification with model checking. We demonstrate the applicability of the approach by the example of a buffer specification in the context of a production system.}},
  author       = {{Flake, Stephan and Müller, Wolfgang}},
  booktitle    = {{Proceedings of SEFM´04}},
  isbn         = {{0-7695-2222-X}},
  keywords     = {{Unified modeling language, Logic, Clocks, Boolean functions, Application software, Time factors, Real time systems, Formal verification, Buffer storage, Software packages}},
  publisher    = {{IEEE}},
  title        = {{{Past- and Future-Oriented Time-Bound Temporal Properties with OCL}}},
  doi          = {{10.1109/SEFM.2004.1347516}},
  year         = {{2004}},
}