THE PROOF THAT THE COMPILER HAS FAITHFULLY TRANSLATED THE SOURCE CODE

With so many ways that a compiler can choose to translate your C source code into the executable, what guarantees are there that this has been done correctly, completely and has not introduced functionality you did not want? The typical approach to assurance is to verify through the use of extensive test. This is expensive and time consuming.

Furthermore, when something has failed to pass test, it is time consuming to identify what has gone wrong and where. FEVER® cuts this effort by automatically showing that the translation from source code is correct through the exploitation of proof.

Benefit 1

Provides assurance of object code

‍

Benefit 2

Automation reduces costs

‍

Benefit 3

Speeds up development

‍

Benefit 4

Can be used in formal methods based tool chain or otherwise

Benefit 1

Reduces the opportunity for error

Benefit 2

Requirements are verifiable

Benefit 3

Simple compliance
to standards

Benefit 4

Automatic checks for consistency

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.

FEVER® in a test-oriented development process

Should a developer wish to use FEVER® in a test-oriented approach, this is possible under certain conditions and will bring considerable benefit. Firstly, 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 ofMISRA-C.

The sub-set is called C-♭ and has a set of independently proven formal semantics for use in programme proof. 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. 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. Compliance to this subset can be automatically checked using the D-RisQ Compliance Tool. FEVER® will then be able to check that the source code has been faithfully translated to the executable and hence reduce the search space for errors during test. By focusing effort on the requirements, design and then code phases.