Exploring Frama-C Resources by Verifying Space Software

The verification process is mandatory in the critical software realm. To improve this process, static analysis tools can make significant contributions. Static analysis meets a variety of goals, including error detection, security analysis, and program verification, which is why standards for critical software development recommend the use of static analysis to identify errors that are difficult to detect at run-time. Thus, this chapter presents a case study on the use of Frama-C as a static analyzer for formal verification of critical software and a lightweight semantic-extractor tool; the former uses an abstract interpretation technique, and the latter allows for the extraction of semantic information to provide a better understanding of source code. In practical terms, the chapter shows how Frama-C can support the development life cycle of an inertial system in aerospace applications, reporting a list of pros and cons. The final results indicate the benefits obtained in terms of software safety, software quality assurance and, consequently, the software verification process.