Towards the Translation of Reflex Programs to Promela: Model Checking Wheelchair Lift Software
Anna A. Ponomarenko, Natalia Olegovna Garanina, Sergey Mikhailovich Staroletov, Vladimir Zyubin · 2021 IEEE 22nd International Conference of Young Professionals in Electron Devices and Materials (EDM) · 2021
In the paper, we examine an approach for verifying control programs initially specified in the process-oriented programming language Reflex using model checking, a formal verification method. We propose a technique to translate discrete-state Reflex programs into Promela language. The latter language fits into the class of modeling languages, and is used with the SPIN verifier. We consider a Reflex-program intended to control a wheelchair lift (platform for low-mobility users). We describe the program-to-model transformation for this example, elaborate requirements and discuss the result of verification consideration.