Tech Reports


Model Checking and the Certification of Autonomous Unmanned Aircraft Systems

Matt Webster, Michael Fisher, Neil Cameron, Mike Jump


In this paper we assess the feasibility of using formal methods, and model checking in particular, within the certification of Unmanned Aircraft Systems (UAS) for civil airspace. We begin by modelling a basic UAS control system in PROMELA, and verify it against a selected subset of the CAA's Rules of the Air using the SPIN model checker. We then refine our UAS control system to incorporate probabilistic aspects, verifying it against the same Rules of the Air using the probabilistic model checker PRISM. This shows how we can measure statistical adherence to such rules. Next we build a similar UAS control system using the autonomous agent language Gwendolen, and verify it against the small subset of the Rules of the Air using the agent model checker AJPF. We introduce more advanced autonomy into the UAS agent and show that this too can be verified. Finally we compare and contrast the various approaches, discuss the paths towards full certification, and present directions for future research.

[Full Paper]