Formal Verification of Robotic Missions and Tasks

An undersea robot like a long-range AUV is a typical example of a critical system, like a satellite or a planetary rover. We mean here that, for such a system, any repairing or recovery operation, even a mission reconfiguration, which would involve the intervention of a human operator is always costly, often difficult and sometimes impossible. This is why such systems should be at least provided with capacities of on-line adaption, like self replanning or sensor-based control. However, this is not sufficient and we have to be sure, as far as possible, that the system will behave correctly, before launching. More precisely, once a mission has been defined, we would like to verify that: * its specifications are correct, i.e. that they correspond to the desired goals, * its programming conforms to specifications, * the constraints induced by real-time and implementation issues do not disturb its behaviour. We are therefore led back to the need for verifying the logical aspects (absence of deadlocks, conformity of the results for various scenarii...), checking some temporal characterisation (absence of temporal deadlocks, values of lower and upper bounds on the duration of specific tasks...) and, possibly, studying hybrid models including other kinds of variables