Practical Application of SPARK to OpenUxAS

  • M. Anthony Aiello
  • Claire Dross
  • Patrick Rogers
  • Laura HumphreyEmail author
  • James Hamil
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11800)


This paper presents initial, positive results from using SPARK to prove critical properties of OpenUxAS, a service-oriented software framework developed by AFRL for mission-level autonomy for teams of cooperating unmanned vehicles. Given the intended use of OpenUxAS, there are many safety and security implications; however, these considerations are unaddressed in the current implementation. AFRL is seeking to address these considerations through the use of formal methods, including through the application of SPARK, a programming language that includes a specification language and a toolset for proving that programs satisfy their specifications. Using SPARK, we reimplemented one of the core services in OpenUxAS and proved that a critical part of its functionality satisfies its specification. This successful application provides a foundation for further applications of formal methods to OpenUxAS.


OpenUxAS SPARK Formal methods Autonomy 


  1. 1.
    Butler, R.W., Finelli, G.B.: The infeasibility of experimental quantification of life-critical software reliability. SIGSOFT Softw. Eng. Notes 16(5), 66–76 (1991). Scholar
  2. 2.
    Dross, C., et al.: Climbing the software assurance ladder-practical formal verification for reliable software (2018).
  3. 3.
    Kingston, D., Rasmussen, S., Humphrey, L.: Automated UAV tasks for search and surveillance. In: 2016 IEEE Conference on Control Applications (CCA), pp. 1–8 (September 2016).
  4. 4.
    Kingston, D., Beard, R.W., Holt, R.S.: Decentralized perimeter surveillance using a team of UAVs. IEEE Trans. Robot. 24(6), 1394–1404 (2008)CrossRefGoogle Scholar
  5. 5.
    Rasmussen, S., Kingston, D., Humphrey, L.: A brief introduction to unmanned systems autonomy services (UxAS), pp. 257–268 (June 2018).

Copyright information

© This is a U.S. government work and not under copyright protection in the U.S.; foreign copyright protection may apply 2019

Authors and Affiliations

  • M. Anthony Aiello
    • 1
  • Claire Dross
    • 2
  • Patrick Rogers
    • 1
  • Laura Humphrey
    • 3
    Email author
  • James Hamil
    • 4
  1. 1.AdaCore Technologies, Inc.New YorkUSA
  2. 2.AdaCore SASParisFrance
  3. 3.Air Force Research LaboratoryDaytonUSA
  4. 4.LinQuest CorporationBeavercreekUSA

Personalised recommendations