[{"doi":"10.1007/978-3-540-27863-4_13","series_title":"Lecture Notes in Computer Science","language":[{"iso":"eng"}],"date_updated":"2022-10-20T09:26:15Z","intvolume":"      3147","title":"Specification and Formal Verification of Temporal Properties of Production Automation Systems","year":"2004","author":[{"first_name":"Stephan","last_name":"Flake","full_name":"Flake, Stephan"},{"id":"16243","first_name":"Wolfgang","last_name":"Müller","full_name":"Müller, Wolfgang"},{"last_name":"Pape","first_name":"Ulrich","full_name":"Pape, Ulrich"},{"full_name":"Ruf, Jürgen","first_name":"Jürgen","last_name":"Ruf"}],"publication_identifier":{"isbn":["978-3-540-27863-4"]},"keyword":["Model Check","Temporal Logic","Object Constraint Language","Abstract Syntax","Temporal Logic Formula"],"type":"book_chapter","department":[{"_id":"672"}],"date_created":"2022-10-20T09:25:53Z","abstract":[{"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.","lang":"eng"}],"publication":"Integration of Software Specification Techniques for Applications in Engineering","user_id":"5786","volume":3147,"editor":[{"last_name":"Ehrig","first_name":"Hartmut","full_name":"Ehrig, Hartmut"},{"last_name":"Damm","first_name":"Werner","full_name":"Damm, Werner"},{"first_name":"Jörg","last_name":"Desel","full_name":"Desel, Jörg"},{"first_name":"Martin","last_name":"Große-Rhode","full_name":"Große-Rhode, Martin"},{"full_name":"Reif, Wolfgang","last_name":"Reif","first_name":"Wolfgang"},{"first_name":"Eckehard","last_name":"Schnieder","full_name":"Schnieder, Eckehard"},{"full_name":"Westkämper, Engelbert","last_name":"Westkämper","first_name":"Engelbert"}],"page":"206-226","publisher":"Springer-Verlag","_id":"33825","status":"public","place":"Berlin, Heidelberg","citation":{"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>.","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} }","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>","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.","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>","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.","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>."}}]