Practical Application of SPARK to OpenUxAS: Initial Results

Formal methods provide powerful tools for the analysis of complex software, enabling engineers to establish assurance of high quality in their software. The SPARK language and tools build upon the foundation of Ada and allow engineers to program not only their software, but also their specifications and their proofs. SPARK thus provides engineers a practical, industrial strength formal method. In this poster, we present initial results from the application of SPARK to OpenUxAS, an Air-Force relevant service-oriented architecture designed to enable cooperative control over multiple unmanned systems in the presence of uncertain comms. We discuss the reimplementation of pieces of the C++ architecture in Ada, the implementation and proof of functional correctness of critical functionality that establishes the validity of tasks submitted to the architecture in SPARK, and describe our next steps, which will lay a foundation for architecture-wide proofs of high-level, application-relevant properties.

M. Anthony Aiello joined AdaCore in April 2018, where he leads the development of System-to-Software Integrity, leads the application of an argument-centric approach based on the overarching properties to qualification of a code generator for use in development of DO-178C Level A software, and leads US-based research activities. Before joining AdaCore, Mr. Aiello was a Principal Scientist at Dependable Computing from 2010 to 2018 and President of Dependable Computing from 2017 to 2018. While at Dependable Computing, Mr. Aiello was the principal investigator of many research efforts related to the application of formal methods, systems engineering, and assurance-case development. Mr. Aiello received a Masters of Computer Science in 2005 and a Bachelors of Science in 2004, both from the University of Virginia.