Abstract
In this paper we present an approach for the automatic translation of control programs implemented in Instruction List (IL) into a suitable model for verification. This model includes a detailed, generic description of the execution mode of Programmable Logic Controllers (PLCs). The approach is integrated into a tool environment for formal verification.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R. and Dill, D. (1994). A theory of timed automata. Theoretical Computer Science, 126:183–235.
Hanisch, H.-M., Thieme, J., Lüder, A., and Wienhold, O. (1997). Modeling of PLC behavior by means of Timed Net Condition/Event Systems. In IEEE Int. Symposium EFTA’ 97, pages 361–396, Los Angeles, USA.
Heiner, M. and Menzel, T. (1999). Modellierung und Analyse von SPS-Anwenderprogrammen mit Petri-Netzen. In 6. Fachtagung Entwurf komplexer Automatisierungssysteme (EKA’99), volume 1, pages 247–265, Braunschweig, Germany.
IEC1131-3 (1993). Standard IEC 1131: Programmable controllers, Part 3: Programming Languages. IEC Geneva, Switzerland.
Mader, A. and Wupper, H. (1999). Timed automaton models for simple programmable logic controllers. In Proceedings of Euromicro Conference on Real-Time Systems.
Moon, I. (1994). Modeling programmable logic controllers for logic verification. Information And Computation, pages 53–59.
Sreenivas, R. and Krogh, B. (1991). On Condition/Event Systems with discrete state realizations. In Discret Event Dynamic Systems: Theory and Applications 1, pages 209–236, Boston. Kluwer Academic Publishers.
Storr, A. and Kraneis, S. (1997). Restruk-turierung und Reverse-Engineering von SPS-Programmen. In 5. Fachtagung Entwurf komplexer Automatisierungssysteme (EKA’ 97), volume 2, pages 446–461, Braunschweig, Germany.
Treseler, H., Bauer, N., and Kowalewski, S. (2000). Verification of IL programs with an explicit model of their PLC execution. Technical report, http://astwww.chemietechnik.unidortmund.de/~verdict//~verdict/, University of Dortmund.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer Science+Business Media New York
About this chapter
Cite this chapter
Treseler, H., Bauer, N., Kowalewski, S. (2000). Verification of IL Programs with an Explicit Model of their PLC Execution. In: Boel, R., Stremersch, G. (eds) Discrete Event Systems. The Springer International Series in Engineering and Computer Science, vol 569. Springer, Boston, MA. https://doi.org/10.1007/978-1-4615-4493-7_29
Download citation
DOI: https://doi.org/10.1007/978-1-4615-4493-7_29
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4613-7025-3
Online ISBN: 978-1-4615-4493-7
eBook Packages: Springer Book Archive