TY - GEN

T1 - Towards Verification Reflex Programs in the Rodin Platform

AU - Shabanova, Margarita

AU - Garanina, Natalia

N1 - Conference code: 26

PY - 2025/8/8

Y1 - 2025/8/8

N2 - Reflex is a domain-specific language designed for developing industrial automation and control systems. Errors in software code can lead to equipment failure, product damage, or even dangerous accidents. Ensuring the correctness of Reflex programs is crucial for the reliability, safety and efficiency of such systems. Therefore, we develop approaches to verifying Reflex programs using formal methods. One such approach is to verify Reflex programs in the Rodin platform, a tool for formal verification. To do this, we need to transform the Reflex program to the Even-B language, the input language of the Rodin platform. We developed a set of transformation rules to systematically map Reflex constructs to E vent-B models. By applying these rules, Reflex programs c an b e analyzed using proof obligations and model-checking techniques to detect potential errors early in the development process. This approach enhances software reliability and ensures compliance with safety standards in industrial automation. Our results demonstrate the feasibility of using Event-B for Reflex program verification.

AB - Reflex is a domain-specific language designed for developing industrial automation and control systems. Errors in software code can lead to equipment failure, product damage, or even dangerous accidents. Ensuring the correctness of Reflex programs is crucial for the reliability, safety and efficiency of such systems. Therefore, we develop approaches to verifying Reflex programs using formal methods. One such approach is to verify Reflex programs in the Rodin platform, a tool for formal verification. To do this, we need to transform the Reflex program to the Even-B language, the input language of the Rodin platform. We developed a set of transformation rules to systematically map Reflex constructs to E vent-B models. By applying these rules, Reflex programs c an b e analyzed using proof obligations and model-checking techniques to detect potential errors early in the development process. This approach enhances software reliability and ensures compliance with safety standards in industrial automation. Our results demonstrate the feasibility of using Event-B for Reflex program verification.

KW - Event-B

KW - Reflex language

KW - Rodin

KW - control systems

KW - formal verification

KW - industrial automation

KW - transformation rules

UR - https://www.scopus.com/pages/publications/105014150497

UR - https://www.mendeley.com/catalogue/d8196188-f6f1-31b7-9c44-ab4129d36b61/

U2 - 10.1109/EDM65517.2025.11096842

DO - 10.1109/EDM65517.2025.11096842

M3 - Conference contribution

SN - 9781665477376

T3 - International Conference of Young Specialists on Micro/Nanotechnologies and Electron Devices, EDM

SP - 1490

EP - 1495

BT - International Conference of Young Specialists on Micro/Nanotechnologies and Electron Devices, EDM

PB - IEEE Computer Society

T2 - 2025 IEEE 26th International Conference of Young Professionals in Electron Devices and Materials (EDM)

Y2 - 27 June 2025 through 1 July 2025

ER -