Verification of Neural Networks Meets PLC Code: An LHC Cooling Tower Control System at CERN

López Miguel, Ignacio David; Fernández Adiego, Borja; Ghawash, Faiq; Blanco Viñuela, Enrique

doi:10.1007/978-3-031-34204-2_35

Record link:

http://hdl.handle.net/20.500.12708/193480
https://doi.org/10.34726/5420

Title:

Verification of Neural Networks Meets PLC Code: An LHC Cooling Tower Control System at CERN

Citation:

López Miguel, I. D., Fernández Adiego, B., Ghawash, F., & Blanco Viñuela, E. (2023). Verification of Neural Networks Meets PLC Code: An LHC Cooling Tower Control System at CERN. In L. Iliadis, I. Maglogiannis, S. Alonso, C. Jayne, & E. Pimenidis (Eds.), Engineering Applications of Neural Networks : 24th International Conference, EAAAI/EANN 2023, León, Spain, June 14–17, 2023, Proceedings (pp. 420–432). Springer. https://doi.org/10.34726/5420

reposiTUm DOI:

10.34726/5420

CatalogPlus:

AC17207609

Publisher DOI:

10.1007/978-3-031-34204-2_35

Publication Type:

Inproceedings - Full-Paper Contribution

Language:

English

Authors:

López Miguel, Ignacio David
Fernández Adiego, Borja
Ghawash, Faiq
Blanco Viñuela, Enrique

Organisational Unit:

E191-01 - Forschungsbereich Cyber-Physical Systems
E056-13 - Fachbereich LogiCS

Published in:

Engineering Applications of Neural Networks : 24th International Conference, EAAAI/EANN 2023, León, Spain, June 14–17, 2023, Proceedings

ISBN:

978-3-031-34204-2

Volume:

1826

DOI of the book:

10.1007/978-3-031-34204-2

Date (published):

7-Jun-2023

Event name:

24th International Conference on Engineering Applications of Neural Networks

Event date:

14-Jun-2023 - 17-Jun-2023

Event place:

León, Spain

Number of Pages:

Publisher:

Springer, Cham

Keywords:

Control system; PLCs; Verification of neural networks

Abstract:

In the last few years, control engineers have started to use artificial neural networks (NNs) embedded in advanced feedback control algorithms. Its natural integration into existing controllers, such as programmable logic controllers (PLCs) or close to them, represents a challenge. Besides, the application of these algorithms in critical applications still raises concerns among control engineers due to the lack of safety guarantees. Building trustworthy NNs is still a challenge and their verification is attracting more attention nowadays. This paper discusses the peculiarities of formal verification of NNs controllers running on PLCs. It outlines a set of properties that should be satisfied by a NN that is intended to be deployed in a critical high-availability installation at CERN. It compares different methods to verify this NN and sketches our future research directions to find a safe NN.

Research Areas:

Logic and Computation: 40%
Information Systems Engineering: 30%
Automation and Robotics: 30%

Science Branch:

1020 - Informatik: 50%
2020 - Elektrotechnik, Elektronik, Informationstechnik: 40%
1010 - Mathematik: 10%

License:

In Copyright

Appears in Collections:

Conference Paper