Research on Event-B based modelling and verification of PLC system

Abstract. In order to ensure the safety of equipment and persons, the rigorous requirements on the correctness and reliability of control program are always needed in industrial control system. The traditional program design methods are based on the realization of the functions and verified by the simulations and tests. Errors can only be founded during the simulation and test phase. And some vital errors cannot be tested, because these errors may cause damages to the equipment and persons. So the correctness and reliability of control program cannot be ensured. For these problems, the formal design methods emerged as the times require. The errors can be found in design level by the formalized-model. In other word, formal methods could detect the errors earlier, reduce the cost of development, and are suitable for the occasions that require rigorous requirements on the correctness and reliability. This paper discussed a kind of Event-B based formal method, using Rodin Platform, to model, refine and verify the automated production line control system