Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Research › peer-review
Towards Verification Reflex Programs in the Rodin Platform. / Shabanova, Margarita; Garanina, Natalia.
International Conference of Young Specialists on Micro/Nanotechnologies and Electron Devices, EDM. IEEE Computer Society, 2025. p. 1490-1495 (International Conference of Young Specialists on Micro/Nanotechnologies and Electron Devices, EDM).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Research › peer-review
}
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 -
ID: 68938254