From Natural Language Requirements to the Verification of Programmable Logic Controllers: Integrating FRET into PLCverif

Ádám, Zsófia; López Miguel, Ignacio David; Mavridou, Anastasia; Pressburger, Thomas; Bęś, Marcin; Blanco Viñuela, Enrique; Katis, Andreas; Tournier, Jean-Charles; Trinh, Khanh V.; Fernández Adiego, Borja

doi:10.1007/978-3-031-33170-1_21

Record link:

http://hdl.handle.net/20.500.12708/192588
https://doi.org/10.34726/5382

Title:

From Natural Language Requirements to the Verification of Programmable Logic Controllers: Integrating FRET into PLCverif

Citation:

Ádám, Z., López Miguel, I. D., Mavridou, A., Pressburger, T., Bęś, M., Blanco Viñuela, E., Katis, A., Tournier, J.-C., Trinh, K. V., & Fernández Adiego, B. (2023). From Natural Language Requirements to the Verification of Programmable Logic Controllers: Integrating FRET into PLCverif. In K. Y. Rozier & S. Chaudhuri (Eds.), NASA Formal Methods : 15th International Symposium, NFM 2023, Houston, TX, USA, May 16–18, 2023, Proceedings (pp. 353–360). Springer. https://doi.org/10.34726/5382

reposiTUm DOI:

10.34726/5382

CatalogPlus:

AC17207570

Publisher DOI:

10.1007/978-3-031-33170-1_21

Publication Type:

Inproceedings - Full-Paper Contribution

Language:

English

Organisational Unit:

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

Published in:

NASA Formal Methods : 15th International Symposium, NFM 2023, Houston, TX, USA, May 16–18, 2023, Proceedings

ISBN:

978-3-031-33170-1

Volume:

13903

DOI of the book:

10.1007/978-3-031-33170-1

Date (published):

3-Jun-2023

Event name:

15th NASA Formal Methods Symposium

Event date:

16-May-2023 - 18-May-2023

Event place:

Houston, Texas, United States of America (the)

Number of Pages:

Publisher:

Springer, Cham

Keywords:

PLCverif; FRET; PLC; Formal verification; Specification

Abstract:

PLCverif is an actively developed project at CERN, enabling the formal verification of Programmable Logic Controller (PLC) programs in critical systems. In this paper, we present our work on improving the formal requirements specification experience in PLCverif through the use of natural language. To this end, we integrate NASA’s FRET, a formal requirement elicitation and authoring tool, into PLCverif. FRET is used to specify formal requirements in structured natural language, which automatically translates into temporal logic formulae. FRET’s output is then directly used by PLCverif for verification purposes. We discuss practical challenges that PLCverif users face when authoring requirements and the FRET features that help alleviate these problems. We present the new requirement formalization workflow and report our experience using it on two critical CERN case studies.

Research Areas:

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

Science Branch:

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

License:

In Copyright

Appears in Collections:

Conference Paper