The Joint Accelerator Conferences Website (JACoW) is an international collaboration that publishes the proceedings of accelerator conferences held around the world.
TY - CONF AU - Blanco Viñuela, E. AU - Darvas, D. AU - Molnár, V. ED - White, Karen S. ED - Brown, Kevin A. ED - Dyer, Philip S. ED - Schaa, Volker RW TI - PLCverif Re-engineered: An Open Platform for the Formal Analysis of PLC Programs J2 - Proc. of ICALEPCS2019, New York, NY, USA, 05-11 October 2019 CY - New York, NY, USA T2 - International Conference on Accelerator and Large Experimental Physics Control Systems T3 - 17 LA - english AB - Programmable Logic Controllers (PLC) are widely used for industrial automation in industry and at CERN. The reliability of PLC software is crucial, but typically only testing is used to validate it. Our work targets the use of formal verification in practical ways for many years, which showed that it can be beneficial and practically applicable to various PLC programs. In this paper, we present PLCverif, our platform for formal analysis of PLC programs which has largely enhanced the quality of the deployed PLC software. By re-engineering the previous internal prototype tool, we built PLCverif to be an open, extensible platform that can be used not only for CERN’s specific PLC programs. PLCverif is licensed under an open source license, allowing the interested parties to use and extend it. PB - JACoW Publishing CP - Geneva, Switzerland SP - 21 EP - 27 KW - PLC KW - controls KW - software KW - target KW - interface DA - 2020/08 PY - 2020 SN - 2226-0358 SN - 978-3-95450-209-7 DO - doi:10.18429/JACoW-ICALEPCS2019-MOBPP01 UR - https://jacow.org/icalepcs2019/papers/mobpp01.pdf ER -