Formal Verification of the Control Software of a Radioactive Material Remote Handling System, Based on IEC 61499 [Elektronisk resurs]
-
Lilli, Giordano (författare)
-
Xavier, Midhun (författare)
-
Le Priol, Etienne (författare)
-
Perret, Vincent (författare)
-
Liakh, Tatiana (författare)
-
Oboe, Roberto (författare)
-
Vyatkin, Valeriy (författare)
-
Luleå tekniska universitet Institutionen för system- och rymdteknik (utgivare)
- Publicerad: Institute of Electrical and Electronics Engineers Inc. 2023
- Engelska.
-
Ingår i: IEEE Open Journal of the Industrial Electronics Society. ; 4, 417-431
-
Läs hela texten
-
Läs hela texten
-
Läs hela texten
- Relaterad länk:
-
http://www.ltu.se/ (Värdpublikation)
Sammanfattning
Ämnesord
Stäng
- 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.
Ämnesord
- Natural Sciences (hsv)
- Computer and Information Sciences (hsv)
- Computer Sciences (hsv)
- Naturvetenskap (hsv)
- Data- och informationsvetenskap (hsv)
- Datavetenskap (datalogi) (hsv)
- Engineering and Technology (hsv)
- Electrical Engineering, Electronic Engineering, Information Engineering (hsv)
- Computer Systems (hsv)
- Teknik och teknologier (hsv)
- Elektroteknik och elektronik (hsv)
- Datorsystem (hsv)
- Natural Sciences (hsv)
- Physical Sciences (hsv)
- Accelerator Physics and Instrumentation (hsv)
- Naturvetenskap (hsv)
- Fysik (hsv)
- Acceleratorfysik och instrumentering (hsv)
- Dependable Communication and Computation Systems (ltu)
- Kommunikations- och beräkningssystem (ltu)
Genre
- government publication (marcgt)
Indexterm och SAB-rubrik
- Formal verification
- IEC 61499
- isotope separation online (ISOL)
- model checking
- NuSMV
- radioactive ion beams (RIBs)
- remote handling
- Selective Production of Exotic Species (SPES)
- simulation
Inställningar
Hjälp
Ingår i annan publikation. Gå till titeln
IEEE Open Journal of the Industrial Electronics Society