Formal Methods in PLC Control Demonstrated at a Flexible Manufacturing Line

Abstract

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.