---
res:
  bibo_abstract:
  - 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.@eng
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Stephan
      foaf_name: Flake, Stephan
      foaf_surname: Flake
  - foaf_Person:
      foaf_givenName: Wolfgang
      foaf_name: Müller, Wolfgang
      foaf_surname: Müller
      foaf_workInfoHomepage: http://www.librecat.org/personId=16243
  - foaf_Person:
      foaf_givenName: Ulrich
      foaf_name: Pape, Ulrich
      foaf_surname: Pape
  - foaf_Person:
      foaf_givenName: Jürgen
      foaf_name: Ruf, Jürgen
      foaf_surname: Ruf
  bibo_doi: 10.1007/978-3-540-27863-4_13
  bibo_volume: 3147
  dct_date: 2004^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/978-3-540-27863-4
  dct_language: eng
  dct_publisher: Springer-Verlag@
  dct_subject:
  - Model Check
  - Temporal Logic
  - Object Constraint Language
  - Abstract Syntax
  - Temporal Logic Formula
  dct_title: Specification and Formal Verification of Temporal Properties of Production
    Automation Systems@
...