Advertisement

Formal Methods for the Certification of Autonomous Unmanned Aircraft Systems

  • Matt Webster
  • Michael Fisher
  • Neil Cameron
  • Mike Jump
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6894)

Abstract

In this paper we assess the feasibility of using formal methods, and model checking in particular, for the certification of Unmanned Aircraft Systems (UAS) within 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. Next we build a more advanced 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.

Keywords

Model Checking Formal Methods Unmanned Aircraft System Autonomous Systems Certification 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Bordini, R., Dastani, M., Dix, J., El Fallah-Seghrouchni, A. (eds.): Multi-Agent Programming: Languages, Tools and Applications. Springer, Heidelberg (2009)zbMATHGoogle Scholar
  2. 2.
    Bordini, R.H., Dennis, L.A., Farwer, B., Fisher, M.: Automated Verification of Multi-Agent Programs. In: Proc. 23rd Int. Conf. Automated Software Engineering (ASE), pp. 69–78. IEEE Computer Society Press, Los Alamitos (2008)Google Scholar
  3. 3.
    Bordini, R.H., Fisher, M., Sierhuis, M.: Formal Verification of Human-Robot Teamwork. In: Proc. 4th Int. Conf. Human-Robot Interaction (HRI), pp. 267–268. ACM, New York (2009)Google Scholar
  4. 4.
    Bordini, R.H., Fisher, M., Visser, W., Wooldridge, M.: Model Checking Rational Agents. IEEE Intelligent Systems 19(5), 46–52 (2004)CrossRefGoogle Scholar
  5. 5.
    Brat, G., Denney, E., Giannakopoulou, D., Frank, J., Jonsson, A.: Verification of Autonomous Systems for Space Applications. In: Proc. IEEE Aerospace Conference (2006)Google Scholar
  6. 6.
    Chaudemar, J.-C., Bensana, E., Seguin, C.: Model Based Safety Analysis for an Unmanned Aerial System. In: Proc. Dependable Robots in Human Environments, DRHE (2010)Google Scholar
  7. 7.
    Civil Aviation Authority. CAP 393 Air Navigation: The Order and the Regulations (April 2010), http://www.caa.co.uk/docs/33/CAP393.pdf
  8. 8.
    Civil Aviation Authority. CAP 722 Unmanned Aircraft System Operations in UK Airspace — Guidance (April 2010) http://www.caa.co.uk/docs/33/CAP722.pdf
  9. 9.
    Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  10. 10.
    Dennis, L.A., Farwer, B.: Gwendolen: A BDI Language for Verifiable Agents. In: Logic and the Simulation of Interaction and Reasoning. AISB 2008 Workshop (2008)Google Scholar
  11. 11.
    Dennis, L.A., Fisher, M., Webster, M.P., Bordini, R.H.: Model Checking Agent Programming Languages. Automated Software Engineering (in press)Google Scholar
  12. 12.
    European Aviation Safety Agency. Certification Specifications for Large Aeroplanes CS-25 (October 2003) ED Decision 2003/2/RM Final 17/10/2003.Google Scholar
  13. 13.
    Holzmann, G.: The Spin Model Checker: Primer and Reference Manual. AW (2004)Google Scholar
  14. 14.
    Jeyaraman, S., Tsourdos, A., Zbikowski, R., White, B.: Formal Techniques for the Modelling and Validation of a Co-operating UAV Team that uses Dubins Set for Path Planning. In: Proc. American Control Conference (2005)Google Scholar
  15. 15.
    Johnson, C.: Computational Concerns in the Integration of Unmanned Airborne Systems into Controlled Airspace. In: Schoitsch, E. (ed.) SAFECOMP 2010. LNCS, vol. 6351, pp. 142–154. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  16. 16.
  17. 17.
    Model-Checking Agent Programming Languages, http://mcapl.sourceforge.net
  18. 18.
    McRuer, D., Graham, D.: Flight control century: Triumphs of the systems approach. Journal of Guidance, Control and Dynamics 27(2), 161–173 (2004)CrossRefGoogle Scholar
  19. 19.
    Nikora, A.P., Balcom, G.: Automated identification of LTL patterns in natural language requirements. In: Proceedings of the 20th International Symposium on Software Reliability Engineering, ISSRE 2009, pp. 185–194. IEEE Computer Society, Los Alamitos (2009)CrossRefGoogle Scholar
  20. 20.
    Office of the Secretary of Defense. Unmanned Aircraft Systems Roadmap 2005–2030. US DoD Publication (2005)Google Scholar
  21. 21.
    Patchett, C., Ansell, D.: The Development of an Advanced Autonomous Integrated Mission System for Uninhabited Air Systems to Meet UK Airspace Requirements. In: Proc. International Conference on Intelligent Systems, Modelling and Simulation (2010)Google Scholar
  22. 22.
    Rao, A., Georgeff, M.: Modeling Agents within a BDI-Architecture. In: Proc. 2nd International Conference on Principles of Knowledge Representation and Reasoning (KR), pp. 473–484. Morgan Kaufmann, San Francisco (1991)Google Scholar
  23. 23.
    Sirigineedi, G., Tsourdos, A., Zbikowski, R., White, B.A.: Modelling and Verification of Multiple UAV Mission Using SMV. In: Proc. FMA 2009. EPTCS, vol. 20 (2009)Google Scholar
  24. 24.
    Sward, R.E.: Proving Correctness of Unmanned Aerial Vehicle Cooperative Software. In: Proc. IEEE International Conference on Networking, Sensing and Control (2005)Google Scholar
  25. 25.
    Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model Checking Programs. Automated Software Engineering 10(2), 203–232 (2003)CrossRefGoogle Scholar
  26. 26.
    Williams, E.: Airborne Collision Avoidance System. In: Cant, T. (ed.) Proc. 9th Australian Workshop on Safety Critical Systems and Software, SCS 2004. Conferences in Research and Practice in Information Technology, vol. 47, pp. 97–110 (2004)Google Scholar
  27. 27.
    Wooldridge, M.: An Introduction to Multiagent Systems. John Wiley & Sons, Chichester (2002)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Matt Webster
    • 1
  • Michael Fisher
    • 2
  • Neil Cameron
    • 1
  • Mike Jump
    • 1
    • 3
  1. 1.Virtual Engineering CentreDaresbury LaboratoryWarringtonUK
  2. 2.Department of Computer ScienceUniversity of LiverpoolUK
  3. 3.School of EngineeringUniversity of LiverpoolUK

Personalised recommendations