Formal Verification of the Control Software of a Radioactive Material Remote Handling System, Based on IEC 61499

Giordano Lilli; Midhun Xavier; Etienne Le Priol; Vincent Perret; Tatiana Liakh; Roberto Oboe; Valeriy Vyatkin

doi:10.1109/OJIES.2023.3321084

Formal Verification of the Control Software of a Radioactive Material Remote Handling System, Based on IEC 61499

Giordano Lilli^*, Midhun Xavier, Etienne Le Priol, Vincent Perret, Tatiana Liakh, Roberto Oboe, Valeriy Vyatkin

^*Corresponding author for this work

Research output: Contribution to journal › Article › Scientific › peer-review

23 Downloads (Pure)

Abstract

Automation systems within nuclear laboratories are intended to work under harsh operating conditions. Selective Production of Exotic Species (SPES) is a nuclear research facility currently under construction by the Istituto Nazionale di Fisica Nucleare, dedicated to the production and study of radioactive ion beams. Isotopes are produced within the target ion source unit, a vacuum vessel that must be replaced on a regular basis. The highly radioactive environment necessitates the deployment of a set of automated systems dedicated to the unit's remote management. To meet high-level security standards, the design of such instrumentation and control systems must include extensive verification. Based on specific safety requirements, model checking can be used to assess the systems' correctness. This article describes how to employ an integrated toolchain to design, simulate, formally verify, and deploy the control software for the Horizontal Handling Machine, a safety-critical remote handling system in operation at SPES. The IEC 61499 standard's adoption led to a redesign of the control logic. Following a preliminary online simulation, the closed-loop system has been formally verified using the NuSMV symbolic model checker, with the help of the FB2SMV converter. In addition, the Function Blocks Modeling Environment tool was used for automating verification and analyzing counterexamples.

Original language	English
Pages (from-to)	417-431
Number of pages	15
Journal	IEEE Open Journal of the Industrial Electronics Society
Volume	4
DOIs	https://doi.org/10.1109/OJIES.2023.3321084
Publication status	Published - 16 Oct 2023
MoE publication type	A1 Journal article-refereed

Keywords

Formal verification
IEC 61499
isotope separation online (ISOL)
model checking
NuSMV
radioactive ion beams (RIBs)
remote handling
Selective Production of Exotic Species (SPES)
simulation

Access to Document

10.1109/OJIES.2023.3321084Licence: CC BY

Formal_Verification_of_the_Control_Software_of_a_Radioactive_Material_Remote_Handling_System_Based_on_IEC_61499Final published version, 11.1 MBLicence: CC BY

Cite this

@article{0c503f31d289400ba473f996e8980533,

title = "Formal Verification of the Control Software of a Radioactive Material Remote Handling System, Based on IEC 61499",

abstract = "Automation systems within nuclear laboratories are intended to work under harsh operating conditions. Selective Production of Exotic Species (SPES) is a nuclear research facility currently under construction by the Istituto Nazionale di Fisica Nucleare, dedicated to the production and study of radioactive ion beams. Isotopes are produced within the target ion source unit, a vacuum vessel that must be replaced on a regular basis. The highly radioactive environment necessitates the deployment of a set of automated systems dedicated to the unit's remote management. To meet high-level security standards, the design of such instrumentation and control systems must include extensive verification. Based on specific safety requirements, model checking can be used to assess the systems' correctness. This article describes how to employ an integrated toolchain to design, simulate, formally verify, and deploy the control software for the Horizontal Handling Machine, a safety-critical remote handling system in operation at SPES. The IEC 61499 standard's adoption led to a redesign of the control logic. Following a preliminary online simulation, the closed-loop system has been formally verified using the NuSMV symbolic model checker, with the help of the FB2SMV converter. In addition, the Function Blocks Modeling Environment tool was used for automating verification and analyzing counterexamples.",

keywords = "Formal verification, IEC 61499, isotope separation online (ISOL), model checking, NuSMV, radioactive ion beams (RIBs), remote handling, Selective Production of Exotic Species (SPES), simulation",

author = "Giordano Lilli and Midhun Xavier and {Le Priol}, Etienne and Vincent Perret and Tatiana Liakh and Roberto Oboe and Valeriy Vyatkin",

note = "Publisher Copyright: {\textcopyright} 2020 IEEE. | openaire: EC/HE/101057083/EU//Zero-SWARM",

year = "2023",

month = oct,

day = "16",

doi = "10.1109/OJIES.2023.3321084",

language = "English",

volume = "4",

pages = "417--431",

journal = "IEEE Open Journal of the Industrial Electronics Society",

issn = "2644-1284",

publisher = "IEEE",

}

