Specification and Formal Verification of Temporal Properties of Production Automation Systems
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.
Download
No fulltext has been uploaded.
Book Chapter
| English
Author
Flake, Stephan;
Müller, WolfgangLibreCat;
Pape, Ulrich;
Ruf, Jürgen
Book Editor
Ehrig, Hartmut;
Damm, Werner;
Desel, Jörg;
Große-Rhode, Martin;
Reif, Wolfgang;
Schnieder, Eckehard;
Westkämper, Engelbert
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.
Keywords
Publishing Year
Book Title
Integration of Software Specification Techniques for Applications in Engineering
Series Title / Volume
Lecture Notes in Computer Science
Volume
3147
Page
206-226
ISBN
LibreCat-ID
Cite this
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. Integration of Software Specification Techniques for Applications in Engineering. Vol 3147. Lecture Notes in Computer Science. Springer-Verlag; 2004:206-226. doi:10.1007/978-3-540-27863-4_13
Flake, S., Müller, W., Pape, U., & 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, & E. Westkämper (Eds.), Integration of Software Specification Techniques for Applications in Engineering (Vol. 3147, pp. 206–226). Springer-Verlag. https://doi.org/10.1007/978-3-540-27863-4_13
@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={10.1007/978-3-540-27863-4_13}, 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, Stephan, Wolfgang Müller, Ulrich Pape, and Jürgen Ruf. “Specification and Formal Verification of Temporal Properties of Production Automation Systems.” In Integration of Software Specification Techniques for Applications in Engineering, 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. https://doi.org/10.1007/978-3-540-27863-4_13.
S. Flake, W. Müller, U. Pape, and J. Ruf, “Specification and Formal Verification of Temporal Properties of Production Automation Systems,” in Integration of Software Specification Techniques for Applications in Engineering, 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.
Flake, Stephan, et al. “Specification and Formal Verification of Temporal Properties of Production Automation Systems.” Integration of Software Specification Techniques for Applications in Engineering, edited by Hartmut Ehrig et al., vol. 3147, Springer-Verlag, 2004, pp. 206–26, doi:10.1007/978-3-540-27863-4_13.
Google Scholar
ISBN Search