# FEVER® in a formal methods tool chain

**FEVER®** can be used to** formally verify** that the **executable object code** for various target processors **satisfies the C source code** from which it was compiled. In order to do this, the source code has to have a **set of semantics** that can be automatically translated to a **formal specification**. The Coding Standard used a subset of C that is an implementation of MISRA-C. The sub-set is called C-♭ and has a set of independently proven formal semantics for use in programme proof (this standard is freely available from D-RisQ on application). As the source code has a set of formal semantics, then it is possible to automatically prove that the compiler has not made any mistakes in the instance of the specific program.

Furthermore, if **CLawZ****®** has been used to prove correctness of the source code with respect to the **design** and if **Modelworks****®** has been used to prove correctness of the design with respect to its **requirements**, then it is the case that the executable, not only **satisfies the source code**, but the **design and the requirements**. This provides the evidence needed to satisfy, for example, **RTCA DO-333/EUROCAE ED-216C section 6.7.f.** The approach enables the compliance to virtually all of Table FM-A.7 this removing the need for expensive test support to meet the criteria for coverage such as MC/DC.