Formal Verification in Robotics: Why and How?

摘要: A mobile robot aimed to operate in an hazardous environment is a typical example of critical system. We mean here that, for such system, like satellite, any repairing or recovery operation, even mission reconfiguration, which would involve the intervention human operator always costly, often difficult and sometimes impossible. This why systems should be at least provided with capacities on-line adaption, self replanning sensor-based control. However, this not sufficient we have sure, as far possible, that system will behave correctly, before launching. More precisely, once has been defined, verify that: its specifications are correct, i.e. they correspond desired goals, its programming conforms specifications, the constraints induced by real-time implementation issues do disturb its behavior.