@inbook{33825,
  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.}},
  author       = {{Flake, Stephan and Müller, Wolfgang and Pape, Ulrich and Ruf, Jürgen}},
  booktitle    = {{Integration of Software Specification Techniques for Applications in Engineering}},
  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}},
  isbn         = {{978-3-540-27863-4}},
  keywords     = {{Model Check, Temporal Logic, Object Constraint Language, Abstract Syntax, Temporal Logic Formula}},
  pages        = {{206--226}},
  publisher    = {{Springer-Verlag}},
  title        = {{{Specification and Formal Verification of Temporal Properties of Production Automation Systems}}},
  doi          = {{10.1007/978-3-540-27863-4_13}},
  volume       = {{3147}},
  year         = {{2004}},
}

@article{34565,
  abstract     = {{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.

This 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       = {{Flake, Stephan and Müller, Wolfgang}},
  journal      = {{Journal on Software and System Modeling (SoSyM)}},
  keywords     = {{Object Constraint Language     UML Statecharts     UML Profile     Real-time constraints     Temporal logics}},
  number       = {{3}},
  pages        = {{164--186}},
  publisher    = {{Springer-Verlag}},
  title        = {{{Formal Semantics of Static and Temporal State-Oriented OCL Constraints}}},
  doi          = {{10.1007/s10270-003-0026-x}},
  volume       = {{2}},
  year         = {{2003}},
}

@inproceedings{39364,
  abstract     = {{The textual Object Constraint Language (OCL) is an of-
ficial part of the Unified Modeling Language (UML). OCL
is primarily used to formulate restrictions over UML mod-
els, in particular, invariants and operation pre- and post-
conditions in the context of class diagrams. However, OCL
is missing means to specify constraints over the dynamic
behavior of a UML model. We have therefore developed a
temporal extension of OCL that enables modelers to specify
behavioral state-oriented constraints. That work provides
an alternative to the rather cryptic temporal logic formulae
that are commonly used to specify behavioral system prop-
erties.
This article now illustrates that our OCL extension al-
lows for specifying all kinds of properties that are regarded
as relevant in practice. We present according temporal OCL
expressions for property specification patterns that have
been identified in the area of formal specification.}},
  author       = {{Flake, Stephan and Müller, Wolfgang}},
  booktitle    = {{Proceedings of SERP'03}},
  keywords     = {{UML, Object Constraint Language, Patterns, Property Specification}},
  title        = {{{Expressing Property Specification Patterns with OCL}}},
  year         = {{2003}},
}

@inbook{34447,
  abstract     = {{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.

This 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       = {{Flake, Stephan and Müller, Wolfgang}},
  booktitle    = {{Advances in Object Modelling with the OCL}},
  editor       = {{Clark, T. and Warmer, J.}},
  isbn         = {{978-3-540-45669-8}},
  keywords     = {{Model Check     Temporal Logic     Object Constraint Language     Execution Path     Kripke Structure}},
  pages        = {{150 -- 171}},
  publisher    = {{Springer-Verlag}},
  title        = {{{An OCL Extension for Real-Time Constraints}}},
  doi          = {{10.1007/3-540-45669-4_8}},
  year         = {{2002}},
}