book chapter Stephan Flake author Wolfgang Müller author 16243 Ulrich Pape author Jürgen Ruf author HartmutEhrig editor WernerDamm editor JörgDesel editor MartinGroße-Rhode editor WolfgangReif editor EckehardSchnieder editor EngelbertWestkämper editor 672 department 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. Springer-Verlag2004 eng Model CheckTemporal LogicObject Constraint LanguageAbstract SyntaxTemporal Logic Formula 978-3-540-27863-410.1007/978-3-540-27863-4_13 3147206-226 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>. 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> @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} } 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> 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. 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. 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>. 338252022-10-20T09:25:53Z2022-10-20T09:26:15Z