A Formal Approach to Multi-UAV Route Validation
Toby Wilkinson, Michael J. Butler, Martin Paxton, Xanthippe Waldron · ePrints Soton (University of Southampton) · 2015
We present ongoing work to apply Event-B to the validation of routes for an Unmanned Aircraft System consisting of a Ground Control Station and two or more UAVs.We extend the mathematical language of Event-B to include a theory of continuous paths in 3-D Euclidean space that allows important safety properties describing the safe separation of UAVs to be formalised in a natural manner.Refinement of the model allows a mathematically verified route validator algorithm to be systematically derived.