Provably Correct Software: Don't Leave Earth Without It

Given the stakes, aerospace software absolutely must be correct and secure. Space hardware is exhaustively tested for operational use, but space software may not be provably correct for operational use, and failures can occur despite best efforts. This paper introduces a new technology for verifying aerospace software. This technology, known as Function Extraction, computes the behavior of software to produce its precise as-built specification for verification and security analysis. Behavior computation is a mathematics-based automated process that derives the domain-to-range behavior of a program at machine speeds with no program execution or human intervention required. This behavior encompasses the spectrum of possible tests and use-cases. As a result, a single behavior computation can provide more information regarding software functionality than large numbers of test cases. Behavior computation is enabled by new mathematical foundations for loop analysis that permit precise derivation of loop functionality. This paper describes Function Extraction technology, and illustrates its use in extraction and verification of the control equations implemented by an inertial navigation program inspired by NASA reports. Behavior computation can be integrated into aerospace software development and evolution processes to reduce risks of failures and compromises. Computed behavior serves as a Digital Twin for software that can enable more effective maintenance as well as reduction in technical debt. Software paired with computed behavior can be more valuable than the software alone.