Verification of autonomous robotic systems: A perspective

One precondition before autonomous mobile robots can be used in commercial application is a method to guarantee a desired behavior or the fulfillment of security requirements. However, this tasks leads to a contradiction between the desired flexible autonomous action of the robot in a complex environment and the required proof of a certain behavior. In this contribution we present a first step in this direction by applying formal verification using model checking to autonomous control architectures. The proposed approach has been investigated using a simple UAV application and some first results are presented.