Advertisement
Published in:
2015 | OriginalPaper | Chapter
Translation Validation for Clock Transformations in a Synchronous Compiler
Authors : Van Chan Ngo, Jean-Pierre Talpin, Thierry Gautier, Paul Le Guernic
Published in: Fundamental Approaches to Software Engineering
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Translation validation was introduced as a technique to formally verify the correctness of code generators that attempts to ensure that program transformations preserve the semantics of input program. In this work, we adopt this approach to construct a validator that formally verifies the preservation of clock semantics during the
Signal
compiler transformations. The clock semantics is represented as a first-order logic formula called
clock model
. We then introduce a
refinement
which expresses the preservation of clock semantics, as a relation on clock models. Our validator does not require any instrumentation or modification of the compiler, nor any rewriting of the source program.