CaSSIS-Verif

CaSSIS-Verif - Towards Verified Flight Software for Future Mars Missions
Software verification entails the algorithmic analysis of programs to mathematically prove properties of their executions - to prove that given certain assumptions, the code is correct and bug-free. It has found extensive application in embedded, cyber-physical, and safety-critical systems. Among others, it allows verifying array bounds (for absence of buffer overflows), pointer safety, exceptions and user-specified assertions. Several approaches involving C/C++ codebases are being actively pursued by the research community.

Performing software verification in practice requires appropriately instrumenting the code at hand, invoking often complicated toolchains, and interpreting verification results. We seek to investigate semi-automation of this process in the context of mission-critical space software. We envision (i) appropriate abstractions and automation tools tailored to this challenging domain, as well as making steps towards (ii) integrating software verification into the development process of mission-critical space software.

This project will leverage expertise of the Planetary Imaging Group in the Space Research and Planetology Division of the Physikalisches Institut and the Software Engineering Group at the Institute of Computer Science, towards the verification of CaSSIS flight software. This is a goal that is highly interdisciplinary in nature, since expertise of both groups is involved.