---
_id: '33825'
abstract:
- lang: eng
  text: This article describes our approach for the specification and verification
    of production automation systems with real-time properties. We focus on the graphical
    MFERT notation and RT-OCL (Real-Time Object Constraint Language) for the specification
    of state-oriented real-time properties. RT-OCL is an extension of the Object Constraint
    Language (OCL) that is part of the Unified Modeling Language (UML). We introduce
    the formal semantics of RT-OCL based on a formal model of UML Class and State
    Diagrams and provide a mapping to temporal logics. The applicability of our approach
    is demonstrated by the case study of a manufacturing system with automated guided
    vehicles.
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
- first_name: Ulrich
  full_name: Pape, Ulrich
  last_name: Pape
- first_name: Jürgen
  full_name: Ruf, Jürgen
  last_name: Ruf
citation:
  ama: 'Flake S, Müller W, Pape U, Ruf J. Specification and Formal Verification of
    Temporal Properties of Production Automation Systems. In: Ehrig H, Damm W, Desel
    J, et al., eds. <i>Integration of Software Specification Techniques for Applications
    in Engineering</i>. Vol 3147. Lecture Notes in Computer Science. Springer-Verlag;
    2004:206-226. doi:<a href="https://doi.org/10.1007/978-3-540-27863-4_13">10.1007/978-3-540-27863-4_13</a>'
  apa: Flake, S., Müller, W., Pape, U., &#38; Ruf, J. (2004). Specification and Formal
    Verification of Temporal Properties of Production Automation Systems. In H. Ehrig,
    W. Damm, J. Desel, M. Große-Rhode, W. Reif, E. Schnieder, &#38; E. Westkämper
    (Eds.), <i>Integration of Software Specification Techniques for Applications in
    Engineering</i> (Vol. 3147, pp. 206–226). Springer-Verlag. <a href="https://doi.org/10.1007/978-3-540-27863-4_13">https://doi.org/10.1007/978-3-540-27863-4_13</a>
  bibtex: '@inbook{Flake_Müller_Pape_Ruf_2004, place={Berlin, Heidelberg}, series={Lecture
    Notes in Computer Science}, title={Specification and Formal Verification of Temporal
    Properties of Production Automation Systems}, volume={3147}, DOI={<a href="https://doi.org/10.1007/978-3-540-27863-4_13">10.1007/978-3-540-27863-4_13</a>},
    booktitle={Integration of Software Specification Techniques for Applications in
    Engineering}, publisher={Springer-Verlag}, author={Flake, Stephan and Müller,
    Wolfgang and Pape, Ulrich and Ruf, Jürgen}, editor={Ehrig, Hartmut and Damm, Werner
    and Desel, Jörg and Große-Rhode, Martin and Reif, Wolfgang and Schnieder, Eckehard
    and Westkämper, Engelbert}, year={2004}, pages={206–226}, collection={Lecture
    Notes in Computer Science} }'
  chicago: 'Flake, Stephan, Wolfgang Müller, Ulrich Pape, and Jürgen Ruf. “Specification
    and Formal Verification of Temporal Properties of Production Automation Systems.”
    In <i>Integration of Software Specification Techniques for Applications in Engineering</i>,
    edited by Hartmut Ehrig, Werner Damm, Jörg Desel, Martin Große-Rhode, Wolfgang
    Reif, Eckehard Schnieder, and Engelbert Westkämper, 3147:206–26. Lecture Notes
    in Computer Science. Berlin, Heidelberg: Springer-Verlag, 2004. <a href="https://doi.org/10.1007/978-3-540-27863-4_13">https://doi.org/10.1007/978-3-540-27863-4_13</a>.'
  ieee: 'S. Flake, W. Müller, U. Pape, and J. Ruf, “Specification and Formal Verification
    of Temporal Properties of Production Automation Systems,” in <i>Integration of
    Software Specification Techniques for Applications in Engineering</i>, vol. 3147,
    H. Ehrig, W. Damm, J. Desel, M. Große-Rhode, W. Reif, E. Schnieder, and E. Westkämper,
    Eds. Berlin, Heidelberg: Springer-Verlag, 2004, pp. 206–226.'
  mla: Flake, Stephan, et al. “Specification and Formal Verification of Temporal Properties
    of Production Automation Systems.” <i>Integration of Software Specification Techniques
    for Applications in Engineering</i>, edited by Hartmut Ehrig et al., vol. 3147,
    Springer-Verlag, 2004, pp. 206–26, doi:<a href="https://doi.org/10.1007/978-3-540-27863-4_13">10.1007/978-3-540-27863-4_13</a>.
  short: 'S. Flake, W. Müller, U. Pape, J. Ruf, in: H. Ehrig, W. Damm, J. Desel, M.
    Große-Rhode, W. Reif, E. Schnieder, E. Westkämper (Eds.), Integration of Software
    Specification Techniques for Applications in Engineering, Springer-Verlag, Berlin,
    Heidelberg, 2004, pp. 206–226.'
date_created: 2022-10-20T09:25:53Z
date_updated: 2022-10-20T09:26:15Z
department:
- _id: '672'
doi: 10.1007/978-3-540-27863-4_13
editor:
- first_name: Hartmut
  full_name: Ehrig, Hartmut
  last_name: Ehrig
- first_name: Werner
  full_name: Damm, Werner
  last_name: Damm
