Verification of embedded control programs

In this paper we are concerned with the problem of verifying embedded control programs. The approach we use combines the logico-numerical techniques developed for the verification of Lustre programs and the set-based image computation for continuous systems. The practical interest of this approach lies in the fact that there exists a tool for generating Lustre code for controllers described in Simulink. We also illustrate the approach with some experimental results obtained for a robotic controller for LEGO Mindstorm.