GF_BASYS2002_sept_2002

Frey, G.:
Formal methods in PLC control demonstrated at a flexible manufacturing line.
Proceedings of the 5th IFIP International Conference on Information Technology for Balanced Automation Systems in Manufacturing and Services BASYS2002, Cancun, Mexico, pp. 501-508, Sept. 2002.

This paper presents various formal approaches in the development of logic control algorithms. Programmable Logic Controllers (PLCs) are commonly used in automation and the algorithms running on them tend to be quite complex. This motivates the application of formal approaches to PLC programming. The approaches range from completely formalized design methods on the one end over the verification and validation (V&V) of formally described controllers to V&V of existing algorithms (developed in some industrially used PLC programming language) on the other end. This paper contains an overview and comparison of various design and verification approaches applied to a common example - the model of a flexible manufacturing line - presented at a session organized by the author at the American Control Conference 2002.