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/).
Cite this article
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 -