Safety verification of programmable logic controller taking into account the physical dynamics - application to material handling robots

PLC (programmable logic controller) has been widely used in the industrial world as a controller for the manufacturing system, process control and so on. The conventional PLC has been designed and verified as a pure discrete event system (DES) by using the abstract model of the controlled plant. In verifying PLC, however, it is also important to take into account the physical behavior of the controlled plant in order to guarantee some important properties such as safety. This paper presents a new verification technique for the PLC-based control system, which is based on the hybrid system framework. The key idea is the introduction of signed distance, which not only measure the distance between two objects but also check whether two objects interfere with each other. The developed idea is applied to illustrative material handling problem, and its usefulness is demonstrated.