- first_name: Jörg
  full_name: Desel, Jörg
  last_name: Desel
- first_name: Martin
  full_name: Große-Rhode, Martin
  last_name: Große-Rhode
- first_name: Wolfgang
  full_name: Reif, Wolfgang
  last_name: Reif
- first_name: Eckehard
  full_name: Schnieder, Eckehard
  last_name: Schnieder
- first_name: Engelbert
  full_name: Westkämper, Engelbert
  last_name: Westkämper
intvolume: '      3147'
keyword:
- Model Check
- Temporal Logic
- Object Constraint Language
- Abstract Syntax
- Temporal Logic Formula
language:
- iso: eng
page: 206-226
place: Berlin, Heidelberg
publication: Integration of Software Specification Techniques for Applications in
  Engineering
publication_identifier:
  isbn:
  - 978-3-540-27863-4
publisher: Springer-Verlag
series_title: Lecture Notes in Computer Science
status: public
title: Specification and Formal Verification of Temporal Properties of Production
  Automation Systems
type: book_chapter
user_id: '5786'
volume: 3147
year: '2004'
...
---
_id: '34447'
abstract:
- lang: eng
  text: "The Object Constraint Language (OCL) was introduced to support the specification
    of constraints for UML diagrams and is mainly used to formulate invariants and
    operation pre- and postconditions. Though OCL is also applied in behavioral diagrams,
    e.g., as guards for state transitions, it is currently not possible to specify
    constraints concerning the dynamic behavior and timing properties of such diagrams.\r\n\r\nThis
    article discusses OCL’s application for the dynamic behavior of UML Statechart
    diagrams and presents an OCL extension for specification of state-oriented time-bounded
    constraints.We introduce operations to extract state configurations from diagrams
    and define additional predicates over states and state configurations. The semantics
    of our OCL extension is given by employing time-bounded Computational Tree Logic
    (CTL) formulae. An example of a flexible manufacturing system with automated guided
    vehicles demonstrates the application of our extension."
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. An OCL Extension for Real-Time Constraints. In: Clark T,
    Warmer J, eds. <i>Advances in Object Modelling with the OCL</i>. Springer-Verlag;
    2002:150-171. doi:<a href="https://doi.org/10.1007/3-540-45669-4_8">10.1007/3-540-45669-4_8</a>'
  apa: Flake, S., &#38; Müller, W. (2002). An OCL Extension for Real-Time Constraints.
    In T. Clark &#38; J. Warmer (Eds.), <i>Advances in Object Modelling with the OCL</i>
    (pp. 150–171). Springer-Verlag. <a href="https://doi.org/10.1007/3-540-45669-4_8">https://doi.org/10.1007/3-540-45669-4_8</a>
  bibtex: '@inbook{Flake_Müller_2002, place={Berlin, Heidelberg}, title={An OCL Extension
    for Real-Time Constraints}, DOI={<a href="https://doi.org/10.1007/3-540-45669-4_8">10.1007/3-540-45669-4_8</a>},
    booktitle={Advances in Object Modelling with the OCL}, publisher={Springer-Verlag},
    author={Flake, Stephan and Müller, Wolfgang}, editor={Clark, T. and Warmer, J.},
    year={2002}, pages={150–171} }'
  chicago: 'Flake, Stephan, and Wolfgang Müller. “An OCL Extension for Real-Time Constraints.”
    In <i>Advances in Object Modelling with the OCL</i>, edited by T. Clark and J.
    Warmer, 150–71. Berlin, Heidelberg: Springer-Verlag, 2002. <a href="https://doi.org/10.1007/3-540-45669-4_8">https://doi.org/10.1007/3-540-45669-4_8</a>.'
  ieee: 'S. Flake and W. Müller, “An OCL Extension for Real-Time Constraints,” in
    <i>Advances in Object Modelling with the OCL</i>, T. Clark and J. Warmer, Eds.
    Berlin, Heidelberg: Springer-Verlag, 2002, pp. 150–171.'
  mla: Flake, Stephan, and Wolfgang Müller. “An OCL Extension for Real-Time Constraints.”
    <i>Advances in Object Modelling with the OCL</i>, edited by T. Clark and J. Warmer,
    Springer-Verlag, 2002, pp. 150–71, doi:<a href="https://doi.org/10.1007/3-540-45669-4_8">10.1007/3-540-45669-4_8</a>.
  short: 'S. Flake, W. Müller, in: T. Clark, J. Warmer (Eds.), Advances in Object
    Modelling with the OCL, Springer-Verlag, Berlin, Heidelberg, 2002, pp. 150–171.'
date_created: 2022-12-15T11:38:20Z
date_updated: 2022-12-15T11:38:47Z
department:
- _id: '672'
doi: 10.1007/3-540-45669-4_8
editor:
- first_name: T.
  full_name: Clark, T.
  last_name: Clark
- first_name: J.
  full_name: Warmer, J.
  last_name: Warmer
keyword:
- Model Check     Temporal Logic     Object Constraint Language     Execution Path     Kripke
  Structure
language:
- iso: eng
page: 150 - 171
place: Berlin, Heidelberg
publication: Advances in Object Modelling with the OCL
publication_identifier:
  isbn:
  - 978-3-540-45669-8
publisher: Springer-Verlag
status: public
title: An OCL Extension for Real-Time Constraints
type: book_chapter
user_id: '5786'
year: '2002'
...