Formal verification of behaviour networks including sensor failures

• Behaviour-based systems are verified using model checking.
• The model checking toolbox Uppaal is used.
• Sensor failures are integrated into the model.
• Crucial properties are checked to ensure the safety of the analysed systems.
• Examples from real robotic systems show the soundness of the presented approach.

The paper deals with the problem of verifying behaviour-based control systems. Although failures in sensor hardware and software can have strong influences on the robot’s operation, they are often neglected in the verification process. Instead, perfect sensing is assumed. Therefore, this paper provides an approach for modelling the sensor chain in a formal way and connecting it to the formal model of the control system. The resulting model can be verified using model checking techniques, which is shown on the examples of the control systems of an autonomous indoor robot and an autonomous off-road robot.