Model-Based Testing of Robots with NModel

We present a method of two level modeling for model-based testing of robotics applications. The goal is to perform model-based hardware-in-the-loop testing of a system of robots. The main idea is to use models in two different roles: as control models of individual robots, and as a coordination model on the global level for modeling the behavior of the system. This way it is possible to reduce the total state space visible to the system level model since the local ab- stractors discard details that are not important from the global perspective. We demonstrate the approach with model programs of the toolkit NModel in the con- text of LEGO NXT based mobile robots. The system consists of robots sharing a critical resource — an intersection where they must not collide. The local control model distinguishes whether the robot is in the critical section and has the means to pause the robot in an appropriate zone. The coordination model provides the system view and enables to detect system level errors, for example whether it is possible that two robots enter the critical section at the same time. We present the local control models and the coordination models and the full toolchain for model-based testing of the system.