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

被引：1

作者：

Adam, Zsofia ^{[1
,6
]}

Lopez-Miguel, Ignacio D. ^{[3
,6
]}

Mavridou, Anastasia ^{[4
]}

Pressburger, Thomas ^{[5
]}

Bes, Marcin ^{[2
]}

Vinuela, Enrique Blanco ^{[2
]}

Katis, Andreas ^{[4
]}

Tournier, Jean-Charles ^{[2
]}

Trinh, Khanh, V ^{[4
]}

Adiego, Borja Fernandez ^{[2
]}

机构：

[1] Budapest Univ Technol & Econ, Dept Measurement & Informat Syst, Budapest, Hungary

[2] European Org Nucl Res CERN, Geneva, Switzerland

[3] TU Wien, Vienna, Austria

[4] NASA, Ames Res Ctr, KBR, Moffett Field, CA 94035 USA

[5] NASA, Ames Res Ctr, Moffett Field, CA 94035 USA

[6] CERN, Geneva, Switzerland

来源：

NASA FORMAL METHODS, NFM 2023 | 2023年 / 13903卷

关键词：

D O I：

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

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

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.

引用

页码：353 / 360

页数：8

共 14 条

[1] Adam Z., 2023, Technical report NASA/TM 0230003752
[2] Applying Model Checking to Industrial-Sized PLC Programs
Adiego, Borja Fernandez
Darvas, Daniel
Vinuela, Enrique Blanco
Tournier, Jean-Charles
Bliudze, Simon
Blech, Jan Olaf
Gonzalez Suarez, Victor Manuel
[J]. IEEE TRANSACTIONS ON INDUSTRIAL INFORMATICS, 2015, 11 (06) : 1400 - 1410
[3] The software model checker BlastApplications to software engineering
Dirk Beyer
Thomas A. Henzinger
Ranjit Jhala
Rupak Majumdar
[J]. International Journal on Software Tools for Technology Transfer, 2007, 9 (5-6) : 505 - 525
[4] Darvas D., 2015, P ICALEPCS 2015 OCT, DOI [10.18429/JACoWICALEPCS2015-WEPGF092, DOI 10.18429/JACOWICALEPCS2015-WEPGF092]
[5] Fernandez Adiego B., 2022, P ICALEPCS 2021, DOI [10.18429/JACoW-ICALEPCS2021-WEPV042, DOI 10.18429/JACOW-ICALEPCS2021-WEPV042]
[6] Fernandez Adiego B., 2017, P ICALEPCS 2017 OCT, DOI [10.18429/JACoWICALEPCS2017-THPHA161, DOI 10.18429/JACOWICALEPCS2017-THPHA161]
[7] FRET, Formal requirements elicitation tool
[8] Giannakopoulou D., 2020, REFSQ Tools
[9] Automated formalization of structured natural language requirements
Giannakopoulou, Dimitra
Pressburger, Thomas
Mavridou, Anastasia
Schumann, Johann
[J]. INFORMATION AND SOFTWARE TECHNOLOGY, 2021, 137
[10] home, High luminosity large hadron collider webpage

← 1 2 →