<div class="csl-bib-body">
<div class="csl-entry">Á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.), <i>NASA Formal Methods : 15th International Symposium, NFM 2023, Houston, TX, USA, May 16–18, 2023, Proceedings</i> (pp. 353–360). Springer. https://doi.org/10.34726/5382</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/192588
-
dc.identifier.uri
https://doi.org/10.34726/5382
-
dc.description.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.
en
dc.language.iso
en
-
dc.relation.ispartofseries
Lecture Notes in Computer Science
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
PLCverif
en
dc.subject
FRET
en
dc.subject
PLC
en
dc.subject
Formal verification
en
dc.subject
Specification
en
dc.title
From Natural Language Requirements to the Verification of Programmable Logic Controllers: Integrating FRET into PLCverif
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Urheberrechtsschutz
de
dc.rights.license
In Copyright
en
dc.identifier.doi
10.34726/5382
-
dc.contributor.affiliation
Budapest University of Technology and Economics, Hungary
-
dc.contributor.affiliation
Ames Research Center, United States of America (the)
-
dc.contributor.affiliation
Ames Research Center, United States of America (the)
-
dc.contributor.affiliation
European Organization for Nuclear Research, Switzerland
-
dc.contributor.affiliation
European Organization for Nuclear Research, Switzerland
-
dc.contributor.affiliation
Ames Research Center, United States of America (the)
-
dc.contributor.affiliation
European Organization for Nuclear Research, Switzerland
-
dc.contributor.affiliation
Ames Research Center, United States of America (the)
-
dc.contributor.affiliation
European Organization for Nuclear Research, Switzerland
-
dc.relation.isbn
978-3-031-33170-1
-
dc.relation.doi
10.1007/978-3-031-33170-1
-
dc.relation.issn
0302-9743
-
dc.description.startpage
353
-
dc.description.endpage
360
-
dc.rights.holder
The Editor(s) (if applicable) and The Author(s), under exclusive license to Springer Nature Switzerland AG 2023
-
dc.type.category
Full-Paper Contribution
-
dc.relation.eissn
1611-3349
-
tuw.booktitle
NASA Formal Methods : 15th International Symposium, NFM 2023, Houston, TX, USA, May 16–18, 2023, Proceedings
-
tuw.container.volume
13903
-
tuw.book.ispartofseries
Lecture Notes in Computer Science
-
tuw.relation.publisher
Springer
-
tuw.relation.publisherplace
Cham
-
tuw.researchTopic.id
I1
-
tuw.researchTopic.id
I4
-
tuw.researchTopic.id
I3
-
tuw.researchTopic.name
Logic and Computation
-
tuw.researchTopic.name
Information Systems Engineering
-
tuw.researchTopic.name
Automation and Robotics
-
tuw.researchTopic.value
20
-
tuw.researchTopic.value
40
-
tuw.researchTopic.value
40
-
tuw.publication.orgunit
E191-01 - Forschungsbereich Cyber-Physical Systems
-
tuw.publication.orgunit
E056-13 - Fachbereich LogiCS
-
tuw.publisher.doi
10.1007/978-3-031-33170-1_21
-
dc.identifier.libraryid
AC17207570
-
dc.description.numberOfPages
8
-
tuw.author.orcid
0000-0003-2354-1750
-
tuw.author.orcid
0000-0002-8044-0385
-
tuw.author.orcid
0000-0002-3943-9753
-
tuw.author.orcid
0000-0001-7013-1100
-
dc.rights.identifier
Urheberrechtsschutz
de
dc.rights.identifier
In Copyright
en
tuw.editor.orcid
0000-0002-6718-2828
-
tuw.event.name
15th NASA Formal Methods Symposium
en
tuw.event.startdate
16-05-2023
-
tuw.event.enddate
18-05-2023
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Houston, Texas
-
tuw.event.country
US
-
tuw.event.presenter
Lopez-Miguel, Ignacio D.
-
tuw.event.presenter
Katis, Andreas
-
tuw.event.presenter
Fernández Adiego, Borja
-
wb.sciencebranch
Informatik
-
wb.sciencebranch
Elektrotechnik, Elektronik, Informationstechnik
-
wb.sciencebranch
Mathematik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.oefos
2020
-
wb.sciencebranch.oefos
1010
-
wb.sciencebranch.value
50
-
wb.sciencebranch.value
40
-
wb.sciencebranch.value
10
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.openairetype
conference paper
-
item.cerifentitytype
Publications
-
item.fulltext
with Fulltext
-
item.openaccessfulltext
Open Access
-
item.languageiso639-1
en
-
item.mimetype
application/pdf
-
item.grantfulltext
open
-
crisitem.author.dept
Budapest University of Technology and Economics, Hungary
-
crisitem.author.dept
E191-01 - Forschungsbereich Cyber-Physical Systems