---
_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: '34565'
abstract:
- lang: eng
  text: "The textual Object Constraint Language (OCL) is primarily intended to specify
    restrictions over UML class diagrams, in particular class invariants, operation
    pre-, and postconditions. Based on several improvements in the definition of the
    language concepts in last years, a proposal for a new version of OCL has recently
    been published [43]. That document provides an extensive OCL semantic description
    that constitutes a tight integration into UML. However, OCL still lacks a semantic
    integration of UML Statecharts, although it can already be used to refer to states
    in OCL expressions.\r\n\r\nThis article presents an approach that closes this
    gap and introduces a formal semantics for such integration through a mathematical
    model. It also presents the definition of a temporal OCL extension by means of
    a UML Profile based on the metamodel of the latest OCL proposal. Our OCL extension
    enables modelers to specify behavioral state-oriented real-time constraints. It
    provides an intuitive understanding and readability at application level since
    common OCL syntax and concepts are preserved. A well-defined formal semantics
    is given through the mapping of temporal OCL expressions to temporal logics formulae. "
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. Formal Semantics of Static and Temporal State-Oriented OCL
    Constraints. <i>Journal on Software and System Modeling (SoSyM)</i>. 2003;2(3):164-186.
    doi:<a href="https://doi.org/10.1007/s10270-003-0026-x">10.1007/s10270-003-0026-x</a>
  apa: Flake, S., &#38; Müller, W. (2003). Formal Semantics of Static and Temporal
    State-Oriented OCL Constraints. <i>Journal on Software and System Modeling (SoSyM)</i>,
    <i>2</i>(3), 164–186. <a href="https://doi.org/10.1007/s10270-003-0026-x">https://doi.org/10.1007/s10270-003-0026-x</a>
  bibtex: '@article{Flake_Müller_2003, title={Formal Semantics of Static and Temporal
    State-Oriented OCL Constraints}, volume={2}, DOI={<a href="https://doi.org/10.1007/s10270-003-0026-x">10.1007/s10270-003-0026-x</a>},
    number={3}, journal={Journal on Software and System Modeling (SoSyM)}, publisher={Springer-Verlag},
    author={Flake, Stephan and Müller, Wolfgang}, year={2003}, pages={164–186} }'
  chicago: 'Flake, Stephan, and Wolfgang Müller. “Formal Semantics of Static and Temporal
    State-Oriented OCL Constraints.” <i>Journal on Software and System Modeling (SoSyM)</i>
    2, no. 3 (2003): 164–86. <a href="https://doi.org/10.1007/s10270-003-0026-x">https://doi.org/10.1007/s10270-003-0026-x</a>.'
  ieee: 'S. Flake and W. Müller, “Formal Semantics of Static and Temporal State-Oriented
    OCL Constraints,” <i>Journal on Software and System Modeling (SoSyM)</i>, vol.
    2, no. 3, pp. 164–186, 2003, doi: <a href="https://doi.org/10.1007/s10270-003-0026-x">10.1007/s10270-003-0026-x</a>.'
  mla: Flake, Stephan, and Wolfgang Müller. “Formal Semantics of Static and Temporal
    State-Oriented OCL Constraints.” <i>Journal on Software and System Modeling (SoSyM)</i>,
    vol. 2, no. 3, Springer-Verlag, 2003, pp. 164–86, doi:<a href="https://doi.org/10.1007/s10270-003-0026-x">10.1007/s10270-003-0026-x</a>.
  short: S. Flake, W. Müller, Journal on Software and System Modeling (SoSyM) 2 (2003)
    164–186.
date_created: 2022-12-19T12:26:46Z
date_updated: 2022-12-19T12:27:00Z
department:
- _id: '672'
doi: 10.1007/s10270-003-0026-x
intvolume: '         2'
issue: '3'
keyword:
- Object Constraint Language     UML Statecharts     UML Profile     Real-time constraints     Temporal
  logics
language:
- iso: eng
page: 164-186
publication: Journal on Software and System Modeling (SoSyM)
publisher: Springer-Verlag
status: public
title: Formal Semantics of Static and Temporal State-Oriented OCL Constraints
type: journal_article
user_id: '5786'
volume: 2
year: '2003'
...
---
_id: '39364'
abstract:
- lang: eng
  text: "The textual Object Constraint Language (OCL) is an of-\r\nficial part of
    the Unified Modeling Language (UML). OCL\r\nis primarily used to formulate restrictions
    over UML mod-\r\nels, in particular, invariants and operation pre- and post-\r\nconditions
    in the context of class diagrams. However, OCL\r\nis missing means to specify
    constraints over the dynamic\r\nbehavior of a UML model. We have therefore developed
    a\r\ntemporal extension of OCL that enables modelers to specify\r\nbehavioral
    state-oriented constraints. That work provides\r\nan alternative to the rather
    cryptic temporal logic formulae\r\nthat are commonly used to specify behavioral
    system prop-\r\nerties.\r\nThis article now illustrates that our OCL extension
    al-\r\nlows for specifying all kinds of properties that are regarded\r\nas relevant
    in practice. We present according temporal OCL\r\nexpressions for property specification
    patterns that have\r\nbeen identified in the area of formal specification."
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. Expressing Property Specification Patterns with OCL. In:
    <i>Proceedings of SERP’03</i>. ; 2003.'
  apa: Flake, S., &#38; Müller, W. (2003). Expressing Property Specification Patterns
    with OCL. <i>Proceedings of SERP’03</i>.
  bibtex: '@inproceedings{Flake_Müller_2003, place={Las Vegas, NV}, title={Expressing
    Property Specification Patterns with OCL}, booktitle={Proceedings of SERP’03},
    author={Flake, Stephan and Müller, Wolfgang}, year={2003} }'
  chicago: Flake, Stephan, and Wolfgang Müller. “Expressing Property Specification
    Patterns with OCL.” In <i>Proceedings of SERP’03</i>. Las Vegas, NV, 2003.
  ieee: S. Flake and W. Müller, “Expressing Property Specification Patterns with OCL,”
    2003.
  mla: Flake, Stephan, and Wolfgang Müller. “Expressing Property Specification Patterns
    with OCL.” <i>Proceedings of SERP’03</i>, 2003.
  short: 'S. Flake, W. Müller, in: Proceedings of SERP’03, Las Vegas, NV, 2003.'
date_created: 2023-01-24T09:45:49Z
date_updated: 2023-01-24T09:45:54Z
department:
- _id: '672'
keyword:
- UML
- Object Constraint Language
- Patterns
- Property Specification
language:
- iso: eng
place: Las Vegas, NV
publication: Proceedings of SERP'03
status: public
title: Expressing Property Specification Patterns with OCL
type: conference
user_id: '5786'
year: '2003'
...
---
_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'
...