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

Datensatz Zitierlink:

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

Titel:

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

Zitat:

Á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

Verlags-DOI:

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

Publikationstyp:

Konferenzbeitrag - Full-Paper Contribution

Sprache:

Englisch

Organisationseinheit:

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

Erschienen in:

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

ISBN:

978-3-031-33170-1

Band:

13903

DOI des Buches:

10.1007/978-3-031-33170-1

Datum (veröffentlicht):

3-Jun-2023

Veranstaltungsname:

15th NASA Formal Methods Symposium

Veranstaltungszeitraum:

16-Mai-2023 - 18-Mai-2023

Veranstaltungsort:

Houston, Texas, Vereinigte Staaten von Amerika

Umfang:

Verlag:

Springer, Cham

Peer Reviewed:

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.

Forschungsschwerpunkte:

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

Wissenschaftszweig:

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

Lizenz:

Urheberrechtsschutz

Enthalten in den Sammlungen:

Conference Paper