In this contribution 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 [1] with an already written control program [2]. 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 is then given.
展开▼
