JACoW logo

Journals of Accelerator Conferences Website (JACoW)

JACoW is a publisher in Geneva, Switzerland that publishes the proceedings of accelerator conferences held around the world by an international collaboration of editors.

RIS citation export for MOPV042: PLCverif: Status of a Formal Verification Tool for Programmable Logic Controller

AU  - Tournier, J-C.
AU  - Fernández Adiego, B.
AU  - Lopez-Miguel, I.D.
ED  - Furukawa, Kazuro
ED  - Yan, Yingbing
ED  - Leng, Yongbin
ED  - Chen, Zhichu
ED  - Schaa, Volker R.W.
TI  - PLCverif: Status of a Formal Verification Tool for Programmable Logic Controller
J2  - Proc. of ICALEPCS2021, Shanghai, China, 14-22 October 2021
CY  - Shanghai, China
T2  - International Conference on Accelerator and Large Experimental Physics Control Systems
T3  - 18
LA  - english
AB  - Programmable Logic Controllers (PLC) are widely used for industrial automation including safety systems at CERN. The incorrect behaviour of the PLC control system logic can cause significant financial losses by damage of property or the environment or even injuries in some cases, therefore ensuring their correct behaviour is essential. While testing has been for many years the traditional way of validating the PLC control system logic, CERN developed a model checking platform to go one step further and formally verify PLC logic. This platform, called PLCverif, first released internally for CERN usage in 2019, is now available to anyone since September 2020 via an open source licence. In this paper, we will first give an overview of the PLCverif platform capabilities before focusing on the improvements done since 2019 such as the larger support coverage of the Siemens PLC programming languages, the better support of the C Bounded Model Checker backend (CBMC) and the process of releasing PLCverif as an open-source software.
PB  - JACoW Publishing
CP  - Geneva, Switzerland
SP  - 248
EP  - 252
KW  - controls
KW  - software
KW  - focusing
DA  - 2022/03
PY  - 2022
SN  - 2226-0358
SN  - 978-3-95450-221-9
DO  - doi:10.18429/JACoW-ICALEPCS2021-MOPV042
UR  - https://jacow.org/icalepcs2021/papers/mopv042.pdf
ER  -