TY - JOUR

T1 - Formal Verification of the Control Software of a Radioactive Material Remote Handling System, Based on IEC 61499

AU - Lilli, Giordano

AU - Xavier, Midhun

AU - Le Priol, Etienne

AU - Perret, Vincent

AU - Liakh, Tatiana

AU - Oboe, Roberto

AU - Vyatkin, Valeriy

PY - 2023/10/16

Y1 - 2023/10/16

N2 - Automation systems within nuclear laboratories are intended to work under harsh operating conditions. Selective Production of Exotic Species (SPES) is a nuclear research facility currently under construction by the Istituto Nazionale di Fisica Nucleare, dedicated to the production and study of radioactive ion beams. Isotopes are produced within the target ion source unit, a vacuum vessel that must be replaced on a regular basis. The highly radioactive environment necessitates the deployment of a set of automated systems dedicated to the unit's remote management. To meet high-level security standards, the design of such instrumentation and control systems must include extensive verification. Based on specific safety requirements, model checking can be used to assess the systems' correctness. This article describes how to employ an integrated toolchain to design, simulate, formally verify, and deploy the control software for the Horizontal Handling Machine, a safety-critical remote handling system in operation at SPES. The IEC 61499 standard's adoption led to a redesign of the control logic. Following a preliminary online simulation, the closed-loop system has been formally verified using the NuSMV symbolic model checker, with the help of the FB2SMV converter. In addition, the Function Blocks Modeling Environment tool was used for automating verification and analyzing counterexamples.

AB - Automation systems within nuclear laboratories are intended to work under harsh operating conditions. Selective Production of Exotic Species (SPES) is a nuclear research facility currently under construction by the Istituto Nazionale di Fisica Nucleare, dedicated to the production and study of radioactive ion beams. Isotopes are produced within the target ion source unit, a vacuum vessel that must be replaced on a regular basis. The highly radioactive environment necessitates the deployment of a set of automated systems dedicated to the unit's remote management. To meet high-level security standards, the design of such instrumentation and control systems must include extensive verification. Based on specific safety requirements, model checking can be used to assess the systems' correctness. This article describes how to employ an integrated toolchain to design, simulate, formally verify, and deploy the control software for the Horizontal Handling Machine, a safety-critical remote handling system in operation at SPES. The IEC 61499 standard's adoption led to a redesign of the control logic. Following a preliminary online simulation, the closed-loop system has been formally verified using the NuSMV symbolic model checker, with the help of the FB2SMV converter. In addition, the Function Blocks Modeling Environment tool was used for automating verification and analyzing counterexamples.

KW - Formal verification

KW - IEC 61499

KW - isotope separation online (ISOL)

KW - model checking

KW - NuSMV

KW - radioactive ion beams (RIBs)

KW - remote handling

KW - Selective Production of Exotic Species (SPES)

KW - simulation

UR - http://www.scopus.com/inward/record.url?scp=85174824634&partnerID=8YFLogxK

U2 - 10.1109/OJIES.2023.3321084

DO - 10.1109/OJIES.2023.3321084

M3 - Article

AN - SCOPUS:85174824634

SN - 2644-1284

VL - 4

SP - 417

EP - 431

JO - IEEE Open Journal of the Industrial Electronics Society

JF - IEEE Open Journal of the Industrial Electronics Society

ER -

Formal Verification of the Control Software of a Radioactive Material Remote Handling System, Based on IEC 61499

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Researchers from University of Padova Provide Details of New Studies and Findings in the Area of Industrial Engineering (Formal Verification of the Control Software of a Radioactive Material Remote Handling System, Based on IEC 61499)

Cite this

Formal Verification of the Control Software of a Radioactive Material Remote Handling System, Based on IEC 61499

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Press/Media

Researchers from University of Padova Provide Details of New Studies and Findings in the Area of Industrial Engineering (Formal Verification of the Control Software of a Radioactive Material Remote Handling System, Based on IEC 61499)

Cite this