Towards Verifiable Approach to Mission Planning for Multiple UAVs
Gopinadh Sirigineedi, Antonios Tsourdos, Brian A. White, Rafał Żbikowski · AIAA Infotech@Aerospace Conference · 2009
Multiple UAV missions ofier beneflts in terms of success rate and area coverage. This research is aimed at developing veriflable mission planning for multiple UAVs cooperatively searching an area. The complexity and safety critical nature of the mission motivated the use of a formal method like model checking to verify the correctness of the system. In this paper, we present model checking approach to verify the bahaviour of a UAV searching an area. The UAV behaviour is captured by means of a flnite state transition model known as Kripke model and the temporal speciflcations are expressed in computational tree logic (CTL). Symbolic Model Verifler (SMV), a popular model checker, has been used to verify whether the model satisfles the speciflcations.