Practical Application of SPARK to OpenUxAS
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.
KeywordsOpenUxAS SPARK Formal methods Autonomy
- 2.Dross, C., et al.: Climbing the software assurance ladder-practical formal verification for reliable software (2018). https://www.adacore.com/uploads/techPapers/spark_avocs_2018.pdf
- 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). https://doi.org/10.1109/CCA.2016.7587813
- 5.Rasmussen, S., Kingston, D., Humphrey, L.: A brief introduction to unmanned systems autonomy services (UxAS), pp. 257–268 (June 2018). https://doi.org/10.1109/ICUAS.2018.8453287