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

by producing a proof script for the run and applying to it the framework's proof
checker.
The concept of validating translators/compilers by proving semantical equiv-
alence between source and target code has been applied in various other projects.
In [22] and [8] the verication of the translator from a high level description lan-
guage to executable code is carried out in two distinct stages: in the 'on-line'
stage, each run of the translator is veried by proving several simple conditions
on the syntactical structure of the results, in comparison to the source code. This
stage is fully automatic and implemented by a simple 'checker'. The reduction
from full translation verication to these simple rules is carried out manually in
a one-time eort (the 'o-line' stage) by an expert. This approach was applicable
in their case due to the relatively structured translation scheme of the source
code. A declaration in the source code is translated into code which performs
RNS transformations (it reduces arithmetical operations to a set of indepen-
dent arithmetic operations on integers of limited size). Thus, the main task of
the validation process is to verify that these transformations are correct. Af-
ter computing a mapping between the input and output variables of the source
and target programs, they prove that the correspondence between the 'semantic'
states of the two programs is preserved by the execution steps. In this sense there
model is similar to the model we will present in this paper. In [7], translation
validation is done on a purely syntactic level. Their method is based on nd-
ing a bijection between abstract and concrete instruction sets (resp. variables)
because they are considering a structural translation of one sequential program
into another sequential program. Since we are dealing with optimizing compilers
we have to employ a far more involved semantic approach.
The rest of the paper is organized as follows. In Section 2 we give a brief
introduction to

and present a running example. After introducing syn-
chronous transition systems as our model of computation in Section 3 we address
the formal semantics of

Signal

. Section 4 presents the concepts which underly
the generation of the proof obligations. In Section 5 we present the decision pro-
cedure to check the validity of these proof obligations. Finally, Section 7 contains
some conclusions and future perspectives.

Signal

2 An Illustrative Example

In this section we rst illustrate details of the compilation process by means
of an example and then explain the principles which underly the translation
validation process.
A program describes a reactive system whose behavior along time is

an innite sequence of instants which represent reactions, triggered by external
or internal events. The main objects manipulated by a

Signal

program are
flows , which are sequences of values synchronized with a clock .Aflowisatyped
object which holds a value at each instant of its clock. The fact that a flow is
currently absent is represented by the bottom symbol

Signal

? (cf. [3]). Clocks are

unary flows, assuming the values f T ;?g . A clock has the value T if and only if