Formal Verification of Robotic Behaviors\\in Presence of Bounded Uncertainties


Robotic behaviors are mainly described by differential
equations. Those mathematical models are usually not precise enough
because of inaccurately known parameters or model
simplifications. Nevertheless, robots are often used in critical
contexts as medical or military fields. So, uncertainties in
mathematical models have to be taken into account in order to
produce reliable and safe analysis results. A framework based on
interval analysis is proposed to safely verify and analyze robotic
behaviors with bounded uncertainties. It follows an interval
constraint programming approach, combined with validated numerical
integration methods to deal with differential equations. A case
study on robust path planning is presented to emphasize the
efficiency of the complete framework.

Author Biographies

Julien Alexandre dit Sandretto, ENSTA ParisTech
Researcher, U2IS
Alexandre Chapoutot, ENSTA ParisTech
Associated professor, U2IS
Olivier Mullier, ENSTA ParisTech
Researcher, U2IS