Translation Validation: From Signal to C - Correct System Design: Recent Insights and Advances - page 222

for-example, [5, 9, 10, 15, 12, 11, 14, 13]), the formal verication of industrial
code generators is generally prohibitive due to their size. Another problem with
compiler verication is that the formal verication freezes the design and evolu-
tion of the compiler, as each change to the code generators nullies their previous
correctness proof.
Alternately, code-validation suggests to construct a fully automatic tool
which establishes the correctness of the generated code individually for each
run of the code generator. In general, code-validation can be the key enabling
technology to allow the usage of code generators in the development cycle of
safety-critical and high-quality systems. The combination of automatic code gen-
eration and validation improves the design flow of embedded systems in both
safety and productivity by eliminating the need for hand-coding of the target
code (and consequently coding-errors are less probable) and by considerably
reducing unit/integration test eorts.
Of course, it is not clear that every compiler and every source and target
languages can be veried according to the code-validation paradigm. But the fact
that the compiler we considered was highly optimized and the source and target
languages had completely dierent structures (synchronous versus sequential
code) indicates that this method has the potential of solving realistic, non-trivial
cases.
The work carried out in the SACRES project proves the feasibility of code-
validation for the industrial code generator used in the project, and demonstrates
that industrial-size programs can be veried fully automatically in a reasonable
amount of time.

1.1 Technical Introduction

In this paper we consider translation validation for the synchronous languages
Signal [3]. This language is mainly used in industrial applications for the de-
velopment of safety-critical, reactive systems. In particular, it is designed to
be translatable into code which is as time/space ecient as handwritten code.
This code is generated by sophisticated code generators which perform vari-
ous analyses/calculations on the source code in order to derive highly ecient
implementations in languages such as C, ADA, or JAVA.
The presented translation validation approach addresses two industrial com-
pilers from

to C. These compilers { which apply more than 100 op-
timization rules during code generation [16] { were developed in the ESPRIT
project SACRES by the French company TNI and by Inria (Rennes) and are
used by Siemens, SNECMA and British Aerospace. Their formal verication is
prohibitive due to their size (more than 20,000 lines of code each) and the fact
that they are constantly improved/extended.
While developed in the context of code generators for synchronous languages,
the proposed method has wider applicability. The main feature which enables
us to perform the validation task algorithmically is that the source language
has a restricted explicit control structure. This is also represented by the fact

Signal