Static code analysis of a critical embedded software

In the context of a IEC 61508 embedded system certification, I had to perform a static analysis of the embedded operating software, written in C.

To do so, I had to use Frama-C, a static software analyzer developped by our technological partners from CEA-List Safety and Security Lab.

To perform the analysis, I had to export the pre-processed code from the prorpietary IDE used to develop it, and then tune the analyzer with respect to loop bounds and hardware interrupts possibly encountered during exploitation, in order to have the most representative analysis.