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

that the resulting C-code consists of a single main loop whose body is a loop-
free program. Source languages with these features can benet from the method
proposed in this paper. For example, the language

[6] which comes from
the world of asynchronous distributed systems is another possible client of the
proposed method.
We present a common semantic model for

unity

and C, introduce the
applied notion of being a correct implementation , formulate the correctness of
the generated C code as proof obligations in rst order logic, and present ecient
decision procedures to check the correctness of the generated proof obligations.
All translations and constructions which are presented in the course of the paper
have been implemented in a tool called CVT (Code Validation Tool) [19]. CVT
has been used to validate the code generated from a 6000 lines

Signal

program
with more than 1000 variables. This program is a turbine-control system which
was developed as an industrial case study by SNECMA in the SACRES project.
A major advantage of a carefully designed translation validation tool is that it
can replace the need for correctness proofs for various compilers if these compilers
are based on the same denition of \correct code generation". This is the case
for the TNI and the Inria compiler and, indeed, CVT is used to validate code
originating from either of these two compilers.

Signal

1.2 Run Time Result Verication

There is a growing interest in the concept of verifying run-time results, rather
than programs or models. A recently held workshop entitled \run-time result
verication" presented various applications of run-time verication techniques.
These applications, in most cases, had similar characteristics to compiler veri-
cation, although they come from a variety of domains: it is very hard, or even
impossible to formally verify them in the `traditional', single-time proof on the
one hand, and on the other hand, their design often changes while the system
is developed. Another motivation for this approach is that in some cases the
program itself is not available for inspection due to commercial and intellectual
property factors 1 . A good example of such a domain is the formal verication
of decision procedures. Implementations of Decision procedures are often exper-
imental and not very robust. They are typically complex and keep evolving over
time. Being generic tools for verifying safety-critical systems, the correctness of
the tools is at least as important as that of the applications they help to verify.
In [21], the decision procedure generates proofs during run-time, in order to val-
idate the decision process. An axiomatization of the proof system is presented in
another formal system, which is referred to as the `logical framework' in which
the proof is carried out. The logical framework tool includes a proof checker of
its own, that can check proofs of any system that is axiomatized in the frame-
work. This enables automatic validation of every run of the decision procedure

1 this is also a common argument in the domain of testing, where often 'black-box'
testing is used rather than 'white-box' testing simply because the code is not available
for inspection