Development and Verification of a Flight Stack for a High-Altitude Glider in Ada/SPARK 2014
Abstract
SPARK 2014 is a modern programming language and a new state-of-the-art tool set for development and verification of high-integrity software. In this paper, we explore the capabilities and limitations of its latest version in the context of building a flight stack for a high-altitude unmanned glider. Towards that, we deliberately applied static analysis early and continuously during implementation, to give verification the possibility to steer the software design. In this process we have identified several limitations and pitfalls of software design and verification in SPARK, for which we give workarounds and protective actions to avoid them. Finally, we give design recommendations that have proven effective for verification, and summarize our experiences with this new language.
Motivation
In 2015, the Federal Aviation Administration (FAA) discovered a software fault in the Boeing 787 that could lead to loss of control if the airplane is powered for 248 days. A simple integer overflow would shut down all electrical alternating power sources simultaneously, regardless of whether the airplane would be on the ground or in the air. Despite their simplicity, overflow errors are still common errors that can cause catastrophic hazards. In order to detect faults in the program before they become run-time errors, many standards require a software verification process.
Verification of safety-critical software is often done after the software is completely implemented. Accepted standards for software development require a fixed software life-cycle process where software verification is mostly a mix of tests, simulation, and manual analysis. As a result, many faults are detected late during the development and some faults are not discovered at all, because traditional testing can only show the presence of run-time errors, but not their absence. Formal analysis, on the other hand, could be used to prove the absence of run-time errors, such as overflows. Since formal analysis is performed statically, it can also help in general to detect faults early during the development. However, formal methods—if used at all—are currently only applied as an additional verification step.
Our development process with integrated formal verification
Furthermore, formal methods are considered to be hard to integrate into the development process, because of the following reasons:
- large amount of additional formal property specifications
- proof requires a lot of user interaction, little automation
- results are difficult to understand and require experts
- special considerations apply and implementation possibilities are limited
- not accepted by standards and certification authorities
As a consequence, most projects refuse to use formal methods, despite the fact that research has shown that formal methods are promising to enhance the quality of the verification process.