Mission Planning and Verification for Autonomous Unmanned Aerial Vehicles

Autonomous robotic systems that work alongside humans or interact with valuable goods impose high demands on safety and fault tolerance. In this work, a robotic architecture is proposed that employs common model checking techniques to ensure the compliance of complex robotic missions with formally specified safety properties. Two formalisms are discussed to describe such mission plans: Hierarchical Finite State Machines and Behaviour Trees. Employing the explicit-state model checker DIVINE and the mission execution framework RAFCON, a tool chain has been developed that facilitates verification of LTL formulae on mission plans specified with either of those methodologies. The proposed system design tries to deal with hardware failures by calculating affected mission building blocks and removing them from the active plan