Verification Of Plc Program Using A Generic Intermediate Language (Iml)

Agile and flexible manufacturing system requires flexible and reusable control program in order to meet dynamically changing manufacturing processes. Proper modelling and fast formation of the control logics using graphical and mathematical tools is one of the most important tasks to make the control logic more feasible for rapid product prototyping and flexible manufacturing. The heterogeneity of the PLC types and the agile and flexible nature of the manufacturing industry made the verification of the control logic more significant. The standardization of the IEC 61131-3 design makes it possible to be interoperable among control programs. This research is focused on developing a generic intermediate language which can be easily utilized for interface between PLC and any existing model checking tools. The explanation of IML generation technique and PLC verification process are also described with a simple example using Instruction List, Intermediate Language (IML), and SMV with Computational Tree Logic (CTL).