Embedded Flight Software Verification (ESOVER)
Together with the Lab for Automated Reasoning (LARA) at EPFL, Ateleris is executing a study using formal software verification to develop mathematically proven (i.e., correct) embedded software. The study is run in the frame of the Mesure de Positionnement 2020 (MdP) of the Swiss Space Office, Space Innovation, and ESA.
To learn more about our current activity, “Generating Formally Verified Communication Protocol Implementations,” visit the ESA Activity website.
A well-known saying in software engineering is, “Software testing proves the existence of bugs, not their absence.” This study aims to introduce cost-effective formal software verification into the development process of space applications, leading to software that is proven to be without defects.
Formal software verification is a method that uses mathematical proofs to establish that software behaves according to the given specification. The use of mathematical proof allows us to verify correctness in all scenarios, even when the number of such scenarios is so large that testing all of them would be infeasible.
The study expands on the groundwork laid out by the LARA group and uses the Scala-based formal software verification tool called Stainless. The EPFL LARA team is extending the Stainless framework, so it understands a larger and more complex set of Scala instructions. This extension is necessary to be able to develop meaningful flight software modules.
In a proof of concept, Ateleris, with their know-how in writing flight software for the STIX instrument, will test the suitability of the approach on the STIX file system. To that end, Ateleris will rewrite the file system in Scala and then verify it with Stainless to create a mathematically proven defect-free file system module.
To facilitate the reintegration process of the verified file system module into the overall flight software, the LARA team and Ateleris will add a new C-code transpiler to the Stainless platform to allow the verified Scala code to be transformed back into runnable C-code.
Why use formal software verification and Stainless?
To generate correct software. With formal verification, the software is proven correct, according to the specification, i.e., all possible inputs have been considered, meaning the software will react correctly to any input.
To be compliant with requirements by design. With formal verification, requirements become part of the software. Changes in the behavior will automatically be detected and reported when they violate the specification.
To have increased software-production efficiency. Flight software development is, in many cases, done in the programming languages C or C++. Programming in these low-level languages is difficult and time-consuming because they allow undefined behaviors, lack complete type-safety, and can be difficult to refactor. This limitation not only introduces many potentially critical errors (buffer overflows, illegal memory access, endless loops, and others) but also slows down development. In the Stainless platform, the programming language Scala is used instead. This higher-level programming language increases developer productivity by offering better abstractions, tooling, and safeguards.
To improve software integration. With formally verified software modules, the API and functionality of the software components can be verified and proven to be correct – after every modification.
To create code for multiple targets. Stainless can automatically translate Scala code back to C code, allowing easy integration with the existing codebase. This improvement also helps with certification, as the space community is skeptical of programming languages and runtimes other than C or C++. By automatically translating Scala code to C and submitting C code for qualification, we sidestep these concerns.
To have reusable verified modules. Once a module or function has been verified, it can be reused in other software and is still correct (with certain limitations). This versatility will allow the construction of a library of verified modules to be reused in other flight software or embedded systems. For example, verified data structures and file systems are modules reusable in a variety of applications.
For integration into the software development process. The proposed approach can be integrated into the traditional software development process and complements other processes like static verification and unit and integration testing (CI/CD).
Publications
- ESOVER Management Summary (PDF)
- Hamza, J., Felix, S., Kunčak, V., Nussbaumer, I., Schramka, F. (2022). From Verified Scala to STIX File System Embedded Code Using Stainless. In: Deshmukh, J.V., Havelund, K., Perez, I. (eds) NASA Formal Methods. NFM 2022. Lecture Notes in Computer Science, vol 13260. Springer, Cham. https://doi.org/10.1007/978-3-031-06773-0_21
Key Technologies/Terms
- Formal Software Verification
- Scala Language
- C-code Transpiler
- Embedded Software Programming
- Stainless Platform
- ASN1SCC (GitHub repository, blog post)
LARA is a research group at EPFL, led by Viktor Kunčak. They develop precise automated reasoning techniques: tools, algorithms, and languages—the goal of these techniques to help the construction of verified computer systems.
