Continuous Formal Verification for Aerospace Applications

Aerospace systems have the most stringent requirements when it comes to safety and reliability. The harsh environment combined with the immense costs of designing and manufacturing space applications places huge concern over ensuring that applications are dependable and function as desired. Formal verification is a tool to guarantee correctness for software executing on aerospace platforms. The advantage of formal verification is the complete absence of error against a design specification. Many applications leverage formal verification to ensure correctness and even integrate it into the certification process (e.g. DO-178C).Formal verification is a highly complex and computationally intense process that requires validating complex structures and an iterative approach to achieve a final, formally verified design. This process is further complicated in aerospace applications as traditional methods often exhibit behavioural differences between a formally verified model and the final software when deployed onto embedded architectures. Thus, formal verification needs to ensure that the verified design is accurate and representative of the executable on the target platform. Another major limitation of formal verification is that current approaches place formal verification towards the end of a project lifecycle. This creates a waterfall design and validation process that often leads to significant rewrites that prevent iterative verification.This research introduces continuous verification, a methodology consistent with current principles and practices in Agile development. This approach allows the early detection and correction of errors during the early stages of a project lifecycle. Designers can now decompose the system as a whole and implement models iteratively. Continuous verification allows the partial verification of models while the programmer iteratively implements them, allowing the early correction of errors and identification of non-verifiable entities that require different forms of validation. Our approach uses executable models that ensure a continuously verifiable design as each new feature gets verified as the application evolves. At any point in time, the working system is also formally verified.We demonstrate the feasibility of this approach through continuous verification using GitHub workflows that continuously integrate and verify designs on target hardware. Verification is performed on the target hardware itself, ensuring a verified, executable model. We have evaluated this approach using flight software that utilises an FPGA and processor that communicate through a shared memory interface. The software components of this design follow trunk-based development with a formally verified main branch. This software is due to launch on a satellite in October 2024.