Decentralised cooperative aerial surveillance for harbour security: A formal verification approach

Formal modelling techniques have been used to verify zero-fault tolerant systems such as hardware chips, communication protocols. In this paper we present formal modelling and verification of a multiple UAV system cooperatively monitoring a harbour area. Kripke modelling formalism is used to formally model the decentralised surveillance strategy and the desired system properties are expressed in temporal logic statements. The Kripke model is then subjected to an algorithmic verification technique known as model checking and the validity of the temporal formulae on the model is verified.