Tech Reports

ULCS-11-001

Model Checking and the Certification of Autonomous Unmanned Aircraft Systems

Matt Webster, Michael Fisher, Neil Cameron, Mike Jump

Abstract

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.

For each technical report listed here, copyright and all intellectual property rights remain with the respective authors. Copyright is effective from the year of publication in each case. By downloading a file from this page, you agree to use it only for purposes of research and scholarship. Any other use of this material or storage of it in any medium or its sale or distribution in any form is expressly forbidden without prior written permission from the authors concerned.