---
_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'
...