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

to C ???

Translation Validation: From Signal

A. Pnueli, O. Shtrichman, and M. Siegel

Weizmann Institute of Science, Rehovot, Israel

Abstract. Translation validation is an alternative to the verication of
translators (compilers, code generators). Rather than proving in advance
that the compiler always produces a target code which correctly imple-
ments the source code (compiler verication), each individual translation
(i.e. a run of the compiler) is followed by a validation phase which veries
that the target code produced on this run correctly implements the sub-
mitted source program. In order to be a practical alternative to compiler
verication, a key feature of this validation is its full automation .
Since the validation process attempts to \unravel" the transformation
eected by the translators, its task becomes increasingly more dicult
(and necessary) with the increase of sophistication and variety of the
optimizations methods employed by the translator. In this paper we ad-
dress the practicability of translation validation for highly optimizing,
industrial code generators from Signal, a widely used synchronous lan-
guage, to C. We introduce new abstraction techniques as part of the
automation of our approach.

1 Introduction

A signicant number of embedded systems contain safety-critical aspects. There
is an increasing industrial awareness of the fact that the application of for-
mal specication languages and their corresponding verication/validation tech-
niques may signicantly reduce the risk of design errors in the development of
such systems. However, if the validation eorts are focused on the specica-
tion level, the question arises how can we ensure that the quality and integrity
achieved at the specication level is safely transferred to the implementation
level. Today's process of the development of such systems consists of hand-coding
followed by extensive unit and integration-testing.
The highly desirable alternative, both from a safety and a productivity point
of view, to automatically generate code from veried/validated specications,
has failed in the past due to the lack of technology which could convincingly
demonstrate to certication authorities the correctness of the generated code.
Although there are many examples of compiler verication in the literature (see,
? This research was done as part of the ESPRIT project SACRES and was supported
in part by the Minerva Foundation and an infra-structure grant from the Israeli
Ministry of Science and Art
?? Preliminary versions of some parts of this paper were published before in [17], [19]
and [20]