Abstract
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.
DISTRIBUTION STATEMENT A: Distribution unlimited; approved for public release; case number 88ABW-2017-1985.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
For the remainder of the paper, we use “task” to refer to a component of a mission in UxAS (see: [3]). When we refer to an Ada task, we will clearly indicate it as such.
- 2.
- 3.
- 4.
- 5.
- 6.
- 7.
In addition to standard containers defined by Ada in the form of generic packages, SPARK includes a library of formal containers that have been designed specifically to facilitate proof.
- 8.
https://github.com/AdaCore/OpenUxAS, in the ‘ada’ branch.
- 9.
We do not use Ada equality on the request queues: the requests contain parts which are hidden from SPARK, so SPARK does not know the meaning of equality for these queues; this is not the case, however, for the data configuration where we took care to only store SPARK-compatible information.
References
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). https://doi.org/10.1145/123041.123054
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
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
Kingston, D., Beard, R.W., Holt, R.S.: Decentralized perimeter surveillance using a team of UAVs. IEEE Trans. Robot. 24(6), 1394–1404 (2008)
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
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 This is a U.S. government work and not under copyright protection in the U.S.; foreign copyright protection may apply
About this paper
Cite this paper
Aiello, M.A., Dross, C., Rogers, P., Humphrey, L., Hamil, J. (2019). Practical Application of SPARK to OpenUxAS. In: ter Beek, M., McIver, A., Oliveira, J. (eds) Formal Methods – The Next 30 Years. FM 2019. Lecture Notes in Computer Science(), vol 11800. Springer, Cham. https://doi.org/10.1007/978-3-030-30942-8_45
Download citation
DOI: https://doi.org/10.1007/978-3-030-30942-8_45
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-30941-1
Online ISBN: 978-3-030-30942-8
eBook Packages: Computer ScienceComputer Science (R0)