Specification and Verification of Collaborative Transport Robots

A collaborative embedded system is an intelligent agent in a cyber-physical system which cooperates with others by negotiation to fulfill individual and common goals. Examples are self-driving cars, soccer-playing robots, or adaptive production plants. In this contribution, we present the industrial case study of autonomous transport robots in factory environments. In our setting, the robots collaborate by competing for transport jobs issued by the production machines. Each robot calculates its individual cost incurring with the job (in terms of distance, time, energy, wear and tear, etc.) and places a bid based on this cost. Then a distributed voting takes place, where the lowest cost bid wins the job. Here, we present our results of specifying and verifying this scenario. We collected requirements via user stories for the scenario, formulated these in suitable specification languages, designed executable models as simulation environments, and used statistical model checking and runtime monitoring for analysing the scenario. We argue that for different aspects of the case study, different analysis methods are to be used. However, all of these methods can make use of the fact that the goals of the individual agents coincide. Our results indicate that by the individual optimization of the cost function, reliability and performance of the collaborative group increases. We believe that this result is typical for a large number of similar systems.