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