Dynamic Mission Planning of Multiple Unmanned Autonomous Platforms for Sensing and Autonomous Urban Reconnaissance
Ke Yu, Antonios Tsourdos, Brian A. White, Peter M. G. Silson · 2009
The aim of this paper is to address two problems which arose in the context of the UK MoD grand challenge when applying formal method. Basic problem is how to formally describe and verify decision making process? Besides the common use of formal method, i.e., formal description and verification, but furthermore, is it possible that formal method can instruct the execution of decision making? To address these questions the behaviours of each sub-system, including the ground control station, the ground vehicle, a micro aerial vehicle (MAV), a high level unmanned aerial vehicle (HLUAV) are investigated and captured and a Kripke model is used to formally describe the system behaviours. Theses behaviour can be easily verified by model checker like SPIN if needed. The main contributions of the paper is the description of how model checking technique can be applied to decision making in UAS such as the MoD grand challenge and to enhance their robustness. Not limited to the common way of using model checking, the paper shows that model checking can instruct system's behaviour as well. In other words, model checking is not just an assistant tool but can be a part of whole system. It is a novel way of applying model checking technique. The paper shows that formal method does enhance the robustness of system. It can not only verify a model but solve a problem.