Verification of a controller for a flexible manufacturing line written in Ladder Diagram via model-checking

In this paper a machining line testbed is used as a case study to assess the interest of performing formal validation on the implementation program of the control with standard PLC programming language. We choose to use well-known PLC language with an already written control program. In this situation, we can perform validation in a separate step after implementation. We express formal properties to be checked by the model of the controller. Conclusions about the controller are then given.