---
_id: '39069'
abstract:
- lang: eng
  text: 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:
- first_name: Stephan
  full_name: Flake, Stephan
  last_name: Flake
- first_name: Wolfgang
  full_name: Müller, Wolfgang
  id: '16243'
  last_name: Müller
citation:
  ama: 'Flake S, Müller W. Past- and Future-Oriented Time-Bound Temporal Properties
    with OCL. In: <i>Proceedings of SEFM´04</i>. IEEE; 2004. doi:<a href="https://doi.org/10.1109/SEFM.2004.1347516">10.1109/SEFM.2004.1347516</a>'
  apa: Flake, S., &#38; Müller, W. (2004). Past- and Future-Oriented Time-Bound Temporal
    Properties with OCL. <i>Proceedings of SEFM´04</i>.  Proceedings of the Second
    International Conference on Software Engineering and Formal Methods. <a href="https://doi.org/10.1109/SEFM.2004.1347516">https://doi.org/10.1109/SEFM.2004.1347516</a>
  bibtex: '@inproceedings{Flake_Müller_2004, place={Beijing, China}, title={Past-
    and Future-Oriented Time-Bound Temporal Properties with OCL}, DOI={<a href="https://doi.org/10.1109/SEFM.2004.1347516">10.1109/SEFM.2004.1347516</a>},
    booktitle={Proceedings of SEFM´04}, publisher={IEEE}, author={Flake, Stephan and
    Müller, Wolfgang}, year={2004} }'
  chicago: 'Flake, Stephan, and Wolfgang Müller. “Past- and Future-Oriented Time-Bound
    Temporal Properties with OCL.” In <i>Proceedings of SEFM´04</i>. Beijing, China:
    IEEE, 2004. <a href="https://doi.org/10.1109/SEFM.2004.1347516">https://doi.org/10.1109/SEFM.2004.1347516</a>.'
  ieee: 'S. Flake and W. Müller, “Past- and Future-Oriented Time-Bound Temporal Properties
    with OCL,” presented at the  Proceedings of the Second International Conference
    on Software Engineering and Formal Methods, 2004, doi: <a href="https://doi.org/10.1109/SEFM.2004.1347516">10.1109/SEFM.2004.1347516</a>.'
  mla: Flake, Stephan, and Wolfgang Müller. “Past- and Future-Oriented Time-Bound
    Temporal Properties with OCL.” <i>Proceedings of SEFM´04</i>, IEEE, 2004, doi:<a
    href="https://doi.org/10.1109/SEFM.2004.1347516">10.1109/SEFM.2004.1347516</a>.
  short: 'S. Flake, W. Müller, in: Proceedings of SEFM´04, IEEE, Beijing, China, 2004.'
conference:
  name: ' Proceedings of the Second International Conference on Software Engineering
    and Formal Methods'
date_created: 2023-01-24T09:03:36Z
date_updated: 2023-01-24T09:03:41Z
department:
- _id: '672'
doi: 10.1109/SEFM.2004.1347516
keyword:
- Unified modeling language
- Logic
- Clocks
- Boolean functions
- Application software
- Time factors
- Real time systems
- Formal verification
- Buffer storage
- Software packages
language:
- iso: eng
place: Beijing, China
publication: Proceedings of SEFM´04
publication_identifier:
  isbn:
  - 0-7695-2222-X
publisher: IEEE
status: public
title: Past- and Future-Oriented Time-Bound Temporal Properties with OCL
type: conference
user_id: '5786'
year: '2004'
...