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

DOI

10.2991/icismme-15.2015.288How to use a DOI?

Keywords

Event-B modeling; formal method; 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.

Copyright

© 2015, the Authors. Published by Atlantis Press.

Open Access

This is an open access article distributed under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).

Download article (PDF)

TY  - CONF
AU  - He Zhao
AU  - Bin Fang
AU  - Hui-jie Li
AU  - Pu Wang
PY  - 2015/07
DA  - 2015/07
TI  - Research on Event-B based modelling and verification of PLC system
BT  - Proceedings of the First International Conference on Information Sciences, Machinery, Materials and Energy
PB  - Atlantis Press
SP  - 1340
EP  - 1346
SN  - 1951-6851
UR  - https://doi.org/10.2991/icismme-15.2015.288
DO  - 10.2991/icismme-15.2015.288
ID  - Zhao2015/07
ER  -