Towards Verification Reflex Programs in the Rodin Platform

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.