Loïc Besnard

Thierry Gautier

Paul Le Guer- Nic

Huafeng Yu

Yue Ma

Christophe Junke

Adnan Bouakaz

Sun Ke

Keywords: phases . . . . . . . . . . primitive operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Synchronous Program Transformed Program Executable Code (C, Java) Lexical Analysis Syntax Analysis Semantic Analysis Intermediate Code Code Generation Optimization _SEQ_TRA.SIG C/C++, Java Clock Calculation, Boolean Abstraction Scheduling

Synchronous languages such as SIGNAL, LUSTRE and ESTEREL are dedicated to designing safety-critical systems. Their compilers are large and complicated programs that may be incorrect in some contexts, which might produce silently bad compiled code when compiling source programs. The bad compiled code can invalidate the safety properties that are guaranteed on the source programs by applying formal methods. Adopting the translation validation approach, this thesis aims at formally proving the correctness of the highly optimizing and industrial SIGNAL compiler. The correctness proof represents both source program and compiled code in a common semantic framework, then formalizes a relation between the source program and its compiled code to express that the semantics of the source program are preserved in the compiled code.

INTRODUCTION

Synchronous programming languages such as SIGNAL, LUSTRE and ESTEREL propose a formal semantic framework to give high-level specification of safety-critical software in automotive and avionics systems [START_REF] Berry | The foundations of esterel[END_REF][START_REF] Le Guernic | Programming real-time applications with signal. another look at real-time programming[END_REF][START_REF] Halbwachs | A synchronous language at work: the story of lustre[END_REF][START_REF] Jackson | A direct path to dependable software[END_REF]. As other programming languages, synchronous languages are associated with a compiler. The compiler takes a source program, analyses and transforms it, performs optimizations, and finally generates executable code in a general-purpose programming language (e.g., C, C ++ , or JAVA). This compilation process is depicted as in Figure 1.1.

However, a compiler is a large and very complex program which often consists of hundreds of thousands, if not millions, lines of code, divided into multiple sub-systems and modules. Moreover, compiler modules often interact in very complex ways, and the design and implementation of a compiler is a substantial engineering task. The compilation process involves many analyzes, program transformations and optimizations. Some transformations and optimizations may introduce additional information, or constrain the compiled program. They may refine its meaning and specialize its behavior to meet a specific safety or optimization goal. Consequently, it is not uncommon that compilers silently issue an incorrect result in some unexpected context or inappropriate optimization goal. For example, the GNU Compiler Collection (GCC) is a compiler produced by GNU Project supporting several languages. GCC has been widely used in software development. It is also available for most embedded platforms. Although it has a long history of development and review by many people, no programmer can assert that it is always right in any context; see the list of bugs which have been found at GCC Bugzilla [START_REF]Gcc bugzilla[END_REF]. Considering bug number 15549, for instance, GCC will compile the expression b < c as (b == 0)&(c! = 0) into the following program, which always aborts. An incorrectly compiled program like the one above will most likely invalidate the safety properties that were secured on the source program. Yet, it is natural to require a compiler to guarantee the preservation of the source program's semantics, hence the safety properties are secured on it.

Correctness of compilation

Proving the correctness of a compiler can be based on the examination of the developed compiler's source code itself, meaning that a qualification process applies on the develop-ment of the compiler, the source of the compiler, and/or the compiler's output. Qualifying a compiler is rare because of the tremendous administrative effort involved. Qualification amounts to demonstrate compliance with all recommendations and objectives specified in the certification standards for safety-critical softwares: DO-178C and its European equivalent ED-12 [START_REF]Software considerations in airborne systems and equipment certification[END_REF]. Although DO-178 has been successful in industry, the cost of complying with it is significant: the activities on verification it incurs may well cost seven times more than the development effort needed [START_REF] Rushby | New challenges in certification for aircraft software[END_REF]. A more traditional method is therefore to solely inspect or formally verify the compiler's output. This task requires less unitary effort, but has to be repeated every time a new target code is generated. For instance, the work of Blanchet et al. [START_REF] Blanchet | Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software[END_REF][START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF] provides a method to design and implement a special-purpose abstract interpretation based static program analyzer for the verification of safety critical embedded real-time software. And the static program analyzer ASTRÉE [START_REF]Astrée. The static program analyzer[END_REF] aims at proving the absence of run time errors (RTE) in the generated C code of the synchronous data-flow compiler from LUSTRE programs. One last resort is hence to formally verify the correctness of the compiler itself.

A compiler is a computer program that reads an input program in one source language and translates it into a semantically equivalent refined program in another target language, Figure 1.2. The structure of a compiler consists of two parts:

Analysis The analysis part creates an intermediate representation of the source program and stores information about the source program in a data structure, the symbol table.

Synthesis The synthesis part generates the desired output program from the intermediate representation and information stored in the symbol table.

We usually call the analysis part the front end of the compiler, and the synthesis part its back end.

Fig. 1.2 Phases of compiler design

Suppose a specification of the properties that a computer program must satisfy when executed, e.g., its pre and post-conditions. It may describe interactions and relationships among program components (e.g., program variables, functions,...). The program is said to be correct with respect to its inputs and outputs if for all program executions with inputs satisfying the required specification. This definition applies for a compiler as well. There are two fundamental principles in design and implementation of a compiler which have to be fulfilled [START_REF] Cooper | Engineering a Compiler[END_REF]:

The compiler must preserve the meaning of the program being compiled.

The compiler must improve the input program in some discernible way.

For example, consider the compilation of an arithmetic expression, onto a stack-machine, in the form of one address code. Compilation assumes the presence of a stack of operands. Operations pop operands from the stack, evaluate them and push the result back onto the stack. For instance, an integer multiplication takes the top two elements from the stack and pushes their product onto the stack. Stack-machine code of the expression (x + 2) * y would be as follows:

Listing 1.2 Stack-machine code of (x + 2) * y 1 push x 2 push 2 3 add 4 push y 5 multiply

In order to prove the correctness of this compilation, one can develop an interpreter that feeds test operations and parameters to the compiler and interprets the source and compiled program to check output equality. For the stack-machine code generation, evaluating a source expression with test inputs should yield the same result as the value on top of the stack in the interpreted address code.

In this line of research, Sheridan's paper [START_REF] Sheridan | Practical testing of a c99 compiler using output comparison[END_REF] is a good survey on compiler testing. ACE [START_REF]Ace supertest suite[END_REF] provides the SUPERTEST compiler test and validation suite which is a large collection of self-testing programs. The certifying compilation [START_REF] Necula | Proof-carrying code[END_REF] attests that the generated object code satisfies the properties established on the source program by generating concrete evidences along the compilation into object code.

Systematic compiler verification techniques use formal methods. Formal methods advocate the use of a mathematical framework for the specification, development and verification of software and hardware systems. For the purpose of compiler verification, there are two approaches, in general, to prove the software correctness:

Formal compiler verification Specifying the intended behavior of the compiler in a formal specification language and building a proof that the compiler satisfies behavioral equivalence or refinement.

Translation validation Proving that each run of the compiler preserves the semantics of the source program in the generated code.

We shall discuss these two approaches in Section 1.2 and Section 1.3, and their application to the translation validation to a multi-clocked synchronous data-flow compiler in Section 1.4.

Formal compiler verification

In the context of software systems, formal verification is a problem of proving the correctness of a system with respect to the desired properties, using formal methods. The verification process consists of constructing an abstract mathematical model of the system behavior and of providing a formal proof on that model. There are several mathematical objects which may be used to construct the abstract model of a system, such as finite state machines, labeled transition systems, Petri nets, automaton, process algebra, and formal semantics of programming languages.

Formal verification can be done though many approaches. One such approach is deductive verification. It consists of providing deductive proofs that a system behaves in a certain way that is described in the specification, with the aid of either interactive theorem provers (such as HOL [START_REF] Camilleri | Reasoning with inductively defined relations in the hol theorem prover[END_REF][START_REF] Gordon | Introduction to hol: A theorem proving environment for higher order logic[END_REF], ISABELLE [START_REF]Isabelle proof assistant[END_REF], or COQ [START_REF]Coq proof assistant[END_REF]), or an automated theorem prover. It often requires to have knowledge of the system mechanism and why the system works correctly, and then convey this information to the verification process.

Another approach is model checking [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching time temporal logic[END_REF][START_REF] Clarke | Automatic verification of finie-state concurrent systems using temporal logic specifications[END_REF][START_REF] Clarke | Automatic verification of finie-state concurrent systems using temporal logic specifications[END_REF][START_REF] Quielle | Specification and verification of concurrent systems in cesar[END_REF]. It involves building an abstract model of the system and ensure that the system model complies with specified requirements by exploring all its accessible states. The system to be verified is often represented in temporal logics, such as Linear Temporal Logic (LTL) or Computational Tree Logic (CTL). The verification process produces a confirmation that the system model conforms to requirements or a counterexample that can be used to locate and eliminate an error. The main disadvantage of this approach is that it does not in general scale to large systems due to the state explosion problem. Some techniques must be used to deal with this problem including abstract interpretation, symbolic simulation and abstract refinement [START_REF] Cousot | Abstract interpretation frameworks[END_REF][START_REF] Cousot | Abstract interpretation and application to logic programs[END_REF][START_REF] Cousot | Refining model checking by abstract interpretation[END_REF].

A new variant of model checking is inspired by recent advances in efficiently solving propositional satisfiability problems (or SAT). Bounded model checking (BMC) [START_REF] Biere | Symbolic model checking without bdds[END_REF][START_REF] Clarke | Bounded model checking using satisfiability solving[END_REF] encodes the fact that potential executions of the system model do not conform to the specification in incremental fashion as propositional satisfiability formulas. The bounded number of evaluation steps is increased as long as the resulting propositional formula is satisfiable. Then a concrete counterexample can be extracted as a trace of system states leading to an error state in the system model.

Another approach is to use inductive reasoning to prove that a system conforms to its specification. The advances in solvers based on Satisfiability Modulo Theories (SMT) have been useful in checking systems inductively. With these solvers, systems can be modeled efficiently, require fewer limitation on representation of the specifications, while still meeting significant performance. In inductive approach, the transition relation of system a property are encoded as logic formulas. Then, it checks that the property is satisfied at initial state as the base case. If the base case holds true, take the assumption that the property holds for some state and prove that it holds for next state as well.

As usual, formal compiler verification is the problem of proving that the behavior of a compiler meets certain specifications. For instance, a compiler of arithmetic expressions for stack machines has to verify that the result of an evaluated operation is the same as that on top of the machine code's stack after execution. A formal compiler verification consists of establishing the given correctness property between source program and its compiled program. In our case, a correctness property should be that, if a source program has well-defined semantics, then it should be observationally equivalent to its generated code. Establishing this correctness property usually consists of:

• Specifying the intended behavior of a compiler in a specification language. This language is defined deterministically based on formal, deductive logic. The specification of the compiler is expressed in terms of the representation of the source and the compiled programs.

• Building a proof, based on some mathematical reasoning and automated proving techniques, to show that the compiler satisfies its model of intended behavior.

Given a source program A, the compilation of a compiler can be considered as a function Cp from a set of source programs to the set of compiled programs and the compilation error: P s -→ P c ∪ {Error}. We denote the compiled program of A by Cp(A) = C and the compilation error by Cp(A) = Error. In other words, for every source program, the output of the compilation is either a compiled program or an error. Then the semantic equivalence between the compiled program and the source program is ensured by the correctness of the compiler. Following the above conception of formal compiler verification, a compiler is a formally verified compiler if it is accompanied with a formal proof of the following theorem [START_REF] Leroy | Formal certification of a compiler back-end, or: Programming a compiler with a proof assistant[END_REF].

∀A ∈ P s ,C ∈ P c , Cp(A) = C ⇒ Correct(A,C) (1.1)
where Correct(A,C) denotes the correctness property between the source program A and its compiled program C.

Therefore, formal compiler verification formally ensures the correctness of the compiler. It makes sure that all guarantees obtained on the source program are preserved in the compiled program. This is particularly important if the compiler is used in development of safety-critical embedded systems, since the safety requirements for the development tools (e.g., compilers, translators,...) that translate programs are very high and require the most rigorous verification methods.

Translation validation

In the translation validation approach, the compiler is not verified. Instead, a validator is associated with the compiler to verify the correctness of each run of the compiler.

The notion of translation validation was first introduced by Pnueli et al. in [START_REF] Pnueli | Translation validation[END_REF] as an approach to verify the correctness of translators (compilers, code generators). The main idea of translation validation is that instead of proving the correctness of the translator, each individual translation (e.g., run of the code generator) is followed by a validation process which checks that the target program correctly implements the source program. It first constructs the formal models of both the source and compiled programs capturing their semantics. Then, it tries to establish a refinement relation between the formal models of the source and target program. If the compiled program behaves differently than the source program then one cannot establish that relation. Fortunately, the compilation scenario should provide a counter-example to help correcting the compiler error.

A verification framework which adopts translation validation benefits from the following features:

• The verification framework does not modify or instrument the compiler. It treats the compiler as a "black box" (as long as there is no error in it). It only considers the input program and its compiled result. Hence, it is not affected by updates and modifications to the compiler, as long as its data-structures remain the same.

• In general, the validator is much simpler and smaller than the compiler. Thus, the proof of correctness of the validator takes less effort than the proof of the compiler.

• The verification process is fully automated.

• The validator can be scaled to large programs, in which we represent the desired program semantics with our scalable abstraction and use efficient techniques to achieve the expected goals: traceability and formal evidence.

A verification framework which adopts the translation validation approach consists of the components depicted in Figure 1. [START_REF] Ackerman | Solvable cases of the decision problem[END_REF].

Model builder

The model builder defines a common semantic representation to capture the semantics of the source program and the compiled program of the translator. The outputs of this module are the formal models of these programs (e.g., they can be a kind of labeled transition system, or a first-order logic formula).

Analyzer The analyzer first formalizes the notion of "correct implementation" as a refinement relation. This relation expresses that the semantics of the source program is preserved during the compilation. This relation is defined based on the common semantic representation of the model builder. The analyzer also provides an automated proof method which allows to prove the existence of the refinement between the formal models. If the analyzer successfully proves the existence of the refinement, a proof script will be created. Otherwise, it will generate a counter-example. For example, in the work of Pnueli et al., the semantics of the source program and its compiled program are represented as Synchronous Transition Systems (STS). That is the common semantic framework. Given two STSs, they formalize the concept of "correct translation" as a refinement relation for them which expresses that the semantics of the source program is preserved in the compiled program. The refinement is checked by the use of a solver and the proof script is also generated.

Contributions

Considering the compiler of the synchronous data-flow language SIGNAL, the compilation process can be divided into three phases as depicted in Figure 1.4. It consists of a sequence of code transformations and optimizations. Some transformations are optimizations that rewrite the code to eliminate inefficient expressions. The transformations may be seen as a sequence of morphisms rewriting SIGNAL programs to SIGNAL programs, meaning that the intermediate representations produced by the compiler are written in SIGNAL. The final steps, C or JAVA code generation, are simple morphisms over the ultimately transformed program. show that it is possible to construct a validator that is plugged to the compiler in such a way it can provide formal correctness guarantees comparatively strong to these which could be obtained by proof assisted formal compiler verification.

Clock calculation and Boolean abstraction

Write C to denote the compiled program and Error to denote the compilation error of a source program A. Consider a validator Val which adopts the translation validation approach. The validator can be represented as a function from the set of pairs of a source program and its compiled program to the set of Boolean values: P s ×P c -→ B. The validator that we want to build satisfies the following property:

∀A ∈ P s ,C ∈ P c ,Cp(A) = C,Val(A,C) = true ⇒ Correct(A,C) (1.2)
We now associate each run of the compiler Cp with the validator Val. The following function Cp Val defines a formally verified compilation process from P s to P c and the compilation error. The verification of the derived compiler Cp Val reduces to the verification of the associated validator Val, meaning that the compiler does not need to be verified and can be considered as a black box. The following trivial theorem is the base of our line of work in this dissertation.

Cp Val (A) =          C if Cp(A) = C
Theorem 1 If the validator Val satisfies the property 1.2, then the derived compiler Cp Val is formally verified in the sense of Theorem 1.1.

It is obvious to prove globally that the source program and its final compiled program have the same semantics. However, we believe that a better approach is to separate concerns and prove each analysis and transformation stage separately with respect to ad-hoc datastructures to carry the semantic information relevant to that phase.

In the case of the SIGNAL compiler, the preservation of the semantics can be decomposed into the preservation of clock semantics at the clock calculation phase and that of data dependencies at the static scheduling phase, and, finally, value-equivalence of variables at the code generation phase. Figure 1.5 shows the integration of this verification framework into the compilation process of the SIGNAL compiler. For each phase, the validator takes the source program and its compiled counterpart, and constructs the corresponding formal models of the programs.

Then, it checks the existence of the refinement relation to prove the preservation of the considered semantics. If the result is that the relation does not exist then a "compiler bug" message is emitted. Otherwise, the compiler continues its work.

Preservation of clock semantics

The first verification stage focuses on proving that all clock relations associated with signals in the source and transformed program are equivalent. We propose two approaches to implement this verification, one based on model checking and the other on SMT solving.

In the first approach, the clock semantics of the source and transformed programs are represented by Polynomial Dynamical Systems (PDSs). A PDS is a system of equations, in which the coefficients of equations range over Z/ 3 Z. The notion of "correct implementation" is formalized as a PDS refinement. An automated proof method based on the simulation technique is provided for checking the existence of this refinement.

In the second approach, the clock semantics of the source and transformed programs are formally represented as clock models. A clock model is a first-order logic formula that characterizes the presence/absence status of all signals in a SIGNAL program at a given instant. Given two clock models, a clock refinement between them is defined which expresses the semantic preservation of clock semantics. A method to check the existence of clock refinement is defined as a satisfiability problem which can be automatically and efficiently proved by an SMT solver.

Let Cp sig and Val clk be the functions which define the SIGNAL compiler and a validator, respectively. The following function defines a formally verified compiler for the clock calculation and Boolean abstraction phase. We write C ⊑ clk A to denote that there exists a refinement between A and C.

Cp sig

Val clk (A) =

         C if Cp sig (A) = C

Preservation of data dependency

Given two signals in a source program, the aim of this work is to prove that data dependenies between them are preserved in the scheduled program. This verification also ensures that if there is no deadlock in the source program, then there is no deadlocks in the scheduled one either.

In order to do that, the data dependencies among signals are represented by a common semantic framework, called Synchronous Data-flow Dependency Graph (SDDG). A SDDG is a labeled directed graph, in which each node is a signal or a clock and each edge represents the dependency between nodes. Each edge is labeled by a clock expression called clock constraint at which the dependency between two extremity nodes is effective. The notion of "correct implementation" is formalized as a dependency refinement relation between graphs. This relation expresses the semantic preservation of data dependencies. It is implemented using an SMT solver to check the existence of the refinement relation.

Let Val dep be the function which defines a validator. The following function defines a formally verified compiler for the static scheduling phase of the SIGNAL compiler. We denote the fact that C refines A by C ⊑ dep A.

Cp sig

Val dep (A) = Given a SDVG, assume that we want to show that two variables have the same value. We simply need to check that they are represented by the same sub-graph, meaning that they point to the same graph node. If all output signals in the source program A and the corresponding variables in the generated C program have the same value, then we say that C refines A, denoted by C ⊑ val A.

         C if Cp sig (A) = C
Let Val val be the function which defines a validator. The following function defines a formally verified compiler for the code generation phase.

Cp sig

Val val (A) =

         C if Cp sig (A) = C

Towards a formally verified SIGNAL compiler

The derived SIGNAL compiler that is associated by the validator, denoted by Val, in Figure 1.5 can be defined by the following function from P s to P c and the compilation error.

Cp sig

Val (A) =                           
• Chapter 5 provides a method to prove the preservation of data dependencies. We define the common semantic frameworks to capture the data dependencies among variables in the programs, called Synchronous Data-flow Dependency Graph. Given the formal representations of data dependencies, we formalize the notion of "correct implementation" as a refinement relation between graphs.

• Chapter 6 presents a method based on the translation validation approach to prove the preservation of value-equivalence of variables between a source SIGNAL program and its generated C code. The computation of variables in the programs is represented as a Synchronous Data-flow Value-Graph. Value-equivalence of variables is validated by the normalization of graphs.

• Chapter 7 summarizes our work and details some directions of future research.

CHAPTER 2 RELATED WORK IN COMPILER VERIFICATION

The story of compiler verification began in 1967 with Mc.Carthy and Painter [START_REF] Mccarthy | Correctness of a compiler for arithmetic expression[END_REF] presenting the correctness proof for an algorithm compiling arithmetic expressions into machine language, and then with Milner's mechanized logical proof of a compiler in [START_REF] Milner | Proving compiler correctness in a mechanized logic[END_REF].

Mc.Carthy and Painter proposed a method to prove the correctness of a simple compiling algorithm. The input language of the compiler contains arithmetic expressions formed from constants and variables. The expressions allow only one operator, addition. The compiled code is written in an assembly-like language whose instructions are li (load immediate), load, sto (store), and add. For example, (x +3)+(x +(y+2)) is compiled into the following assembly code: The semantics of the source language is given by the following formula:

value(e, ξ ) = if isconst(e) then val(e) else if isvar(e) then c(e, ξ ) else if issum(e) then value(s1(e), ξ ) + value(s2(e), ξ )

where isconst(e), isvar(e) and issum(e) are predicates that check that an expression e is a constant, a variable or the sum of two expressions, and ξ is a state vector. The state vector associates the registers of the machine with their content. There are two functions on state vectors: c(x, η) denotes the content of register x in machine state η. a(x, α, η) denotes the state vector that is obtained from the state vector η by updating the content of register x to α, leaving other registers unchanged. Two state vectors η 1 and η 2 are equal except for variables in A, written

η 1 = A η 2 if x ̸ ∈ A, c(x, η 1 ) = c(x, η 2 ).
In the same way, the semantics of the object code is given as follows. It describes the state vector η that results from executing an instruction.

step(s, η) = if isli(s) then a(ac, arg(s), η) else if isload(s) then a(ac, c(adr(s), η), η)
else if issto(s) then a(adr(s), c(ac, η), η) else if isadd(s) then a(ac, c(adr(s), η) + c(ac, η), η) where isli(s), isload(s), issto(s) and isadd(s) are predicates to check that an instructor s is load immediate, load, store, and add, respectively. And the state vector that results from executing the program p with the state vector η, is given as follows:

outcome(p, η) = if null(p) then η else outcome(rest(p), step( f irst(p), η))
The compiler is defined by a function from the abstract syntax of the source language to the abstract syntax of the object code. The semantics of the compiling algorithm is given by the following formula:

compile(e,t) = if isconst(e) then mkli(val(e)) else if isvar(e) then mkload(loc(e, map)) else if issum(e) then compile(s1(e),t) * mksto(t) + compile(s2(e),t + 1) * mkadd(t) Symbol t stands for the index of a register in the state vector. All variables are stored in the state vector at indexes less than t, so that registers at index t and above are available for temporary storage. Instructions are named mkli, mkload, mksto and mkadd. The operation p 1 * p 2 denotes the program obtained by appending sub-program p 2 at the end of p 1 .

Assume that there is a map loc(e, map) which associates each expression e to a location in the memory map of the machine. The compiling algorithm is correct if executing the compiled program puts ends up with the value of the compiled expression in the accumulator. No registers except the accumulator and those with addresses ≥ t should be affected. This can be expressed as follows:

If c(loc(v, η)) = c(v, ξ ) then outcome(compile(e,t), η) = t a(ac, value(e, ξ ), η).
This work illustrates the main steps to formally prove the correctness of a simple compiler. First, one needs to formalize the semantics of the source language and compiled code, and then the compilation algorithm. Then, the definition of correct compilation has to be specified and a theorem proved to demonstrate that it is satisfied by the algorithm.

Since this pioneering work, many proofs of program correctness have been published, using techniques based on testing or on formal methods; see [START_REF] Dave | Compiler verification: A bibliography[END_REF] for a detailed survey.

Compiler verification based on testing

Trust regarding the correctness of a compiler's translation of source code into object code can be established by the validation of the compiler itself or by testing the compiler's output. For instance, the SUPERTEST suite [START_REF]Ace supertest suite[END_REF] is one of the most comprehensive test and validation suite to verify compilers. It contains a large collection of more than 3 millions test programs. These program are self-testing when compiled and run. They are be divided into the following classes:

• Conformance test: to test compilation of the basic constructs of the programming language.

• Early compiler bugs: derived from bugs found in earlier compilers that tend to occur repeatedly.

• Negative tests: to ensure that compilers handle errors in programs accurately.

• Stress tests: to seek the limits of the compiler in terms of sizes, number of basic blocks, live variables, etc., that the compiler handles.

• Generated tests: to systematically exploring combinations of operators, types, storage classes and constant values.

• Tests for the C ++ Standard Library: These tests verify both conformity with the standard [START_REF]Standard for programming language c++[END_REF]130] and correctness of the implementation. The correctness of the compiler's translation of source code into object code can alternatively be based on the examination of the compiler's output through the methodology proposed by the DO-178 standard. This provides user a way to demonstrate that the properties established in the source code still hold in the object code. In order to fulfil this objective, DO-178 recommends a proof that requirements at source-code level can be traceable down to the object code [START_REF] Brown | Guidance for using formal methods in a certification context[END_REF][START_REF] Ledinot | Formal methods and compliance to the do-178c/ed12c standard in aeronautics[END_REF], including the integration of software onto its hardware execution platform.

The form of verification which is required by DO-178 is based on high-level requirements, such as "HLR1: the program is never in error state E1", and low-level requirements, such as "LLR1: function F computes output O1, ..., On from inputs I1, ..., Im". For both HLRs and LLRs, the DO-178 guidance requires compliance and robustness verification. These verifications can be done either by testing or by using formal verification as indicates the new standard, DO-178C, also known as DO-333 [START_REF]Formal methods supplement to do-178c and do-278a[END_REF].

The compliance verification focuses on the intended nominal behavior of a compiler. The robustness verification focuses on the behaviors outside the nominal behaviors (e.g., the compilers are free of runtime errors such as out-of-range array elements, deallocation of null pointer, over-flow).

The new version of DO-178 permits to replace part of testing with formal verification. For instance, AIRBUS uses formal analysis tools to compute the worst case execution time and maximum stack usage of executable programs [START_REF] Souyris | Formal verification of avionics software products[END_REF] in order to comply with some DO-178 requirements. Compliance and robustness verifications can also be proved by using formal methods. For instance, HLR1 can be expressed as a temporal logic formula on traces of execution and an observer tool can check that the error state is unreachable.

Compiler verification based on formal methods

There are two approaches, in general, to prove the correctness of a compiler using formal methods. One approach consists of specifying the intended behavior of the compiler in a specification language as a formal model and of building a proof to show that the compiler behaves exactly as prescribed by requirements. The second approach consists of examining the source and compiled programs in order to prove that, for each run of the compiler, the semantics of the source program is preserved. Many correctness proofs of compiler implementations based on the two above approaches have been carried out, formal verification of the compiler itself [START_REF] Blazy | Formal verification of coalescing graphcoloring register allocation[END_REF][START_REF] Chirica | Towards compiler implementation correctness proofs[END_REF][START_REF] Polak | Compiler verification and specification[END_REF][START_REF] Thatcher | More on advice on structuring compilers and proving them correct[END_REF] or the verification of its compiled code [START_REF] Heffter | Towards proof generating compilers[END_REF][START_REF] Klein | A machine-checked model for a java-like language, virtual machine and compiler[END_REF][START_REF] Leinenbach | Towards the formal verification of a c0 compiler[END_REF][START_REF] Necula | Translation validation for an optimizing compiler[END_REF][START_REF] Pnueli | Translation validation[END_REF][START_REF] Pnueli | Translation validation: From signal to c[END_REF][START_REF] Rinard | Credible compilation[END_REF][START_REF] Zuck | Voc: A translation validator for optimizing compilers[END_REF]. A recent and typical example of compiler correctness proof is [START_REF] Blazy | Formal verification of coalescing graphcoloring register allocation[END_REF]. In this example, the correctness of the whole Iterated Register Coalescing (IRC) algorithm [START_REF] George | Iterated register coalescing[END_REF] is formally verified. The verification process works in cooperation with the proof assistant COQ. The register allocation via graph coloring which was invented by Chaitin et al. [START_REF] Chaitin | Register allocation via coloring[END_REF] is widely used in compiler implementation. However, since IRC was published in 1996, several mistakes have been reported in some of its implementations.

The input of IRC is an interference graph and a palette of colors, the output is the colored graph. In [START_REF] Blazy | Formal verification of coalescing graphcoloring register allocation[END_REF], the interference graph is first defined in a purely functional language, GALLINA, and implemented in the COQ prover. Then IRC is written in GALLINA. The implementation of the abstract interference graph and the operations of the algorithm are formally proved to be correct. The verified program is translated automatically into OCAML code that can be plugged in the COMPCERT compiler to provide correct register allocation.

A compiler is a large and very complex program which often consists of hundreds of thousands, if not millions, lines of code, and is divided into multiple sub-systems and modules. In addition, each compiler implements a particular algorithm in its own way. Consequently, that makes two main drawbacks of the formal verification of the compiler itself approach. First, constructing the specifications of the actual compiler implementation is a long and tedious task. Second, the correctness proof of a compiler implementation, in general, cannot be reused for another compiler.

To deal with this drawbacks of formally verifying the compiler itself, one can prove that the source program and the compiled program are semantically equivalent, which is the approach of translation validation. The principle of translation validation is as follows: for a given input sample, the source and the compiled programs will give corresponding execution traces. These traces are equivalent if they have the same observation. An observation is a sequence (finite or infinite) of values (e.g., values of variables, arguments, returned values,...). The compilation is correct if for any input, the source and the compiled programs have observationally equivalent execution traces.

A pioneering contribution to this area was the work of Pnueli et al. [START_REF] Pnueli | Translation validation[END_REF][START_REF] Pnueli | Translation validation: From signal to c[END_REF] to prove the correctness of the code generator from SIGNAL programs to C programs. Pnueli et al. formalize the semantics of a SIGNAL program and the generated C code in terms of Synchronous Transition Systems (STS). A STS consists of the set of states, the set of initial sates and a transition relation. A running of program is represented by a computation of STS which is an infinite sequence of states σ = ⟨s 0 , s 1 , s 2 , ...⟩ such that s 0 is an initial state and s i+1 is the successor state of s i , for all i ∈ N. And the set of all possible computations represents the semantics of the program. Given a computation σ , an observation is an infinite sequence of values by applying the observation function on each state of σ . Then, the authors formalize the concept of "correct translation" as a refinement between two STSs which expresses that the semantics of the source program is preserved at the compiled program, meaning that for any observation of the STS of the compiled program, it is also the observation of the STS of the source program. The refinement is generated as a set of verification conditions, and it is proved by the use of a solver such as SMT solver.

Zuck et al. [START_REF] Leviathan | Validating software pipelining optimizations[END_REF][START_REF] Pnueli | Validation of interprocedural optimization[END_REF][START_REF] Zuck | Validation of optimizing compilers[END_REF][START_REF] Zuck | Voc: A translation validator for optimizing compilers[END_REF] introduce a methodology to validate optimizations by generating a set of verification conditions and using a theorem prover. The main idea of their work is that the validator generates a set of verification conditions based on an invariant for intra-procedural optimizations. The invariant for an intra-procedural optimization is composed of:

• A relation between the nodes in the control-flow graphs.

• A relation between the program states (e.g., contents of registers, stacks, heaps,...).

• Invariants for the individual input and output programs. This set of verification conditions indicates the program equivalence for finite slices of program executions. That implies that the optimized program is a correct refinement of the input program.

A representative example is the COMPCERT project [START_REF]Compcert c verified compiler[END_REF]. The COMPCERT compiler is a formally verified compiler for C language. The compiler is mostly written in the functional programming language GALLINA. The implementation is formally verified and automatically translated into OCAML code by COQ. Some representative works of the project are carried out by Blazy et al. [START_REF] Blazy | Which c semantics to embed in the front-end of a formally verified compiler? Tools and Techniques for Verification of System Infrastructure[END_REF][START_REF] Blazy | Formal verification of a c compiler front-end[END_REF][START_REF] França | Formally verified optimizing compilation in acg-based flight control software[END_REF]] and Leroy et al. [START_REF] Leroy | Formal certification of a compiler back-end, or: Programming a compiler with a proof assistant[END_REF][START_REF] Leroy | A formally verified compiler back-end[END_REF][START_REF] Leroy | Formal verification of a c-like memory model and its uses for verifying program transformations[END_REF].

For instance, Blazy et al. proposed a correctness proof of the translation from a large subset of C language, Clight, into the intermediate language, Cminor, the front-end of the COMPCERT compiler. The semantic preservation for the translation is formalized as a simulation for a Clight program and the translated Cminor program. The semantics of Clight and Cminor, the memory state model, and the simulation are formalized in COQ. A Clight program contains a list of functions, a list of global variables declarations, and the entry point of the program, the main function. A Cminor is structured like the Clight language with some differences (e.g., the operators are not overloaded, type casting is explicit,...). The semantics of Clight and Cminor are both specified using big-step operational semantics. We omit the details of evaluation judgements for Clight, Cminor, and the translation. The interested readers should refer to the original article.

To prove the correctness of the translation, the notion of memory injections α is introduced to map a block reference b to either None, meaning that block has no counter part, or a sub-block b ′ at offset δ in Cminor memory state. The memory injections are used to define the relation between Clight values v and Cminor v ′ and the relation between Clight and Cminor memory states, denoted by

α ⊢ v ≈ v ′ , α ⊢ M ≈ M ′ , respectively. A memory injection α ′ extends the memory injection α, denoted by α ′ ≥ α; it is defined by ∀b, α ′ (b) = α(b) ∨ α(b) = None.
A matching relation EnvMatch(γ, α, E, M, E ′ , sp) is introduced to match a Clight environment E and memory state M to a Cminor environment E ′ and reference to a stack block sp, since the Clight environment E maps local variables to references of blocks containing the values of the variables, while the Cminor environment E ′ maps directly local variables to the values. γ is a translation environment which reflects the placement of Clight variables. A call stack cs is a list of tuples (γ, E, E ′ , sp). A call stack is global consistent with respect to a memory state M and memory injection α, written CallInv(α, M, cs) if EnvMatch(γ, α, E, M, E ′ , sp) holds for all elements (γ, E, E ′ , sp) of the stack.

Assuming suitable consistency conditions over the call stack, the semantics of the Clight program is preserved in the translated Cminor program if the generated Cminor expressions and statements evaluate in ways that simulate the evaluation of the corresponding Clight expressions and statements. The definition of this simulation relation is given as follows. Let G ′ be the global Cminor environment obtained from the global Clight environment G. Assume that CallInv(α, M, (γ, E, E ′ , sp).cs) and α ⊢ M ≈ M ′ . Then, there exists a Cminor environment E ′ 1 , a Cminor memory state M ′ 1 and a memory injection

α 1 ≥ α such that • (R-values) If G, E ⊢ a, M ⇒ v, M 1 , ∃v ′ such that G ′ , sp, L ⊢ R γ (a), E ′ , M ′ → v ′ , E ′ 1 , M ′ 1 and α 1 ⊢ v ≈ v ′ . • (L-values) If G, E ⊢ a, M ⇒ l loc, M 1 , ∃v ′ such that G ′ , sp, L ⊢ L γ (a), E ′ , M ′ → v ′ , E ′ 1 , M ′ 1 and α 1 ⊢ Vptr(loc) ≈ v ′ . • (Statements) If G, E ⊢ s, M ⇒ out, M 1
, and τ r is the return type of the function,

∃out ′ such that G ′ , sp ⊢ S γ (s), E ′ , M ′ → out ′ , E ′ 1 , M ′ 1 and α 1 , τ r ⊢ out ≈ out ′ .
Furthermore, the final memory states M 1 and

M ′ 1 satisfy CallInv(α 1 , M 1 , (γ, E, E ′ 1 , sp).cs) and α 1 ⊢ M 1 ≈ M ′ 1 .
The semantic preservation theorem is given as follows. Note that it is assumed that programs always terminate. The semantic preservation is stated as follows: Assume the Clight program p is well-typed and translated without errors to a Cminor program p ′ . If ⊢ p ⇒ v, and if v is an integer or float value, then ⊢ p ′ → v.

Another example is the work of Leroy [START_REF] Leroy | A formally verified compiler back-end[END_REF] which describes the correctness proof of the code generation, the back-end of the COMPCERT compiler, from a low-level, imperative intermediate language Cminor into optimized POWERPC assembly code, using the COQ proof assistant.

Inspired by the work of COMPCERT compiler, the formal development of a code generator based on the correct-by-construction components method is carried out in the GE-NEAUTO project [START_REF] Geneauto | Geneauto project[END_REF][START_REF] Izerrouken | Machine checked sequencer for critical embedded code generator[END_REF][START_REF] Izerrouken | Use of formal methods for building qualified code generator for safer automotive systems[END_REF]. The GENEAUTO code generator takes as input a functional description of a system specified in a high-level modeling language (e.g., SIMULINK, STATEFLOW) and generates C code as output.

The GENEAUTO toolset is composed of several tools which represent either systems or code models using XML file format. The project focuses on proving the correctness of the block sequencer tool which assigns a unique execution order to each block in the system specified in a high-level modeling language. The block sequencer has to satisfy the set of sequencing constraints which contains:

• Data-flow: blocks computing values used by another block must be executed first.

• Control-flow: caller blocks must be executed during callee blocks after their inputs have been computed.

• Sequential blocks: read part of Unit Delay blocks are executed before the write one.

• User priority: two blocks can be sequenced using a user defined priority if they cannot be sequenced with the above constraints.

• Graphical position: if two blocks cannot be sequenced with the above constraints and there is no user defined priority, they are sequenced based on the graphical position defined implicitly in the graphical model.

All the sequencing constraints are translated into formal specification. The specification is written in the functional language GALLINA within the COQ prover. The verification phase proves the conformance to the set of sequencing constraints based on the translation validation approach, meaning that the sequential generated code correctly implements the system specified in a high-level modeling language with respected to the set of sequencing constraints.

Another recent work inspired by the COMPCERT project is the correctness proof of the translation from a small subset of SIGNAL language into the intermediate language, clock guarded actions [START_REF] Brandt | Integrating system descriptions by clocked guarded actions[END_REF][START_REF] Brandt | Representation of synchronous, asynchronous, and polychronous components by clocked guarded actions[END_REF], the front-end of a forthcoming verified compiler [START_REF] Yang | A verified transformation: from polychronous programs to a variant of clocked guarded actions[END_REF]. The semantics of both input and output of the translation are expressed as trace semantics. Then, the formal development of the translation follows a correct-by-construction components method, meaning that for any translation from a primitive operator of SIGNAL into the corresponding clock guarded actions structure, it preserves the trace semantics. The translation is written in the functional programming language GALLINA and formally proved to be correct. The verified translation is translated automatically into OCAML code as the formally verified compiler prototype of the SIGNAL language.

Gamatié et al. [START_REF] Feautrier | Enhancing the compilation of synchronous data-flow programs with combined numerical-boolean abstraction[END_REF][START_REF] Gamatié | Static analysis of synchronous programs in signal for efficient design of multi-clocked embedded systems[END_REF][START_REF] Gamatié | Towards static analysis of signal programs using interval techniques[END_REF] introduce an approach to statically analyze SIGNAL programs for efficient code generation. The main idea of their work is that the clocks and clock relations are formalized as first-order logic formulas with the help of interval-Boolean abstraction technique. This work aims to remove the dead-code segments (e.g., segment of code to compute a data-flow which is always absent). The dead-code segments are identified by detecting the existence of empty clocks, mutual exclusion of two or more clocks, or clock inclusions. The reasoning on the logic formulas is done using a SMT solver. With the interval abstraction, the analysis of clock hierarchy is more precise and more efficient when dealing with the numerical expressions. The common semantics frameworks which are used to construct the translation validation of clock models and SDDGs in Chapter 4 and Chapter 5 are based on their interval abstraction technique. CHAPTER

SYNCHRONOUS DATA-FLOW LANGUAGES

This chapter introduces general concepts about reactive systems, the synchronous approach to model reactive systems and the formal verification background. Section 3.1 first defines what reactive systems are. It presents some main features as well as some important issues that designers have to deal with during the design of these systems. Section 3.2 is an introduction to the synchronous approach in designing reactive systems, which has been proposed as a useful approach to describe embedded and safety-critical systems, particularly in automotive and avionics. Then, in Section 3.3, we consider an instance of synchronous programming language, the SIGNAL language. The polychronous semantic model which is used to define the formal semantics of the language is studied as well.

Embedded, reactive and real-time systems

There are several definitions of embedded systems, here, we consider the definition which is proposed by Henzinger and Sifakis [START_REF] Henzinger | The embedded systems design challenge[END_REF]. The definition in [START_REF] Gamatié | Designing Embedded Systems with the Signal Programming Language[END_REF] which conforms to theirs is given as follows:

Definition 1 (Embedded system) An embedded system is a special-purpose computer system that consists of a combination of software and hardware components that are subject to physical constraints. Such physical constraints come from the system's environment and its execution platform.

This computer system is embedded as part of a complete device that includes hardware and mechanical parts. Its function is specific, in contrast to a general-purpose computer, such as a personal computer (PC), which is designed to be flexible with a wide range of services.

In general, embedded systems are designed based on micro-controllers (i.e CPUs with integrated memory and/or peripheral interfaces). Physically, embedded systems can range from portable devices such as digital watches, smart phones, to large devices such as factory controllers, hybrid vehicles, and avionics. They can have one micro-controller or multi micro-controllers.

Reactive systems

In [START_REF] Harel | On the development of reactive systems[END_REF], Harel and Pnueli introduced the term "reactive system", it is commonly accepted to describe a computer system that continuously interacts with its environment at a speed which is determined by this environment. One example of reactive systems is embedded systems that can be seen anywhere in our modern life. And they are reactive in nature.

Definition 2 (Reactive system) A reactive system is a computer system that continuously interacts with its environment at a speed which is determined by this environment.

It is different from a "transformational system", which is a system whose role is to make some outputs computed from some inputs. A transformational system terminates in a finite time duration (e.g., a compiler). It also distinguishes from interactive systems, which interact continuously with their environment, but at their own speed (e.g., operating systems).

Reactive systems range from very simple systems (e.g., a system with sensors to record the temperature) to complex systems. Many reactive systems are safety-critical, meaning that even minor errors are unacceptable, and minor errors can make systems go disastrously wrong. For instance, health-related systems, automotive systems, airplane flight control systems and control systems for nuclear plants are reactive systems. The main features of reactive systems which are pointed out in [START_REF] Benveniste | Hybrid dynamical systems theory and the signal language[END_REF][START_REF] Berry | Real-time programming: Special purpose or general purpose languages[END_REF][START_REF] Berry | Synchronous programming of reactive systems, an introduction to esterel[END_REF][START_REF] Halbwachs | Synchronous Programming of Reactive Systems[END_REF] are the following: Concurrency A reactive system involves concurrency because of the concurrency between the system and its environment. In addition, it is convenient to consider a system as a set of components, which cooperate to achieve the desired behavior. In practice, some systems are implemented on parallel and distributed architectures in order to improve their performance and reliability.

Strict time requirements

The systems have to satisfy the requirements about their input rate and their input/output response time. These constraints must be expressed in the system specifications. In order to check these constraints, the evaluation of execution time has especially to be precise during the system design.

Deterministic The outputs of the system are entirely determined by their input values and by the occurrence times of these inputs. The systems will always behave in the same manner, with respect to their expected functional requirements. This makes the validation of the system much easier.

Reliability This can be considered as the most important feature of reactive systems. Errors in reactive systems can be catastrophes, and involve human lives. Therefore, reactive systems require especially rigorous design methods, for instance, formal verification must be considered.

Mixing of hardware and software In many cases, reactive systems are partly implemented by hardware and software, in which they cooperate to achieve the intended function.

Real-time systems

A reactive embedded system has to guarantee a response within a finite and specified time interval, often referred to as "deadline", is called a real-time system. Process control, manufacturing support, command and control are all example application areas where real-time systems have a major role. We consider the definition of a real-time system in [START_REF] Gamatié | Designing Embedded Systems with the Signal Programming Language[END_REF] which is given as follows: Definition 3 (Real-time system) A reactive embedded system is a real-time system when its correctness depends not only on the logical results of its associated computations, but also on the delay after which the results are produced.

It is common to distinguish between hard and soft real-time systems. Hard real-time systems are those whose responses occur strictly within the specified deadline. If the deadlines are missed the system will be failed. Soft real-time systems are those where response time is required to be within the specified deadline, however the system still function correctly if deadlines are occasionally missed. Note that most systems combine both hard and soft real-time subparts.

For example, the flight control system of an aircraft is a hard real-time system. A data acquisition is an example of soft real-time system, as it is defined to sample the data from an input sensor at regular time intervals, but it can tolerate some intermittent delays.

Time is obviously a critical resource for real-time systems and must be managed effectively. Unfortunately, it is very difficult to design and implement a system that guarantees timing requirements under all possible circumstances. Therefore, real-time systems are usually constructed with respect to "worst-case execution time". In general, real-time programming languages provide the developer real-time control facilities. These control facilities specify times at which actions are to be performed and have to be completed. They also provide the developer solutions to respond to the situations where the timing requirements cannot be met, and the situations where the timing requirements are changed dynamically.

Synchronous programming

To implement a reactive system, one can use a single loop, of the form in Listing 3.1. This programming scheme is called "event driven" since each reaction is triggered by an input event from the environment. Listing 3.1 "Event driven" These two programming schemes do not deeply differ, but they correspond to different intuitive points of view. In the following, we shall present the approaches to describe the implementation of the above programming schemes (see [START_REF] Berry | Real-time programming: Special purpose or general purpose languages[END_REF][START_REF] Halbwachs | Synchronous Programming of Reactive Systems[END_REF] for a more complete representation).

Classical approaches

Reactive systems can be modeled using task-based models, finite automata, Petri-net-based models, or classical concurrent and real-time programming languages.

Task-based models The system is designed as a set of sequential tasks. The tasks are activated and controlled by a real-time operating system. The communication between tasks is implemented using a shared memory. The time requirements are guaranteed by means of scheduling instructions (interrupts, priorities,...) and are not directly expressed in the description. Analysis, debug, and maintenance of such systems is hard. In addition, realtime operating systems are generally nondeterministic, which in turn makes programming more difficult.

Finite automata

The control kernel of a reactive system is often implemented using an automaton. From a current state, the automaton selects a transition, calls the corresponding sequential tasks, and changes its states for the next reaction. A reaction is neither loop nor recursion with no interrupt and no overhead. The "worst case" execution time can be accurately bounded. Automata are deterministic and can be automatically analyzed by numerous available formal verification techniques [START_REF] Clarke | Automatic verification of finie-state concurrent systems using temporal logic specifications[END_REF][START_REF] Fernandez | An implementation of an efficient algorithm for bisimulation equivalence[END_REF][START_REF] Queille | Specification and verification of concurrent systems in cesar[END_REF]. However, writing an automaton with a big number of states is a difficult and error-prone task. Automata, in general, do not directly support hierarchical design and concurrency. Consequently, they are very difficult to use to design complex systems. A small change to the system specifications might involve a complete modification and rewriting of the automaton.

Petri-net-based models Petri-nets can be used to express concurrency in a natural way [START_REF] Reisig | Petri nets[END_REF]. But they lack modular structure and often lack determinism. Consequently, it is suitable for small systems.

Classical concurrent and real-time programming languages Concurrent and real-time programming languages such as ADA [START_REF]The programming language ada reference manual[END_REF] or OCCAM [START_REF]The occam programming manual[END_REF] take concurrency as a primary concern and support modularity. Communication and synchronization mechanisms use rendez-vous, and fifo queues. However, they are essentially asynchronous and nondeterministic: the time taken between the possibility of a communication and its actual achievement can be arbitrary and is unpredictable. And the order is also unpredictable when several communications take place. In addition, the formal verification of program written in these languages is often not feasible because asynchrony makes the formal description of the program very large [START_REF] Berry | Real-time programming: Special purpose or general purpose languages[END_REF].

The synchronous approach

The synchronous approach naturally expresses concurrency. It is deterministic and hierarchical, and possible to use automatic verification tools.

In the synchronous approach [START_REF] Benveniste | Synchronous programming with events and relations: the signal language and its semantics[END_REF][START_REF] Benveniste | The synchronous languages 12 years later[END_REF], time is abstracted by a partial order relation. Events occurring during the same reaction are regarded as simultaneous. Time only increments from one reaction to the next one. Durations between events are not specified. Under this abstraction, computation is considered to take zero time. A synchronous program is supposed to instantly and deterministically react to the events from its environment. To illustrate the basic idea of synchronous approach, we consider an example in [START_REF] Halbwachs | Synchronous Programming of Reactive Systems[END_REF] which requires the two following constraints:

• "The train must stop within 10 seconds"

• "The train must stop within 100 meters" These constraints can be expressed in completely different ways if the physical time is considered. In the synchronous model, they will be expressed by the following constraints:

• "The event stop must precede the 10th next occurrence of the event second"

• "The event stop must precede the 100th next occurrence of the event meter"

The notion of instant is understood as a logical instant: the history of a system is a totally ordered sequence of logical instants. At each instant, there are zero, one, or several events that can occur. Events which occur at the same instants are considered as simultaneous. In the duration between two instants, nothing happens either in the system or its environment. Finally, all the processes of the system have the same knowledge of the events occurring at a given instant.

The SIGNAL language

Synchronized data flow

We shall consider the concept of synchronized data flow as described in [START_REF] Besnard | Compilation of polychronous data-flow equations[END_REF][START_REF] Gamatié | Polychronous design of embedded real-time applications[END_REF][START_REF] Guernic | Polychrony for system design[END_REF]. Based on the data flow semantics given by Kahn [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF] as functions over flows, in the following expression, y is the greatest sequence of values a ′ t + a t where a ′ is the sub-sequence of strictly positive values in the sequence of values a.

1 if a > 0 then 2 x = a 3 y = x + a
If we consider an execution where the edges are FIFO queues [START_REF] Gostelow | Some relationships between asynchronous interpreters of data-flow language[END_REF], if a is a finite or infinite sequence of zero or negative values, the queue associated with a grows or grows forever, the queue associated with x is always empty. Assume that the queue consists only of a single cell [START_REF] Dennis | Data flow schemas[END_REF], the execution to compute a value of the sequence associated with y cannot perform as soon as a negative value appears on the input since the first operand does not hold a value (the sequence associated with a is empty), meaning that there exists a deadlock. To deal with this situation in the context of embedded system design, synchronized data flow introduces synchronizations between occurrences of flows. The absent of value is usually represented by nil, null, or the symbol ⊥.

An overview of the language

SIGNAL [START_REF] Benveniste | Hybrid dynamical systems theory and the signal language[END_REF][START_REF] Gautier | Signal, a declarative language for synchronous programming of real-time systems[END_REF] is a polychronous data-flow language that allows the specification of multiclocked systems. It handles unbounded sequences of typed values x(t),t ∈ N, called signals, denoted as x. Each signal is implicitly indexed by a logical clock indicating the set of instants at which the signal is present, noted C x . At a given instant, a signal may be present where it holds a value, or absent where it holds no value (denoted by ⊥). Given two signals, they are synchronous if and only if they have the same clock. In SIGNAL, a process (written as P or Q) consists of the synchronous composition (denoted by |) of equations over signals x, y, and z, written as x := y op z or x := op(y, z), where op is an operator. A program itself is a process.

Data domains Data types contain usual scalar types (Boolean, integer, float, complex, and character), enumerated types, array types, tuple types, and the special type event, subtype of the Boolean type which has only one value, true.

Operators The core language consists of two kinds of "statements" defined by the following primitive operators: first four operators on signals and last two operators on processes. The operators on signals define basic processes, with implicit clock relations, while the operators on processes are used to construct complex processes with the parallel composition operator.

• Stepwise functions: y := f (x 1 , ..., x n ), where f is a n-ary function on values, defines the extended stream function over synchronous signals as a basic process whose output y is synchronous with x 1 , ..., x n and ∀t ∈ C y , y(t) = f (x 1 (t), ..., x n (t)).

• Delay: y := x$1 init a defines a basic process such that y and x are synchronous, y(t 0 ) = a, and ∀t ∈ C y ∧ t > 0, y(t) = x(t -), where

t 0 = inf{t ′ |x(t ′ ) ̸ = ⊥} and t -= sup{t ′ |t ′ < t ∧ x(t ′ ) ̸ = ⊥}.
• Merge: y := x default z defines a basic process which specifies that y is present if and only if x or z is present, and that

y(t) = x(t) if t ∈ C x and y(t) = z(t) if t ∈ C z \C x .
• Sampling: y := x when b where b is a Boolean signal, defines a basic process such that ∀t ∈ C x ∩C b ∧ b(t) = true, y(t) = x(t), and otherwise, y is absent.

• Composition: If P 1 and P 2 are processes, then P 1 | P 2 , also denoted (|P 1 | P 2 |), is the process resulting of their parallel composition. This process consists of the composition of the systems of equations. The composition operator is commutative, associative, and idempotent.

• Restriction: P/x, where P is a process and x is a signal, specifies a process by considering x as local variable to P (i.e., x is not accessible from outside P).

Clock relations In addition, the language allows clock constraints to be defined explicitly by some derived operators that can be replaced by primitive operators above.

• Clock extraction: y := ˆx specifies that y is the clock of x with type event. It is equivalent to y := (x = x) in the core language.

• Synchronization: xˆ= y means that x and y have the same clock. It can be replaced by ˆx =ˆy.

• • Clock union: x ˆ+ y defines a clock as the union C x ∪ C y , which can be rewritten as ˆx defaultˆy.

• Clock intersection: x ˆ * y defines a clock as the intersection C x ∩ C y , which can be rewritten as ˆx whenˆy.

Dependency

Clock relation Let x, y be two signals and c be a Boolean signal, if at any instant t such that t ∈ C x ∩ C y ∩ C c and c(t) = true, setting a value to y cannot precede the availability of x, then we say that y depends on x at the condition c. We use x c -→ y to denote the fact that there is a dependency between y and x at the condition c. In particular, the following dependencies apply implicitly.

x C x C x -→ x c (Boolean signal) c [c] -→ [c], c [¬c] --→ [¬c] x c - → y [c] [c] -→ y y := f (x 1 , ..., x n ) x 1 C y -→ y ... x n C y -→ y C y = C x 1 ... C y = C x n y := x$1 init a C y = C x y := x when b x C y -→ y, b C y -→ C y C y = C x ∩ [b] y := x default z x C x -→ y, z C z \C x ---→ y C y = C x ∪C z
• Any signal is preceded by its clock.

• For a Boolean signal c, [c] and [¬c] depend on c. Let us comment this program. FB, and N are respectively input and output signals of type integer (line 2 and 3). FB is accepted, it is present, only when ZN becomes less than or equal to 1 (line 4). N is set to FB when its previous value is less than or equal to 1, otherwise it is decremented by 1 (line 5). ZN is defined as carrying the previous value of N and its initial value is 1) (line 6). ZN is a local signal (line 8). We can see that the clock of the output signal is more frequent than that of the input. This is illustrated in the following possible traces: 1 6 5 4 3 2 1 3 2 1 4 N 6 5 4 3 2 1 3 2 Program structure The language is modular, meaning that a process can be used as a basic pattern, by means of an interface that describes its parameters and its input and output signals. Moreover, a process can use other subprocesses, or even external parameter processes that are only known by their interfaces. For example, to emit three sequences of values FB i -1, ..., 2, 1 for all three positive integer inputs FB i , with i = 1, 2, 3, one can define the following process (in which, without additional synchronizations, the three subprocesses have unrelated clocks):

1 t . . . . . . . . . . 2 FB 6 ⊥ ⊥ ⊥ ⊥ ⊥ 3 ⊥ ⊥ 2 3 ZN

Semantics of the language

This section presents the operational and denotational semantics of the SIGNAL language. Operational semantics are classified in two categories: big-step semantics and small-step semantics [START_REF] Plotkin | The origins of structural operational semantics[END_REF]. Big-step semantics describe how the overall results of the executions are obtained. By opposition small-step semantics formally describe how the individual steps of a computation take place on an abstract machine. Denotational semantics [START_REF] Scott | Toward a mathematical semantics for computer languages[END_REF] formalize the meanings of programming languages by constructing mathematical objects (called denotations) that describe the meanings of expressions from the languages. Denotational semantics describe a valid program as a function from its inputs to its outputs. The operational and denotational semantics of SIGNAL were originally proposed by Benveniste et al. in [START_REF] Benveniste | Synchronous programming with events and relations: the signal language and its semantics[END_REF] and Le Guernic et al. in [START_REF] Guernic | Polychrony for system design[END_REF]. They are also presented by Gamatié in the book on designing embedded systems with the SIGNAL language [START_REF] Gamatié | Designing Embedded Systems with the Signal Programming Language[END_REF].

Operational semantics

Let X and V be a countable set of variables and their domain of values, respectively. The domain with the absent value is denoted by V ⊥ = V ∪ ⊥. A signal variable can be assigned values according to an environment that is defined as follows:

Definition 4 (Environment) Let X 1 ⊂ X be a set of signal variables, an environment associated with X 1 is defined as a function ε : X 1 → V ⊥ . This function assigns values to signals at each instant during an execution.

The set of environments associated with X 1 is written as ε X 1 . When the signal s is present, the environment assigns a value v ∈ V to s (denoted by s(v) ∈ ε, or ε(s) = v). Otherwise, s is associated with the special value, absent value (noted as s(⊥)). An environment where all signals are absent is denoted by ⊥ ε .

Definition 5 (Environment restriction) Consider an environment ε associated with X and a subset X 1 ⊆ X, the restriction written as ε X 1 is defined as follows:

ε X 1 : X \ X 1 → V ⊥ such that ∀x ∈ X \ X 1 , ε(x) = ε X 1 (x)
For example, we consider the following environment:

ε : {s 1 , s 2 , s 3 } → {v 1 , v 2 , v 3 , v 4 }; ε(s 1 ) = v 1 , ε(s 2 ) = v 2 , ε(s 3 ) = v 3
Then, the environment restriction ε s 2 is defined as:

ε s 2 : {s 1 , s 3 } → {v 1 , v 2 , v 3 , v 4 }; ε(s 1 ) = v 1 , ε(s 3 ) = v 3
The signal s 2 is not visible in the environment restriction.

Definition 6 (Environment composability) Let ε 1 ∈ ε X 1 and ε 2 ∈ ε X 2 be two environments. If for all signal variables x ∈ X 1 ∩ X 2 , ε 1 (x) = ε 2 (x)
, then they are composable and their composition ε 1 ⊕ ε 2 is defined as follows:

⊕ :ε X 1 × ε X 2 → ε X 1 ∪X 2 (ε 1 , ε 2 ) → ε 1 ∪ ε 2
For example, we consider the following environments:

ε 1 :{s 1 , s 2 , s 3 } → {v 1 , v 2 , v 3 , v 4 }; ε(s 1 ) = v 1 , ε(s 2 ) = v 2 , ε(s 3 ) = v 3 ε 2 :{s 1 , s 4 , s 5 , s 6 } → {v 1 , v 4 , v 5 , v 6 }; ε(s 1 ) = v 1 , ε(s 4 ) = v 4 , ε(s 5 ) = v 5 , ε(s 6 ) = v 6
Since ε 1 and ε 2 are composable, we have their composition environment as follows:

ε 1 ⊕ ε 2 :{s 1 , s 2 , s 3 , s 4 , s 5 , s 6 } → {v 1 , v 2 , v 3 , v 4 , v 5 , v 6 }; ε(s 1 ) = v 1 , ε(s 2 ) = v 2 , ε(s 3 ) = v 3 , ε(s 4 ) = v 4 , ε(s 5 ) = v 5 , ε(s 6 ) = v 6
The operational semantics of the SIGNAL language is described by a labeled transition systems where the states are SIGNAL processes. It is given as follows:

C p 1 ε - → p 2
where p 1 and p 2 are processes, ε is an execution environment, and C is a precondition on p 1 , p 2 , and ε. We now define the operational semantics for all primitive operators of the language SIGNAL. Consider the environment in which all signals involved in a process p are absent. Hence, the process p never reacts. The operational semantics of this process can be represented by the following trivial rule:

p ⊥ ε -→ p
Stepwise functions Let p be the basic process y := f (x 1 , ..., x n ), the signal y is present and holds the value calculated by the expression f (v 1 , ..., v n ) when the signal x 1 , ..., x n are present and carry the values v 1 , ..., v n , respectively. The operational semantics of p is defined as follows: -----------------→ p When all signals are absent, the operational semantics is represented by the trivial rule.

p x 1 (v 1 ),...,x n (v n ),y( f (v 1 ,...,v n ))
Delay The operational semantics of the basic process p = y := x$1 init a is defined by the following transition rule. where p ′ = y := x$1 init v. The delay operator expresses a dynamic behavior in which the value of the signal x is memorized after each transition. The process p ′ memorizes the previous value v carried by x as the new initialization value for the next transition. The trivial rule is also applied for the delay operator.

Merge The semantics of merge operator, y := x default z, is defined by the following transition rules:

p x(v 1 ),z(⊥),y(v 1 ) ---------→ p p x(v 1 ),z(v 2 ),y(v 1 ) ---------→ p p x(⊥),z(v 2 ),y(v 2 ) ---------→ p p ⊥ ε -→ p
Sampling The semantics of sampling operator, y := x when b, is defined by the following transition rules:

p x(v),b(⊥),y(⊥) --------→ p p x(⊥),b(v b ),y(⊥) ---------→ p p x(v),b(true),y(v) ----------→ p p x(v),b(false),y(⊥) -----------→ p p ⊥ ε -→ p Composition Let p 1 , p 2 , p 3 ,
and p 4 be four processes within the environments ε 1 and ε 2 .

The operational semantics of the composition operator is defined as follows:

p 1 ε 1 -→ p 2 ; p 3 ε 2 -→ p 4 ; ε 1 and ε 2 are composable (p 1 | p 3 ε 1 ⊕ε 2 ---→ (p 2 | p 4 )
The upper part of the transition rule defines the condition at which the composition of two processes is possible (the two environments must be composable). The lower part describes the composition whenever this condition is satisfied.

Restriction Let p 1 and p 2 be two processes within an environment ε. The semantics of the process restriction is simply defined by restricting the visibility of the signals concerned in the transition environment. The operational semantics is defined as follows:

p 1 ε - → p 2 p 1 /x ε x -→ p 2 /x 3.3.3.2 Denotational semantics Let X, B = { f f ,tt}, V ⊇ B,
and T be a countable set of variables, a set of Boolean values ( f f and tt denote false and true, respectively), the domain of variables, and a dense set equipped with a partial order relation ≤. The elements in T are called tags. The partially ordered set (T , ≤) is a subset T ⊂ T such that:

• T is countable,
• T has a lower bound 0 for ≤,

• the partial order ≤ on T is well-founded.

We denote by C T the set of all chains C in T . Then, for a tag t ∈ C, min(C), max(C) and pred C (t) denote the minimum, maximum and the predecessor of t.

Definition 7 (Event, signal and behavior) Given a set T , an event e ∈ E is a relation between a tag and a value. A signal s ∈ S = T ⇀ V is a partial function defined on a chain of tags to a set of values. A behavior b ∈ B = X ⇀ S is a partial function that maps a signal name x ∈ X to a signal s ∈ S .

We write tags(s) and vars(b) to denote the domain of s and domain of b, respectively. Then, tags(b) = x∈vars(b) tags(b(x)) denote the tags of the behavior b. Therefore, x is present at instant t in behavior b can be formally expressed by t ∈ tags(b(x)).

For example, consider the following trace, we have:

1 t 0 t 1 t 2 t 3 t 4 t 5 t 6 t 7 t 8 t 9 ... 2 x 1 : 1 2 3 ... 3 x 2 : 1 2 3 ... 4 x 3 : 1 2 3 ... • X = {x 1 , x 2 , x 3 } • V = {1, 2, 3}
• T = {t 0 ,t 1 ,t 2 ,t 3 ,t 4 ,t 5 ,t 6 ,t 7 ,t 8 ,t 9 , ...}

• E = {e 0 = (t 0 , 1), e 1 = (t 1 , 1), e 2 = (t 2 , 1), e 3 = (t 3 , 2), e 4 = (t 4 , 2), e 5 = (t 5 , 2), e 6 = (t 6 , 3), e 7 = (t 7 , 3), e 8 = (t 8 , 3), ...}

• S = {s 1 = {e 0 , e 4 , e 6 , ...}, s 2 = {e 1 , e 5 , e 7 , ...}, s 3 = {e 2 , e 3 , e 8 , ...}}

• B = {(v 1 , s 1 ), (v 2 , s 2 ), (v 3 , s 3 )} The projection of a behavior b on a set X 1 ⊂ X of names, b | X 1 , is defined as follows: • vars(b | X 1 ) = X 1 • ∀x ∈ X 1 , b | X 1 (x) = b(x)
We write b /X 1 for the projection of b on the complementary of X 1 in vars(b). The empty signal is denoted by λ . 0

| X 1 = {(x, λ ) | x ∈ X 1 to denote the association of X 1 ⊂ X to the empty signal.
Definition 8 (Process) A process p ∈ P is a stretch-closed set of behaviors which have the same domain X (denoted by vars(p)). The synchronous composition of two processes p | q is defined by the set of behaviors that extend a behavior b ∈ p by the restriction c /vars(p) of a behavior c ∈ q provided that the projections of b and c on vars(p) ∩ vars(q) are equal.

p | q = {b ⊎ c /vars(p) | (b, c) ∈ p × q, b | vars(p)∩vars(q) = c | vars(p)∩vars(q) } Definition 9 (Stretching) A behavior c is a stretching of b, noted b ≤ B c, iff vars(b) =
vars(c) and there exists a bijection f : T → T such that:

• ∀t, u ∈ T ,t ≤ u ↔ f (t) ≤ f (u) • ∀C ∈ C , ∀t ∈ C,t ≤ f (t) • f orallx ∈ vars(b),tags(c(x)) = f (tags(b(x))) • ∀x ∈ vars(b), ∀t ∈ tags(b(x)), b(x)(t) = c(x)( f (t))
The stretching relation is a partial order on behaviors B. This provides an equivalence relation between two behaviors. For each primitive operator of SIGNAL, we describe its denotational semantics in terms of sets of behaviors. We denote by [[p]] the set of all possible behaviors of the process p.

Stepwise functions The denotational semantics of the stepwise functions, y := f (x 1 , ..., x n ), is defined as follows:

[[y := f (x 1 , ..., x n )]] = {b ∈ B | y,x 1 ,...,x n | tags(b(y)) = tags(b(x 1 )) = ... = tags(b(x n )) = C ∈ C \ / 0 ∀t ∈ C, b(y)(t) = [[ f ]](b(x 1 )(t), ..., b(x n )(t))}
The denotational semantics of the stepwise functions is the set of behaviors b such that:

• The tags of each signal x i represent the same chain C of tags.

• For each tag in C, the relation f holds between the values carried by the involved signals. We denote the stepwise interpretation of f by

[[ f ]].
Delay The denotational semantics of the delay operator, y := x$1 init a, is defined as follows:

[[y := x$1 init a]] = {0 | y,x } ∪ {b ∈ B | y,x | tags(b(y)) = tags(b(x)) = C ∈ C \ / 0 b(y)(min(C)) = a, ∀t ∈ C \ min(C), b(y)(t) = b(x)(pred C (t))}
The denotational semantics of the delay operator is the set of behaviors b such that:

• The tags of the signals y and x represent the same chain C of tags.

• At the initial tag of C, y holds the value a.

• For all other tag t in C, y holds the value that is carried by x at the predecessor of t.

Merge The denotational semantics of the merge operator, y := x default z, is defined as follows:

[[y := x default z]] = {b ∈ B | y,x,z | tags(b(y)) = tags(b(x)) ∪ tags(b(z)) = C ∈ C ∀t ∈ C, b(y)(t) = b(x)(t) if t ∈ tags(b(x)) else b(z)(t)}
The set of behaviors satisfy:

• The tags of the signals y is the union of those associated with x and z.

• The value taken by y is the value carried by x at any common tag of x and y. Otherwise, y takes the value carried by z.

Sampling The denotational semantics of the sampling operator, y := x when b, is defined as follows:

[[y := x when b]] = {b ∈ B | y,x,b | tags(b(y)) = {t ∈ tags(b(x)) ∩ tags(b(b)) | b(b)(t) = tt} = C ∈ C ∀t ∈ C, b(y)(t) = b(x)(t)}
The denotational semantics of the sampling operator consists of the behaviors which satisfy:

• The tags of the signals y is the intersection of the tags of x and the set of tags at which b carries the value true.

• At each tag of y, it holds the value carried by x.

Composition The composition of two processes p and q is the stretch closure of the behaviors b such that the projections of these behaviors on vars(p) and on vars(q) give behaviors in p and q, respectively. The denotational semantics is given as follows:

[[p | q]] = ({b | b | vars(p) ∈ p, b | vars(q) ∈ q}) *
Restriction The restriction of a process p over x is the stretch closure of the behaviors of p projected on the complementary set of {s}. The denotational semantics is defined as follows:

[[p/x]] = ({c | ∃b ∈ p ∧ c ≶ b /{x} }) * CHAPTER 4
TRANSLATION VALIDATION OF TRANSFORMATIONS

ON CLOCKS

Clocks and clock relations are used to represent all the control parts (e.g. activation events) and interaction between different components in a system. The control flow resulting from the analysis of clocks and clock relations is used to derive an optimized data-flow following the transformations of the compiler. Therefore, the correctness of clock analysis in the compilation of synchronous programs strongly impacts the quality of the compiled program.

In this chapter, we describe how the preservation of clock semantics can be proved based on the translation validation approach. It focuses on proving that for any transformation in the first phase of the SIGNAL compilation process, the source program and its compiled program have the same clock semantics. We propose two approaches based on model checking and the use of SMT solver.

In the first approach, the clock semantics of the programs are represented by Polynomial Dynamical Systems (PDSs) that is considered as a common semantic framework in our translation validation. A PDS refinement is formally formalized to express the concept of correct transformation and provide a method to prove the existence of this refinement based on the simulation technique.

In the second approach, the presence/absence status of all signals in a program at a given instant is deterministically characterized by a first-order logic formula with uninterpreted functions, called clock model. Given two clock models, a clock refinement between them is defined which expresses the preservation of clock semantics. A method to check the existence of clock refinement is defined as a first-order logic formula satisfiability problem.

We design a validator and plug it within the clock calculation and Boolean abstraction phase. Figure 4.1 shows the integration of this validator into the compilation process. The validator takes the source program and its compiled counterpart, and constructs the corre-sponding PDSs or clock models for the first and second approaches, respectively. It then checks the existence of PDS refinement or clock refinement depending on which approach is being used. If the result is that the relation does not exist then a "compiler bug" message is emitted. Otherwise, the compiler continues its work.

Fig. 4.1 A bird's-eye view of the verification process

The remainder of this chapter is organized as follows. Section 4.1, first, describes how the SIGNAL compiler calculates the clocks and makes the Boolean abstraction of synchronous programs to answer some important questions in the first phase compilation. Section 4.2 addresses the Z/ 3 Z encoding of signal clocks and values. In Section 4.3, we consider the formal definition of PDSs, the translation of SIGNAL programs into PDSs and translation validation of PDSs. Section 4.4 provides the definition of clock model, the encoding scheme from SIGNAL programs into clock models and the translation validation of clock models. We also address the mechanism of the verification process, the application of the verification process to the SIGNAL compiler, and its integration in the POLYCHRONY toolset [START_REF]Polychrony toolset[END_REF]. Section 4.5 presents some related works, concludes our work and outlines some future directions.

The clock calculus in SIGNAL compiler

Consider the first phase of the SIGNAL compilation process, the goal of this phase is calculating clocks of all signals, synthesizing clock relations, and providing a Boolean abstraction of a program. The compiled program is also written in SIGNAL language as depicted Figure 1.4. The compiler represents the clocks and clock relations as a system of equations. These equations are encoded in the finite field Z/ 3 Z of integers modulo 3, where -1 encodes the presence of a Boolean signal holding the value false, 0 encodes the absence of a signal, +1 encodes the presence of a Boolean signal holding the value true. The full encoding scheme of SIGNAL programs will be presented in Section 4.2 and Section 4.2.1.

The analysis of such a system of equations provides some important functions of the compiler [START_REF] Benveniste | Hybrid dynamical systems theory and the signal language[END_REF]. The first function of this phase is the detection of empty behavior and synchronization errors. If the system of equations has only one solution such that the empty clock is set to every signal, then the program cannot execute. For instance, we consider the following program:

1 (| x := a when ( a > 0) 2 | y := a when not ( a < 0) 3 | z := x + y 4 |) which induces [a > 0] = [¬(a > 0)] = C a \ [a > 0] (since x and y are synchronous), because [a > 0] ⊆ C a , we get C a = C x = C y = C z = / 0.
If the program can be executed but some inputs from the environment are not accepted, then the program can be deadlocked. This happens in the following program:

1 (| c := a > 0 2 | x := a when c 3 | y := x + a 4 |) which provides C a ∩ [c] = C a and C a = C c , implies that [c] = C c ,
which means that the input signal a must always be positive. In consequence of this constraint on the input, this program will be rejected if its environment provides a negative value for a which implies that the signal a is present, c is present and holds the value false and x is absent.

The other function of this phase is to construct the control flow of the program. Given a program, it may be established an order relation on the set of clocks: the clock of signal h is said to be greater than the clock of signal k if the set of instants of k is a sub-set of the set of instants of h (k is an under-sampling of h), denoted by C h ≥ C k . Equivalently, we say that the class C h dominates the class C k . The relation ≥ on the quotient set of signals by ˆ= (two signal are in the same class if and only if they are synchronous) is called a clock hierarchy [START_REF] Amagbegnon | Arborescent canonical form of boolean expressions[END_REF]. When the clock hierarchy has a unique highest class, then the program has a fastest rated clock (called the master clock) and the definitions of other clocks are expressed as under-samplings of the fasted rated clock. In this case, the status (presence/absence) of all signals is a pure flow function: this status depends neither on communication delays, nor on computing latencies.

A program which contains only one master clock is referred to as endochronous, meaning that there is a unique way to compute the clocks of its signals. Endochronous programs can be executed in a deterministic way [START_REF] Guernic | Polychrony for system design[END_REF]. If there exists more than one master clock, some parts of the program can run at independent rates. Consider the following example:

1 (| x := ( x$ init 0) + 1 2 | y := x when c 3 |) / x
We get the clock relation

C y = C x ∪ [c],
which leaves the clock of x and c unrelated. The signal x is not synchronized by any external signal, thus its computation rate is undetermined. As a result, the output y can be any subsequence of the sequence of integers. To make the program execute in a deterministic way, this program needs extra information from its environment (i.e., the clock of x needs to be synchronized by some external signal).

The synchronization space Z/ 3 Z

We denote by Z/ p Z[Z] the set of polynomials over variables Z = {z 1 , ..., z k } whose coefficients range over the finite field modulo p, Z/ p Z, with p prime. For a polynomial P ∈ Z/ p Z[Z], the solutions of the equation P(Z) = 0 are denoted by Sol(P).

We say that P 1 ≡ P 2 whenever Sol(P 1 ) = Sol(P 2 ). And the representative of Sol(P) of each ≡-equivalence class is called the canonical generator. In the rest of this chapter, we shall use the following notations, where P| z i =v is P obtained by instantiating any occurrence of variable z i by value v. P 1 -P p-1 P 1 ⊕ P 2 (P p-1

1 + P p-1 2 ) p-1 P 1 ⇒ P 2 {Z ∈ (Z/ p Z) k |P 1 (Z) = 0 ⇒ P 2 (Z) = 0} ∃z i P P| z i =1 * P| z i =2 * ... * P| z i =p ∀z i P P| z i =1 ⊕ P| z i =2 ⊕ ... ⊕ P| z i =p
Following the above notations, we can see that the solutions of P are defined as Sol(P) = (Z/ p Z) k \Sol(P). And the polynomial P 1 ⇒ P 2 has the same the set of solutions as P 1 * P 2 , or P 1 ⇒ P 2 ≡ P 1 * P 2 . The manipulations of polynomials over the finite field modulo p, with p prime can be found in [START_REF] Le Borgne | Dynamical systems over galois fields and control problems[END_REF].

We consider the finite field modulo 3, Z/ 3 Z = {-1, 0, +1}. This field holds some very interesting properties that are used to reason about properties of encoded statements. For instance, let x be an element in Z/ 3 Z and n ∈ N, then:

x 2n = x 2 x 2n+1 = x x + x = -x 1 x = x, ∀x ̸ = 0 x(1 -x 2 ) = 0 ( f (x 2 )) 2n = f (x 2 )
Our aim is to build a formal model which represents the behaviors of synchronous dataflow programs in terms of the presence of signals and the relations among signals. Let us, by the way of illustration, consider the basic SIGNAL process corresponding to the primitive sampling operator, y := x when b, where x and y are non-Boolean signals and b is a Boolean signal. This basic process expresses the following statements:

• if x is present, and b is present and holds the value true, then y is defined by the value of x,

• if x is absent, or b is absent, or b is present and holds the value false, then y is absent.

It shows that at a given instant, to express the control, we need to represent the status of the signals x, y and b. In this example, for the non-Boolean signals such as x, its status are: x is present and x is absent. For the Boolean signal b, its status are: b is present and holds the value false, b is present and holds the value true and b is absent. The principle is that the status of a signal can be encoded in the finite field modulo p = 3, Z/ 3 Z. This encoding scheme were proposed by Le Guernic et al. in [START_REF] Gamatié | Polychronous design of embedded real-time applications[END_REF][START_REF] Guernic | Polychrony for system design[END_REF] as a model of the synchronization relation. For a Boolean signal, its three possible status at a given instant are encoded as:

• present and false → -1,

• present and true → 1,

• absent → 0.

For a non-Boolean signal, it only encodes the fact that the value is present or absent (it does not encode value):

• present → ±1,

• absent → 0.

In this way, if x is the encoding of the signal x, its clock can be considered as x 2 : 1 if x is present; 0 if x is absent. Thus, for two synchronous signals x and y (they have the same clock), x and y satisfy the constraint equation:

x 2 = y 2 .

PDS model

Processes are translated into systems of polynomial equations over the finite field modulo p = 3, Z/ 3 Z, following the above encoding scheme. Each individual SIGNAL equation is translated into a polynomial equation. Since the language is defined from a few primitive operators, we only need to define the translation of these primitive operators to polynomial equations.

Stepwise functions

The functions which apply on signal values in the primitive stepwise functions are usual logic operators (not, and, or), numerical comparison functions (<, >, =, <=, >=, /=), and numerical operators (+, -, *, /). The encoding in the finite field modulo p = 3, Z/ 3 Z, of stepwise functions is given as follows:

• If x and y are Boolean signals:

y := not x -→ y = -x z := x and y -→ z = xy(xy -x -y -1) x 2 = y 2 z := x or y -→ z = xy(1 -x -y -xy) x 2 = y 2
• If x and y are non-Boolean signals:

y := f (x 1 , ..., x n ) -→ y 2 = x 2 1 = ... = x 2 n 4.2.

Delay

Considering the delay operator, y := x$1 init a, its encoding is given as follows:

• If x, y and a are Boolean signals:

y := x$1 init a -→      m.x ′ = x + (1 -x 2 )m.x y = x 2 m.x m.x = a
• If x, y and a are non-Boolean signals:

y := x$1 init a -→ y 2 = x 2
This encoding requires that at any instant, signals x and y have the same status (present or absent). If the signals are Boolean, it encodes the value of the output signal as well. Here, we introduce a memorization variable m.x that stores the last value of x. The next value of m.x is m.x ′ and it is initialized to a in m.x = a.

Merge

The encoding of the merge operator, y := x default z is given as follows:

• If x, y and z are Boolean signals:

z := x default y -→ z = x + (1 -x 2 )y
• If x, y and z are non-Boolean signals:

z := x default y -→ z 2 = x 2 + y 2 -x 2 y 2
For Boolean signals, the encoding equation can be interpreted as follows: if x is defined then z is defined and holds the same value as x (z = x + (1 -1)y = x). Otherwise, when y is defined and x is not, then z holds the same value as y (z = 0 + (1 -0)y = y).

Sampling

The encoding of the sampling operator, y := x when b, is given as follows:

• If x, y and z are Boolean signals:

y := x when b -→ y = x(-b -b 2 )
• If x, y and z are non-Boolean signals:

y := x when b -→ y 2 = x 2 (-b -b 2 )
The encoding of this operator for Boolean signals may be interpreted as follows: y holds the same value as x when b is defined and holds the value true (y = x(-1 -1) = x).

Composition

Consider the composition of two processes P 1 and P 2 . The encoding of φ (P 1 |P 2 ) in the finite field modulo p = 3, Z/ 3 Z, is the union of the encodings of P 1 and P 2 .

Restriction

The encoding of P/x is the same as the encoding of P. That means the local definitions do not affect the encoding in the finite field modulo p = 3, Z/ 3 Z.

Clock relations

Let us recall the rewriting of the clock relations. Following the above encoding scheme, we can obtain the following encoding for derived operators on clocks. Here, z is a signal of type event:

(z :=ˆx) = (x = x) -→ z = x 2 (xˆ= y) = (ˆx =ˆy) -→ x 2 = y 2 z := ( when b) = (b when b) -→ z = -b -b 2 z := (xˆ+ y) = (ˆx defaultˆy) -→ z = x 2 + (1 -x 2 )y 2 z := (xˆ * y) = (ˆx whenˆy) -→ z = x 2 y 2 z := (xˆ-y) = ( when (notˆy defaultˆx)) -→ z = x 2 (1 -y 2 )
The composition of the basic encodings of the SIGNAL primitive operators, presented in the above encoding scheme, constructs a polynomial dynamical system. Formally, the definition of PDS is given as follows:

Definition 12 (PDS) A PDS is a system of equations which is organized into three subsys-Translation validation of transformations on clocks tems of polynomial equations of the form:

     Q(X,Y ) = 0 X ′ = P(X,Y ) Q 0 (X) = 0
where:

• X is a set of n variables, called state variables, represented by a vector in

(Z/ 3 Z) n ,
• Y is a set of m variables, called event variables, represented by a vector in (Z/ 3 Z) m ,

• X ′ = P(X,Y ) is the evolution equation of the system. It can be considered as a vectorial function [P 1 , ...,

P n ] from (Z/ 3 Z) n+m to (Z/ 3 Z) n , • Q(X,Y ) = 0 is the constraint equation of the system. It is a vectorial equation [Q 1 , ..., Q l ],
• Q 0 (X) = 0 is the initialization equation of the system. It is a vectorial equation

[Q 0 1 , ..., Q 0 n ].
The equations of PDS have the following meaning:

• The initialization equation represents the initialization of signals in the program.

• The constraint equation is a set of equations which expresses the clock relations of the program. It is also considered as the invariant properties of the program.

• The evolution equation describes the evolution of state variables (corresponding to the delay operators) according to the logical time in the program. Therefore, it shows the dynamical behavior of the program.

Example

We

= x + (1 -x 2 ) * m.x 5 /* constraint equation */ 6 x = -zx; 7 zx = m.x * x 2 ; 8 a 2 = -x -x 2 ; 9 b 2 = -zx -zx 2

Translation validation of PDSs

To apply the translation validation to the transformations on clocks of the SIGNAL compiler, we capture the clock semantics of the original program and its transformed counterpart by means of PDSs that is proposed by Marchand et al. [START_REF] Marchand | Formal verification of signal programs: Application to a power transformer station controller[END_REF] to build a formal verification framework of SIGNAL programs. The semantics of PDSs is considered as the common semantics framework in our translation validation. Then, we introduce a refinement relation which expresses the preservation of clock semantics, as a simulation relation between two PDSs. We provide a method to check the existence of that simulation based on model checking technique which is implemented as a library of SIGALI checker [START_REF] Dutertre | Sigali: un système de calcul formel pour la vérification de programmes signal[END_REF].

Definition of correct transformation: PDS refinement

Given a PDS model over the finite field Z/ 3 Z, it can be viewed as an intensional Labeled Transition System (ILTS) [START_REF] Kouchnarenko | Intensional approaches for symbolic methods[END_REF] as in the following definition.

Definition 13 (ILTS) An intensional labeled transition system is a structure L = (Q,Y, I , T ), where Q is a set of states, Y is a set of m variables Y 1 , ...,Y m , I is a set of initial states, and The ILTS representation of a PDS can be obtained directly from the set of state variables, event variables, initialization, constraint and evolution equations as follows:

T ⊆ Q × Z/ 3 Z[Y]×Q is
• Q = D X , where D X = ∏ i∈[1,n] D x i = (Z/ 3 Z) n as the domain of a set of variables X = (x 1 , ..., x n ) • Y = Y, D Y = ∏ i∈[1,m] D y i = (Z/ 3 Z) m • I = Sol(Q 0 (X)) • (q, P q (Y ), q ′ ) ∈ T where P q (Y ) ≡ Q(q,Y ) ⊕ (P(q,Y ) -q ′ )
We write q P(Y ) --→ q ′ (or for short q P -→ q ′ ), instead of (q, P(Y ), q ′ ) ∈ T . Then ILTSs can be viewed as an "intensional" representation of classical LTSs, where the labels are tuples in (Z/ 3 Z) m : each arrow of the ILTS labeled by P(Y ) intensionally represents as many arrows labeled by some y ∈ Sol(P(Y )). The corresponding "extensional" LTS of an ILTS L is denoted by Ext(L), meaning that each arrow of L labeled by P(Y ) is represented by the number (the number of solutions of P(Y )) of arrows labeled by y ∈ Sol(P(Y )).

For example, we consider the PDS model in Listing 4.2. Its ILTS representation is given as follows:

• Q = {-1, 0, +1}) • Y = {a, b, x, zx} • I = Sol(m.x = -1) = {0} • (q, P q (Y ), q ′ ) ∈ T where P q (Y ) ≡ Q(q,Y ) ⊕ (P(q,Y ) -q ′ ), Q(q,Y ) = [x = -zx, zx = q * x 2 , a 2 = -x -x 2 , b 2 = -zx -zx 2 ], and
P(q,Y ) = x + (1 -x 2 ) * q
Definition 14 (Execution) Let L = (Q,Y, I , T ) be an ILTS. The infinite sequence σ = q 0 , y 0 , q 1 , y 1 , q 2 , y 2 , ..., where q i ∈ Q, y i ∈ D Y for each i ∈ N, is an execution of L if it satisfies the following requirements:

• q 0 ∈ I .

• There exists a polynomial P(Y ) such that (q i , P(Y ), q i+1 ) ∈ T ∧ y i ∈ Sol(P(Y )) for each i ∈ N.

We denote by σ act = y 0 , y 1 , y 2 , .... an action-based execution, ||L||, ||L|| act the sets of executions and action-based executions of the ILTS L, respectively.

Consider the two ILTSs

L A = (Q 2 ,Y, I 2 , T 2 ) and L C = (Q 1 ,Y, I 1 , T 1 )
, to which we refer respectively as the ILTS of the source program A and the ILTS of the compiled program C produced by the compiler. We assume that they have the same set of event variables. In case the set of event variables of the compiled model is different from the set of event variables of the source model, we consider only the set of common event variables and the different event variables are considered as hiding events as described in [START_REF] Pinchinat | Symbolic abstractions of automata and their application to the supervisory control problem[END_REF]. That means that we ensure that the clocks of common signals in the source and compiled programs are the same after the transformations.

In our case, the set of action-based executions models the clock semantics of the program. The set of action-based executions reflects the status of the clocks and clock relations in the program. The strongest notion of clock semantics preservation during compilation is that the source program A and its compiled program C have exactly the same clock semantics, meaning that their corresponding intensional labeled transition systems have the same set of action-based executions:

∀σ act . (σ act ∈ ||L C || act ⇔ σ act ∈ ||L A || act ) (4.1)
The compiled program C has fewer behaviors than the source program A. For instance, compilers do transformations, optimizations for removing or eliminating some behaviors of the source program (e.g., eliminating subexpressions, trivial clock constraints). To address these issues, we relax the requirement 4.1 as follows:

∀σ act . (σ act ∈ ||L C || act ⇒ σ act ∈ ||L A || act ) (4.2)
Requirement 4.2 says that all action-based executions of L C are acceptable executions of L A . And we say that L C refines L A w.r.t action-based executions, denoted by L C ⊑ Pds L A . In the next section we will present a method to establish the refinement between the two given ILTSs L C and L A .

Proving refinement by simulation

We now discuss an approach to automatically prove that a compiler preserves the clock semantics of the source program during its compilation, in the sense of refinement relation. Given two ILTSs L A and L C , we use a symbolic simulation [START_REF] Kouchnarenko | Intensional approaches for symbolic methods[END_REF] for the two ILTSs to establish that L C ⊑ Pds L A . The symbolic simulation satisfies the property that if there exists a symbolic simulation for

(L C , L A ) then L C ⊑ Pds L A . Definition 15 (Symbolic simulation) Let L C = (Q 1 ,Y, I 1 , T 1 ) and L A = (Q 2 ,Y, I 2 , T 2 ) be two ILTSs. A symbolic simulation for (L C , L A ) is a binary relation R ⊆ Q 1 × Q 2 which
satisfies the following properties:

1. ∀q 1 ∈ I 1 , ∃q 2 ∈ I 2 , (q 1 , q 2 ) ∈ R.
2. for any (q 1 , q 2 ) ∈ R it holds that: if q 1 P -→ q ′ 1 there exists a finite set of transitions (q 2

P i -→ q i
2 ) i∈I (where I is a set of indexes) with Condition (1) asserts that every initial state of L C is related to an initial state of L A . According to condition (2), for every transition of the state q 1 which is labeled by the set of events (or actions) represented by Sol(P(Y )), there exist some transitions of the state q 2 which are labeled by the same set of events. And it states that every outgoing transition from q 1 must be matched by outgoing transitions from q 2 . Thus, Definition 15 captures exactly classic action-based simulation definition of standard LTSs. Since symbolic simulation is closed under arbitrary unions, there is a greatest symbolic simulation. In the following parts, when we talk about symbolic simulation, we imply talking about the greatest symbolic simulation. L C is simulated by L A (or equivalently, L A simulates L C ), denoted by L C ≼ L A , if there exists a symbolic simulation for (L C , L A ). Given two states q 1 ∈ Q 1 and q 2 ∈ Q 2 , the state q 1 is simulated by q 2 , denoted q 1 ≼ q 2 , if there exists a symbolic simulation R for (L C , L A ) with (q 1 , q 2 ) ∈ R. In that case, we say that the two states "q 1 and q 2 are similar".

• (P ⇒ ∏ i∈I P i ) ≡ 0 and • (q ′ 1 , q i 2 ) ∈ R,
Definition 16 Let L C = (Q 1 ,Y, I 1 , T 1 ) and L A = (Q 2 ,Y, I 2 , T 2 ) be two ILTSs.
We define a family of binary relations

≼ j ⊆ Q 1 × Q 2 by induction over j ∈ N. • ≼ 0 Q 1 × Q 2 .
• q 1 ≼ ( j+1) q 2 iff ∀(q 1 , P, q ′ 1 ) ∈ T 1 , there exists a finite set of transitions (q 2 , P i , q i 2 ) i∈I with (P ⇒ Π i∈I P i ) ≡ 0 ∧ q ′ 1 ≼ j q i 2 , ∀i ∈ I, where I is a set of indexes.

Based on the above definition, we can now have the following theorem which gives us a method to compute the greatest symbolic simulation for two ILTSs.

Theorem 2 Let L C = (Q 1 ,Y, I 1 , T 1 ) and L A = (Q 2 ,Y, I 2 , T 2 ) be two ILTSs.
1. There exists a symbolic simulation for (L C , L A ) iff there exists a simulation for the corresponding "extensional" LTSs, (Ext(L C ), Ext(L A )).

Then for all q

1 ∈ Q 1 and q 2 ∈ Q 2 , q 1 ≼ q 2 iff q 1 ( n∈N ≼ n ) q 2 , where ( n∈N ≼ n ) = ≼ 0 ∩ ≼ 1 ∩...∩ ≼ n .
Proof 1 (1) Following an approach which is similar to [START_REF] Kouchnarenko | Intensional approaches for symbolic methods[END_REF],

(2) Since the number of state variables, event variables and the value domain of a PDS are finite then its ILTS is finite. Symbolic simulation over a finite ILTS (therefore finitely branching) is the limit of nested projective equivalences. Thus we can use the same proof method as in [START_REF] Milner | Operational and algebraic semantics of concurrent processes[END_REF] for strong simulation. We omit the proof here.

The use of a symbolic simulation as a proof method to establish the refinement between the two given models L C and L A is stated in the following theorem.

Theorem 3 Let L C = (Q 1 ,Y, I 1 , T 1 ) and L A = (Q 2 ,Y, I 2 , T 2 ) be two ILTSs. If there exists a symbolic simulation for (L C , L A ), then L C ⊑ Pds L A .
Proof 2 The proof of Theorem 3 is trivial, following Lemma 1.

Lemma 1 Let L C and L A be ILTSs, R is a symbolic simulation for (L C , L A ), and (q 1 , q 2 ) ∈ R. Then for each infinite (or finite) execution σ 1 = q 0,1 , y 0,1 , q 1,1 , y 1,1 , q 2,1 , y 2,1 , ... starting in q 0,1 = q 1 there exists an execution σ 2 = q 0,2 , y 0,2 , q 1,2 , y 1,2 , q 2,1 , y 2,2 , ... from state q 0,2 = q 2 of the same length such that (q j,1 , q j,2 ) ∈ R and y j,1 = y j,2 for all j.

Proof 3 Let σ 1 = q 0,1 , q 1,1 , q 2,1 , ... be an execution in L C starting in q 1 = q 0,1 and assume (q 1 , q 2 ) ∈ R. We can define a corresponding execution in L A starting in q 2 = q 0,2 with the same length (in case the execution σ 1 is finite), where the transitions q i,1 -→ q i+1,1 are matched by transitions q i,2 -→ q i+1,2 such that (q i+1,1 , q i+1,2 ) ∈ R. We use the induction method on i to prove it.

• Base case: i = 0. It follows directly from (q 1 , q 2 ) ∈ R in case q 1 is a terminal state. If there is a transition q 0,1

P(Y )
--→ q 1,1 such that y 0,1 ∈ Sol(P(Y )) then there exists a finite set of transitions (q 0,2

P j -→ q j 1,2
) j∈J with Sol(P) ⊆ Sol( ∏ j∈J P j ) and (q 1,1 , q j 1,2 ) ∈ R, ∀ j ∈ J. Because Sol(P) ⊆ Sol( ∏ j∈J P j ), there exists a polynomial P j (Y ) such that y 0,1 ∈ Sol(P j ), and the transition q 0,1 y 0,1 --→ q 1,1 can be matched by the transition q 0,2

y 0,1 --→ q j 1,2
with (q 1,1 , q j 1,2 ) ∈ R. This yields the execution fragment q 0,2 , y 0,2 , q 1,2 with y 0,1 = y 0,2 in L A .

• Induction step: Assume i > 0 and that the execution q 2 , y 0,2 , q 1,2 , y 1,2 , q 2,2 , y 2,2 , ..., q i,2 is already constructed with (q k,1 , q k,2 ) ∈ R and y k,1 = y k,2 for k = 0, ..., i. If σ 1 has length i and q i,1 is a terminal state, then the execution fragment σ 2 = q 2 , y 0,2 , q 1,2 , y 1,2 , q 2,2 , y 2,2 , ..., q i,2 is an execution fragment with the same length which is state-wise related to σ 1 . Now we assume that s i,1 is not terminal. We consider the step q i,1

P(Y ) --→ q i+1,1 with y i,1 ∈ Sol(P(Y )) in σ 1 . Since (q i,1 , q i,2
) ∈ R, there exists a finite set of transitions (q i,2 P j -→ q j i+1,2 ) j∈J with Sol(P) ⊆ Sol( ∏ j∈J P j ) and (q i+1,1 , q j i+1,2 ) ∈ R, ∀ j ∈ J. Because Sol(P) ⊆ Sol( ∏ j∈J P j ), there exists a polynomial P j (Y ) such that y i,1 ∈ Sol(P j ), and the transition q i,1 y i,1 --→ q i+1,1 can be matched by the transition q i,2 y i,1 --→ q j i+1,2 with (q i+1,1 , q j i+1,2 ) ∈ R. This yields the execution fragment q 2 , y 0,2 , q 1,2 , y 1,2 , ..., q i,2 , y i,2 , q i+1,2 which is state-wise related to the execution σ 1 and y i,1 = y i,2 in L A .

Composition of compilation phases

Let Cp be an unverified compiler, the following process defines a derived compiler such that it is formally verified.

1 if ( Cp ( A ) == Error ) return Error 2 else 3 { 4 if (L IR(A) ⊑ Pds L A ) return IR(A) 5 else return Error 6 }
where Cp(A) is the compilation of A to either compiled code (written as Cp(A) = IR(A)) or compilation errors (written as Cp(A) = Error), L A and L IR(A) are the intensional labeled transition systems of A and IR(A), respectively.

Compilation is always decomposed into several phases of transformations and optimizations through intermediate representations. Thus it is better to decompose the verification process too. Fortunately, our verification process can be decomposed well thanks to the transitive property of symbolic simulation. Let L A , L I and L C be three ILTSs, if L I ≼ L A and L C ≼ L I then L C ≼ L A (the proof is trivial based on the definition of symbolic simulation).

We assume that there are two compilation phases Cp1 and Cp2 from the source program A to the compiled program I and from the compiled program I to other compiled program C, respectively. Consider the composition compilation as follows:

1 if ( Cp1 ( A ) == Error ) return Error 2 else 3 { 4 if (L I ⊑ Pds L A ) 5 { 6 if ( Cp2 ( I ) == Error ) return Error 7 else 8 { 9 if (L C ⊑ Pds L I ) return C else return Error } } else return Error }
It is obvious to see that the compilation process from A to C is formally verified.

Implementation with SIGALI

In this section, we discuss how to implement the proof method with symbolic simulation using the companion model-checker of the POLYCHRONY toolset, SIGALI.

Implementation

We design a validator that is integrated into the clock calculation and Boolean abstraction phase of the SIGNAL compiler. The validator which is depicted in Figure 4.2 works as follows. It takes the input program and its transformed counterpart to construct the corresponding PDSs. These PDSs are given as the input of the model-checker SIGALI. In the checking phase, SIGALI will answer whether there exists a symbolic simulation for two PDSs. Symbolic simulation can be implemented as an extended library of SIGALI. We represent an ILTS in the more specific form L = (X, X ′ ,Y, I , T ), where:

• X, X ′ and Y are the sets of state and event variables as in the PDS,

• I (X) = Q 0 (X) is the polynomial representing the set of initial states, Sol(I),

• T (X,Y, X ′ ) ≡ Q(X,Y )⊕(P(X,Y )-X ′ ) is the polynomial representing the set of tran- sitions.
In SIGALI, polynomials are internally represented as Ternary Decision Diagrams (TDD) [START_REF] Dutertre | Sigali: un système de calcul formel pour la vérification de programmes signal[END_REF] which are an extension of Binary Decision Diagrams (BDD) [START_REF] Bryant | Graph-based algorithms for boolean function manipulation[END_REF]. They are convenient for an efficient manipulation of the polynomial equation systems. Theorem 2 gives us an iterative algorithm to compute the greatest symbolic simulation for two intensional labeled transition systems. It can be obtained by computing the convergence of the sequence (R j ) j∈N as in Listing 4.3 which can be efficiently implemented with the fixed-point computation of the SIGALI kernel. The correctness of Listing 4.3 is proved by the following proposition.

Listing 4.3 Compute symbolic simulation

1 Input : L C = (X 1 , X ′ 1 ,Y, I 1 , T 1 ), L A = (X 2 , X ′ 2 ,Y, I 2 , T 2 ) 2 Output : R(X 1 , X 2 ) 3 R 0 (X 1 , X 2 ) ≡ 0 4 while (R j (X 1 , X 2 ) is not convergent ) do 5 { 6 R j+1 (X 1 , X 2 ) is the canonical generator of the ≡-class of : 7 R j (X 1 , X 2 )⊕ 8 ∀X ′ 1 ∀Y [(T 1 (X 1 ,Y, X ′ 1 ) ⇒ ∃X ′ 2 (T 2 (X 2 ,Y, X ′ 2 ) ⊕ R j (X ′ 1 , X ′ 2 ))] 9 } 10 if (∀X 1 [(I 1 (X 1 ) ⇒ ∃X 2 (I 2 (X 2 ) ⊕ R(X 1 , X 2 ))]) return R(X 1 , X 2 ) else return R(X 1 , X 2 ) ≡ 1 Proposition 1 For all j ∈ N,R j (x 1 , x 2 ) = 0 iff x 1 ≼ j x 2 .
Proof 4 ⇒) We use an induction proving method over j. It holds obviously with j = 0.

Assume that we have R j+1 (x 1 , x 2 ) = 0 and let x 1

P -→ x ′ 1 be a transition in L C . It is clear that P(Y ) ≡ T 1 (x 1 ,Y, x ′ 1 ). We define the polynomial Q(Y ) ≡ ∃x ′ 2 T 2 (x 2 ,Y, x ′ 2 ) ⊕ R j (x ′ 1 , x ′
2 ), R j being computed in Listing 4.3 above. This polynomial captures the set {y|∃x 2

P i -→ x i 2 , P i (y) = 0 ∧ x ′ 1 ≼ j x i 2 }
. By the definition of R j+1 , the y value is in Sol(T 1 (x 1 ,Y, x ′ 1 )). We have Sol(P(Y )) ⊆ i Sol(P i ), which means x 1 ≼ ( j+1) x 2 . ⇐) We can apply again an induction method over j similar to the proof of Theorem 2. Thus, we omit it here.

Proposition 2 Algorithm in Listing 4.3 terminates and at the end, R(x 1 , x 2 ) = 0 if and only

if x 1 ≼ x 2 .
Proof 5 Termination is guaranteed by the fact that relations R j are finite and nested. The second statement is a corollary of Proposition 1 and Theorem 2.

Experimental results

Table 4.1 shows some experimental results verifying the transformations of the SIGNAL compiler with a simulation based proof method. The experimental results deal with the complexity of the symbolic simulation computation. All the examples are available in the online examples of the POLYCHRONY toolset. In the X,Y , and "Correct" columns, we write the numbers of state variables, event variables and the correctness of the compiler transformations, respectively (hence, the transition relation T (X,Y, X ′ ) will have 2X + Y variables). We measure the complexity of the symbolic simulation by the size of fix point computation in Listing 4.3 (in terms of the number of TDD nodes that we need to represent the manipulation of polynomial equation systems). The number of TDD nodes is shown in SIGALI model checker only when it is big enough, so for the tests whose numbers of TDD nodes are not shown we write "Small" to indicate that the computation effort is light. We

denote R 1 (X 1 , X 2 ), R 2 (X 1 , X 2 ), R 3 (X 1 , X 2
) symbolic simulations for (A_TRA.z3z,A.z3z), (A_BOOL_TRA.z3z,A_TRA.z3z) and (A_SEQ_TRA.z3z, A_BOOL_TRA.z3z), respectively, for the compilation of program A.

Translation validation of clock models

We provide another approach to prove the preservation of the clock semantics for every transformation of the compiler based on the translation validation approach. We use clock model as the common semantic framework to represent the clock semantics of source program and its compiled program. A refinement relation is formally defined to expresses the preservation of clock semantics, as a relation on clock models. We write Φ(C) ⊑ clk Φ(A) to denote that Φ(C) is a refinement of Φ(A).

Clock model of SIGNAL program

In this section, we describe the clock semantics of a program in terms of a first-order logic formula. Let us consider the semantics of the sampling operator y := x when b. At any logical instant, the signal y holds the value of x if the following conditions are satisfied: x holds a value, and b is present and holds the value true; otherwise, it holds no value.

Hence, to represent the underlying control conditions, we need to represent the statuses: present with the value true, present with the value false and absent for the signal b, and the statuses: present and absent for the signal x. This section explores a method to construct the control model of a program as an abstraction of the clock semantics, called clock model, which is the computational model of our translation validation approach.

Name X Y R 1 (X 1 , X 2 ) R 2 (X 1 , X 2 ) R 3 (X 1 , X 2 )
In SIGNAL, clocks play a much more important role than in other synchronous languages, they are used to express the underlying control (i.e., the synchronization between signals) for any conditional definition. This differs from LUSTRE, where all clocks are built by sampling the fastest clock. For instance, we consider again the basic process corresponding to the primitive operator sampling, y := x when b, where x and y are numerical signals, and b is a Boolean signal. To express the control, we need to represent the status of the signals x, y and b at a given instant. In this example, we use a Boolean variable x to capture the status of x:

• ( x = true) means x is present. • ( x = false) means x is absent.
In the same way, the Boolean variable ŷ captures the status of y. With each signal x i , based on the encoding scheme proposed in [START_REF] Feautrier | Enhancing the compilation of synchronous data-flow programs with combined numerical-boolean abstraction[END_REF][START_REF] Gamatié | Static analysis of synchronous programs in signal for efficient design of multi-clocked embedded systems[END_REF][START_REF] Gamatié | Towards static analysis of signal programs using interval techniques[END_REF], we attach a Boolean variable x i to encode its clock and a variable x i of same type as x i to encode its value. If x i ∈ R then we introduce a memorization variable to store the initialized, previous and next values. Formally, the abstract values which represent the clock semantics of the program can be computed using the following functions: ˆ: X -→ B associates a signal with a Boolean value, ˜: X -→ D associates a signal with a value of same type as the signal.

The composition of SIGNAL processes corresponds to logical conjunction. Thus the clock model of P will be a conjunction Φ(P) = n i=1 φ (eq i ) whose atoms are x i , x i , where φ (eq i ) is the abstraction of statement eq i (using the SIGNAL primitive operators), and n is the number of statements in the program. In the following, we present the abstraction corresponding to each SIGNAL operator.

Stepwise functions

The functions which apply on signal values in the primitive stepwise functions are usual logic operators (not, and, or), numerical comparison functions (<, >, =, <=, >=, /=), and numerical operators (+, -, *, /). In our experience working with the SIGNAL compiler, it performs very few arithmetical optimizations and leaves most of the arithmetical expressions intact. Every variable is determinable by the inputs, memorizable values, otherwise program cannot be compiled. This suggests that most of the implications will hold independently of the features of the numerical comparison functions and numerical operators and we can replace the operations by uninterpreted functions. Following the encoding procedure of [START_REF] Ackerman | Solvable cases of the decision problem[END_REF], for every numerical comparison function and numerical operator (denoted by ) occurring in an equation, we perform the following rewriting:

• Replace each x y by a new variable v i of a type equal to that of the value returned by . Two stepwise functions x y and x ′ y ′ are replaced by the same variable v i iff x, y are identical to x ′ and y ′ , respectively.

• For every pair of newly added variables v i and v j , i ̸ = j, corresponding to the nonidentical occurrences x y and x ′ y ′ , add the implication

( x = x ′ ∧ ỹ = y ′ ) ⇒ v i = v j into the abstraction Φ(P).
The abstraction φ (y := f (x 1 , ..., x n )) of stepwise functions is defined by induction as follows:

• φ (true) = true and φ (false) = false.

• φ (y

:= x) = ( ŷ ⇔ x) ∧ ( ŷ ⇒ ( ỹ ⇔ x)) if x and y are Boolean signals. φ (y := x) = ( ŷ ⇔ x) ∧ ( ŷ ⇒ ( ỹ ⇔ x)) ∧ ( x ⇒ x) if
x is an event signal.

• φ (y := x 1 and

x 2 ) = ( ŷ ⇔ x 1 ⇔ x 2 ) ∧ ( ŷ ⇒ ( ỹ ⇔ x 1 ∧ x 2 )). • φ (y := x 1 or x 2 ) = ( ŷ ⇔ x 1 ⇔ x 2 ) ∧ ( ŷ ⇒ ( ỹ ⇔ x 1 ∨ x 2 )). • φ (y := x 1 x 2 ) = ( ŷ ⇔ v i ⇔ x 1 ⇔ x 2 ) ∧ ( ŷ ⇒ ( ỹ = v i )).

Delay

Considering the delay operator, y := x$1 init a, its encoding φ (y := x$1 init a) contributes to Φ(P) with the following conjunct:

( ŷ ⇔ x) ∧ ( ŷ ⇒ (( ỹ = m.x) ∧ (m.x ′ = x))) ∧ (m.x 0 = a)
This encoding requires that at any instant, signals x and y have the same status (present or absent). To encode the value of the output signal as well, we introduce a memorization variable m.x that stores the last value of x. The next value of m.x is m.x ′ and it is initialized to a in m.x 0 .

Merge

The encoding of the merge operator, y := x default z, contributes to Φ(P) with the following conjunct:

( ŷ ⇔ ( x ∨ ẑ)) ∧ ( ŷ ⇒ (( x ∧ ỹ = x) ∨ (¬ x ∧ ỹ = z)))

Sampling

The encoding of the sampling operator, y := x when b, contributes to Φ(P) with the following conjunct:

( ŷ ⇔ ( x ∧ b ∧ b)) ∧ ( ŷ ⇒ ( ỹ = x))

Composition

Consider the composition of two processes P 1 and P 2 . Its abstraction φ (P 1 |P 2 ) is defined as follows:

φ (P 1 ) ∧ φ (P 2 )

Restriction

Restriction process P 1 /x restricts the scope of the signal x to the process P. In our abstraction the scope of signal declarations is not considered. The abstraction is given as follows:

Φ(P 1 /x) = Φ(P 1 )

Clock relations

Given the above rules, we can obtain the following abstraction for derived operators on clocks. Here, z is a signal of type event:

• φ (z :=ˆx) = (ẑ ⇔ x) ∧ (ẑ ⇒ z) • φ (xˆ= y) = x ⇔ ŷ • φ (z := xˆ+ y) = (ẑ ⇔ ( x ∨ ŷ)) ∧ (ẑ ⇒ z) • φ (z := xˆ * y) = (ẑ ⇔ ( x ∧ ŷ)) ∧ (ẑ ⇒ z) • φ (z := xˆ-y) = (ẑ ⇔ ( x ∧ ¬ ŷ)) ∧ (ẑ ⇒ z) • φ (z := when b) = (ẑ ⇔ ( b ∧ b)) ∧ (ẑ ⇒ z) 4
( FB ⇔ ZN1 ∧ ZN1) ∧ ( ZN1 ⇔ v 1 <= ⇔ ZN) ∧ ( ZN1 ⇒ ( ZN1 = v 1 <= )) ∧ ( ZN ⇔ N) ∧ ( ZN ⇒ ( ZN = m.N ∧ m.N ′ = Ñ)) ∧ (m.N 0 = 1) ∧ ( N ⇔ FB ∨ ZN2) ∧ ( N ⇒ (( FB ∧ Ñ = FB) ∨ (¬ FB ∧ Ñ = ZN2))) ∧ ( ZN2 ⇔ v 1 -⇔ ZN) ∧ ( ZN2 ⇒ ( ZN2 = v 1 -))
In

( FB → true, N → true, ZN → true, FB → 6, Ñ → 6, ZN → 1)
is a clock configuration of Φ(DEC). But the following interpretation

( FB → true, N → true, ZN → false, FB → 6, Ñ → 6, ZN → 1)
is not a clock configuration since it is not a model of the clock model. The set of all clock configurations of Φ(P), denoted by E Φ(P) , is given as follows:

E Φ(P) = { I | I |= Φ(P)}

Soundness of clock model

We will show that the clock model is sound in terms of preservation of the clock semantics of the abstracted program. That means if the clock model satisfies a property defined over the clocks, then the abstracted SIGNAL program also satisfies this property.

Clock semantics of SIGNAL program

We rely on the basic elements of trace semantics [START_REF] Guernic | Advanced topics in data-flow computing, chapter dataflow to von neumann: the signal approach[END_REF] to define the clock semantics of a synchronous data-flow program and the soundness proof method in [START_REF] Gamatié | Static analysis of synchronous programs in signal for efficient design of multi-clocked embedded systems[END_REF]. Let X = {x 1 , x 2 , ..., x n } be a finite set of typed variables. For each x i ∈ X, we use D x i to denote its domain of values, and D ⊥ x i = D x i ∪ {⊥} to denote its domain of values with absent value, where ⊥ ̸ ∈ D x i denotes the absent value. Then, the domain of values of X with absent value is defined as follows:

D ⊥ X = n i=1 D x i ∪ {⊥}
Definition 17 (Clock events) Given a non-empty set X, the set of clock events on X, denoted by E c X , is the set of all possible interpretations I over X.

An interpretation I is an assignment of values from X to D ⊥ X . The assignment I(x) = ⊥ means x holds no value while I(x) = v means that x holds the value v, and I(X) is defined as follows:

I(X) = (I(x 1 ), I(x 2 ), ..., I(x n )), x i ∈ X

For example, consider a program whose signals are X = {x, b} where x is an integer signal and b is Boolean signal, the set of clock events is given as follows, where v is an integer value:

E c X = {(x → ⊥, b → ⊥), (x → ⊥, b → false), (x → ⊥, b → true), (x → v, b → false), (x → v, b → true), (x → v, b → ⊥)}
Then at a given instant, the signals clock information is one of these clock events. By convention, the set of clock events of the empty set is defined as the empty set E c / 0 = / 0.

Definition 18 (Clock traces) Given a non-empty set X, the set of clock traces on X, denoted by T c X , is defined by the set of functions T c defined from the set N of natural numbers to E c X , denoted by T c : N -→ E c X .

The natural numbers represent the instants, t = 0, 1, 2, ..., a trace T c is a chain of clock events. We denote the interpreted value of a variable x i at instant t by T c (t)(x i ). Considering the above example:

(0, (x → ⊥, b → ⊥)), (1, (x → 1, b → false)), ...
is one of the possible clock traces on X = {x, b}, and T c (0

)(x) = T c (0)(b) = ⊥
Definition 19 (Restriction clock trace) Given a non-empty set X, a subset X 1 ⊆ X, and a clock trace T c being defined on X, the restriction of T c onto X 1 is denoted by X

1 .T c . It is defined as X 1 .T c : N -→ E c X 1 such that ∀t ∈ N, ∀x ∈ X 1 , X 1 .T c (t)(x) = T c (t)(x).
Let X be the set of all signals in program P. We write [[P]] c to denote the clock semantics of P which is defined as the set of all possible clock traces on X. For any subset X 1 ⊆ X, the set of all restriction clock traces on X 1 defines the clock semantics of P on X 1 , denoted by ([[P]] c ) \X 1 . Table 4.2 shows the clock semantics of the SIGNAL processes corresponding to the primitive operators. In the clock semantics of the delay operator, in f is the infimum (or the greatest lower bound) of the subset of instants such that x is present, sup is the supremum

Concrete clock semantics

Let Φ(P) be the clock model of the program P. We now define the concrete clock semantics of a clock model based on the notion of clock configurations. Given a clock configuration Î, the set of clock events according to Î is the set of interpretations I such that for every signal x i , if x i holds a value then x i has the value true (meaning x i is present), and x i holds the same value as x i . Otherwise, x i has the value false (meaning x i is absent). The set of clock events according to Î and the set of all clock events of Φ(P) are computed as follows:

S E c X ( Î) = {I ∈ E c X | ∀x i ∈ X, (I(x i ) = Î( x i ) ∧ Î( x i ) = true) ∨ (I(x i ) = ⊥ ∧ Î( x i ) = false)} S E c X (Φ(P)) = Î|=Φ(P) S E c X ( Î)
With a set of clock events S E c X (Φ(P)), the concrete clock semantics of Φ(P) is defined by the following set of clock traces:

Γ(Φ(P)) = {T c ∈ T c X | ∀t, T c (t) ∈ S E c X (Φ(P))}
For any subset X 1 ⊆ X, the concrete clock semantics of Φ(P) on X 1 is defined as follows: To show the soundness of our abstraction, we consider a similar reasoning as in [START_REF] Gamatié | Static analysis of synchronous programs in signal for efficient design of multi-clocked embedded systems[END_REF]. Our abstraction above is sound in terms of preservation of the clock semantics of the abstracted program P: if the clock semantics of the abstraction satisfies a property defined over the clocks, then the abstracted program also satisfies this property as stated by the following proposition. For any property ϕ which is defined over the set X, its concretization Γ(ϕ) is given by:

Γ(Φ(P)) \X 1 = {X 1 .T c | T c ∈ T c X
S E c X (ϕ) = Î|=ϕ S E c X ( Î) Γ(ϕ) = {T c ∈ T c X | ∀t, T c (t) ∈ S E c X (ϕ)}
∈ S E c X (Φ(P)) is also in S E c X (ϕ), meaning that ∀t, T c (t) ∈ S E c X (ϕ). Therefore, we have T c ∈ Γ(ϕ).
Lemma 2 For all programs P, [[P]] c ⊆ Γ(Φ(P)).

Proof 7 We prove it by induction on the structure of program P, meaning that for every primitive operator of the language we show that its clock semantics is a subset of the corresponding concretization.

• Stepwise functions: P : y := f (x 1 , ..., x n ). First, consider y as numerical signal; following the encoding scheme, we have

Φ(P) = ( ŷ ⇔ v k f ⇔ x 1 ⇔ ... ⇔ x n ) ∧ ( ŷ ⇒ ỹ = v k f ).
For any interpretation Î such that Î |= Φ(P), we have:

either ∀i, ŷ = false, v k f = false and x i = false;

-or ŷ = true, v k f = true, ∀i. x i = true and ỹ = v k f .
Then the set of clock events according to Î is given as follows:

S E c X ( Î) = {I ∈ E c {y,x 1 ,...,x n ,v k f } | I(y) = Î( ỹ) ∧ ∀i, I(x i ) = Î( x i ) if Î( ŷ) = Î( v k f ) = Î( x i ) = true and I(y) = I(x i ) = ⊥ if Î( ŷ) = Î( v k f ) = Î( x i ) = false} Let T c ∈ [[P]
] c be a clock trace and t ∈ N be any instant, then either ∀i, T c (t

)(y) = T c (t)(x i ) = ⊥ or T c (t)(y) = f (T c (t)(x 1 ), T c (t)(x 2 ), ..., T c (t)(x n )). We have T c (t) ∈ S E c X (Φ(P))
for every instant t. Therefore, T c ∈ Γ(Φ(P)). When y is a Boolean signal, the proof is similar.

• Delay, sampling, and merging operators: we prove in the same manner.

• Composition: Consider the finite set of common signals X = X A ∩ X C and the set of common variables which are used to construct the clock models is X = X A ∩ X C , we say that A and C have the same clock semantics on X if Φ(A) and Φ(C) have the same set of concrete restriction clock traces on X:

P = P1|P2. Let T c ∈ [[P]] c be a clock trace, since X 1 .T c ∈ [[P 1 ]] c , X 2 .T c ∈ [[P 2 ]] c , [[P 1 ]] ⊆ Γ(Φ(P 1
∀X.T c .(X.T c ∈ Γ(Φ(C)) \X ⇔ X.T c ∈ Γ(Φ(A)) \X ) (4.3)
In fact, the compilation makes the transformed program more concrete. For instance, when the SIGNAL compiler performs the "endochronization" which is used to generate the sequential executable code (see Section 3.3.2), the signal with the fastest clock is always present in the generated code. Moreover, compilers perform transformations and optimizations for removing or eliminating some redundant behaviors of the source program (e.g., eliminating subexpressions, trivial clock relations). Additionally, the SIGNAL compiler strengthens the data-flow dependencies expressed in the original program to produce sequential code. Consequently, Requirement (4.3) is too strong to be practical. Hence, we have to relax the requirement as follows:

∀X.T c .(X.T c ∈ Γ(Φ(C)) \X ⇒ X.T c ∈ Γ(Φ(A)) \X ) (4.4)
Requirement (4.4) expresses that every restriction clock trace of Φ(C) is also a clock trace of

Φ(A) on X, or Γ(Φ(C)) \X ⊆ Γ(Φ(A)) \X . We say that Φ(C) is a correct clock transformation of Φ(A), or Φ(C) is a clock refinement of Φ(A) on X, denoted by Φ(C) ⊑ clk Φ(A).
Proposition 4 The clock refinement is reflexive and transitive:

• ∀Φ(P), Φ(P) ⊑ clk Φ(P) on X P .

• Assume that X ⊆ X P 1 , X ⊆ X P 2 and X ⊆ X P 3 . If Φ(P 1 ) ⊑ clk Φ(P 2 ) and Φ(P 2 ) ⊑ clk Φ(P 3 ) on X, then Φ(P 1 ) ⊑ clk Φ(P 3 ) on X.

Proof 8 Proposition 4 is proved based on the clock refinement definition.

• Reflexivity: For every restriction clock trace X.T c , we have X.T c ∈ Γ(Φ(P)) \X ⇒ X.T c ∈ Γ(Φ(P)) \X .

• Transitivity: For every clock trace X.T c ∈ Γ(Φ(P 1 )) \X , we have X.T c ∈ Γ(Φ(P 2 )) \X . Since Φ(P 2 ) ⊑ clk Φ(P 3 ) on X, we have X.T c ∈ Γ(Φ(P 3 )) \X , or Φ(P 1 ) ⊑ clk Φ(P 3 ) on X.

Adaptation to SIGNAL compiler

We will adapt the definition of the above general clock refinement to the case of the SIGNAL compiler to prove the preservation of clock semantics when the compiler transforms one SIGNAL program into the intermediate representation form written in SIGNAL as well. We need to consider the following factors.

A first consideration is that the SIGNAL programs take the inputs from their environment and the register values. Then, they calculate the outputs to react with the environment. In general, the programs can use some local variables to make the output calculations. However, from the outside, the natural observation of the programs is the snapshot of the values of the input and output signals. In our context, it is the snapshot of the presence of the input and output signals. For example, for the program DEC, the observation is the tuple of the presence of the signals (FB, N) at a considered instant.

A second consideration is that in the compilation process of the SIGNAL compiler, the local signals in the source program do not necessarily have counterparts in the transformed program. However, all input and output signals are preserved in the transformations and are represented by identical names in the transformed program. Moreover, all signals in the R set are also preserved in the transformations. Therefore, it is natural to choose the snapshot of the presence of the input and output signals to be the observation for the transformed program.

These considerations let us adapt the above definition of clock refinement as follows. Let X A and X C be the sets of all signals in the source program A and its counterpart transformed program C. We write X IO to denote the set of common input and output signals. We say that C is correct transformation of A if at any instant, the tuples of values representing the presence of the signals in X IO are the same in both programs. In other words, Φ(C) ⊑ clk Φ(A) on X IO .

Proving clock refinement by SMT

We shall propose a method to check the existence of refinement between two clock models with the use of a SMT solver. Let Φ(A) and Φ(C) be the clock models of given input and transformed programs. We denote the set of all common input and output signals between A and C by X IO . Our aim is proving that Φ(C) refines Φ(A) on X IO . Let X A , X C and X IO be the set of variables which are used to construct Φ(A), Φ(C) and the set of common variables between the two clock models.

For every variable in the clock model Φ(C) except the common variables in X IO , we added "c" as superscript to distinguish them from the variables in the clock model of the input program. The standard way of proving the existence of the clock refinement is based on the following elements:

• The identification of a variable mapping that maps the non input, output variables from the clock model Φ(A) to the non input, output variables in the clock model Φ(C). We denote the mapping by:

X A \ X IO = α( X C \ X IO )
• The premises of a rule such that if the premises hold, then the conclusion, Φ(C) refines Φ(A), is true. The premise is presented in Figure 4.3.

For a variable mapping

X A \ X IO = α( X C \ X IO ), Premise. ∀ Î over X A ∪ X C .( Î |= Φ(C) ⇒ Î |= Φ(A)) Conclusion. Φ(C) ⊑ clk Phi(A) on X IO

Fig. 4.3 Rule CLKREF

The rule CLKREF says that for any interpretation Î over X A ∪ X C such that the variable mapping is evaluated to true, Î is a clock configuration of Φ(C) then it is also a clock model of Φ(A). Then there exists a clock refinement for (Φ(C), Φ(A)). The rule CLKREF is sound based on the following theorem.

Theorem 4 For a variable mapping X

A \ X IO = α( X C \ X IO ), if the formula Φ(C) ⇒ Φ(A) is valid, then Φ(C) ⊑ clk Φ(A) on X IO .
Proof 9 To prove it, we have to show that for every interpretation Î over X = X A ∪ X C such that it is evaluated to true.

If Î |= (Φ(C) ⇒ Φ(A)), then Γ(Φ(C)) \X IO ⊆ Γ(Φ(A)) \X IO . Given X IO .T c ∈ Γ(Φ(C)) \X IO , it means that ∀t, T c (t) ∈ S E c X (Φ(C)). Since for every interpretation Î, Î |= Φ(C) implies that Î |= Φ(A)), thus S E c X (Φ(C)) ⊆ S E c X (Φ(A))
under the variable mapping. We get T c (t) ∈ S E c X (Φ(A)) for every t. Therefore, we have T c ∈ Γ(Φ(A)).

Consider a variable x ∈ X A \ X IO , the mapping α x of the variable mapping defines the value of x in the clock model Φ(A) α-related to the value represented by the clock model Φ(C).

We therefore need to describe the mappings

α x for x c ∈ X C \ X IO = M clk ∪ R clk ∪ L clk .
Recall that every state signal s, we introduce a memorization variable m.s in the clock model Φ(A), and a corresponding a memorization variable m.s c in the clock model Φ(C). For example, the state signal N in the equation ZN := N$1 init 1, makes use of the memorization variables m.N and m.N c in the clock models. Therefore, we define the following instance of the α mapping for each state signal s:

s ⇔ s c ⇒ m.s ⇔ m.s c if s is Boolean signal s = s c ⇒ m.s = m.s c if s is non-Boolean signal
For example, the mapping for the variables m.N and m.N c will be given by the formula:

Ñ = N c ⇒ m.N = m.N c
It remains to define the instance of the mapping α for variables l, l ∈ S clk ∪ L clk in the clock model Φ(A) which correspond to the local or state signal named l in the SIGNAL program. In a SIGNAL program, one signal is defined by an equation l = eq, if we follow the definitions of all output and local signals in this equation and apply successively substitutions, then we get that the equation is constructed only by the input and state signals. This property is yielded since the SIGNAL program is determinate, meaning that all definitions of signals are defined determinately by the input and state signals, and the SIGNAL compilers rejects all non-determinate program. Equivalently, in the corresponding clock model Φ(A), the output, state and local variables are determinately defined by the input I and memorization M variables. The definition is written in the clock model in the form l ⇔ f ∧ l = f , where f and f are the formulas which define the clock relations and the values of the signal l in the clock model Φ(A). Therefore, we define the following instance of the α mapping in the clock model corresponding to each state or local signal l:

l ⇔ f ∧ l ⇔ f if l is Boolean signal l ⇔ f ∧ l = f if l is non-Boolean signal
For example, the mapping for the variables ZN and ZN in the clock model Φ(DEC) corresponding to the local variable ZN in the SIGNAL program DEC will be given by the formula:

( ZN ⇔ N) ∧ ( ZN ⇒ ( ZN = m.N ∧ m.N ′ = Ñ)) ∧ (m.N 0 = 1)
Therefore, the variable mapping X A \ X IO = α( X C \ X IO ) is expressed as the following formula: (1) when the signal is of Boolean type and (2) the signal is of non-Boolean type.

m.s∈M s ⇔ s c ⇒ m.s ⇔ m.s c (1) s = s c ⇒ m.s = m.s c (2) ∧ l, l∈S∪L l ⇔ f ∧ l ⇔ f (1) l ⇔ f ∧ l = f (2)
To solve the validity of the formula (Φ(C) ⇒ Φ(A)) in Theorem 4 under the variable mapping, a SMT solver is needed since this formula involves non-Boolean variables and uninterpreted functions (using a SAT solver would not be sufficient). A SMT solver decides the satisfiability of arbitrary logic formulas of linear real and integer arithmetic, scalar types, other user-defined data structures, and uninterpreted functions. If the formula belongs to the decidable theory, the solver gives two types of answers: sat when the formula has a model (there exists an interpretation that satisfies it); or unsat, otherwise. In our case, we will ask the solver to check whether the formula

¬(Φ(C) ∧ X A \ X IO = α( X C \ X IO ) ⇒ Φ(A)) is unsatisfiable, since this formula is unsatisfiable iff |= (Φ(C) ∧ X A \ X IO = α( X C \ X IO ) ⇒ Φ(A)).
In our translation validation, the clock models which are constructed from Boolean or numerical variables and uninterpreted functions belong to a part of first-order logic which has a small model property according to [START_REF] Borger | The classical decision problem[END_REF]. The numerical variables are involved only in some implications with uninterpreted functions such as

( x = x ′ ∧ ỹ = y ′ ) ⇒ v i = v j
In addition, the formula is quantifier-free. This means that the check of satisfiability can be established by examining a certain finite cardinality of models. Therefore, the formula can be solved efficiently and significantly improves the scalability of the solver.

Implementation with SMT

We describe the main steps of our approach, and the main techniques which are used to implement them. This implementation can be integrated into the existing POLYCHRONY toolset to prove the preservation of clock semantics.

Implementation

Given a source program A, with an unverified compiler, we consider the following compilation process:

1. The compiler takes program A and transforms it.

2. If there is any error (e.g., syntax error), it outputs an Error.

Otherwise, it outputs the intermediate representation C = IR(A).

These steps can be represented in the following pseudo-code, where Cp(A) is the compilation from the source program A to either compiled program IR(A) or compilation error:

1 if ( Cp ( A ) is Error ) return Error ; 2 else return IR ( A ) ;
If we associate a verification process which checks that IR(A) refines A with respect to the clock semantics, we obtain the following derived compiler that gives a guarantee of the preservation of clock semantics during the compilation from A to IR(A). We design a validator depicted in Figure 4.4 that takes the source program A and the counterpart compiled program C to construct the corresponding clock models. Then, it establishes the first-order logic formula with the above mapping from C to A as the input of the solver. Finally, in the solving phase, it checks the validity of the formula

(Φ(C) ∧ X A \ X IO = α( X C \ X IO ) ⇒ Φ(A)).

Signal Program A Clock Model Construction

(A) Clock model construction Given the input program A and its transformed programs C, this step will construct the corresponding clock models according to the above encoding scheme. At the end of this step, the clock models of the input and transformed programs are represented as the first-order logic formulas Φ(A) and Φ(C), respectively.

Clock Model Construction

Checking formula construction Consider the clock models Φ(A) and Φ(C). This step first establishes the variable mapping, then it constructs the formula

(Φ(C) ∧ X A \ X IO = α( X C \ X IO ) ⇒ Φ(A))
which is the input of the solving phase for checking its validity.

SMT-based proof

We delegate checking the validity of the checking formula to a SMT solver. For our implementation, we consider the YICES solver [START_REF] Dutertre | Yices smt solver[END_REF], which is one of the best solvers at the SMT-COMP competition [START_REF] Stump | Smt-comp[END_REF].

Let us illustrate the above process on the program DEC in Listing 3.3, and its transformed program DEC_BASIC_TRA in Listing 4.5 at the first phase of the compilation process.

Φ(DEC) = ( FB ⇔ ZN1 ∧ ZN1) ∧ ( ZN1 ⇔ v 1 <= ⇔ ZN) ∧ ( ZN1 ⇒ ( ZN1 = v 1 <= )) ∧ ( ZN ⇔ N) ∧ ( ZN ⇒ ( ZN = m.N ∧ m.N ′ = Ñ)) ∧ (m.N 0 = 1) ∧ ( N ⇔ FB ∨ ZN2) ∧ ( N ⇒ (( FB ∧ Ñ = FB) ∨ (¬ FB ∧ Ñ = ZN2))) ∧ ( ZN2 ⇔ v 1 -⇔ ZN) ∧ ( ZN2 ⇒ ( ZN2 = v 1 -)) Φ(DEC_BASIC_TRA) = ( CLK c ⇔ CLK_N c ∧ ¬ CLK_FB c ) ∧ ( CLK c ⇒ CLK c ) ∧ ( CLK_N c ⇔ CLK_N c ∨ CLK_FB c ) ∧ ( CLK_N c ⇒ CLK_N c ) ∧ ( CLK_N c ⇔ N ⇔ ZN c ) ∧ ( N ⇔ FB ∧ CLK_FB c ∧ CLK_FB c ∨ ZN2 c ∧ CLK c ∧ CLK c ) ∧ ( N ⇒ ( FB ∧ CLK_FB c ∧ CLK_FB c ∧ Ñ = FB ∨¬( FB ∧ CLK_FB c ∧ CLK_FB c ) ∧ Ñ = ZN2 c )) ∧ ( ZN2 c ⇔ v 1c -⇔ ZN c ) ∧ ( ZN2 c ⇒ ( ZN2 c = v 1c -)) ∧ ( ZN c ⇔ N) ∧ ( ZN c ⇒ ( ZN c = m.N ∧ m.N ′ = Ñ)) ∧ (m.N 0 = 1 ∧ ( CLK_FB c ⇔ ZN1 c ∧ ZN1 c ) ∧ ( CLK_FB c ⇒ CLK_FB c ) ∧ ( ZN1 c ⇔ v 1c <= ⇔ ZN c ) ∧ ( ZN1 c ⇒ ( ZN1 c = v 1c <= )) ∧ ( CLK_FB c ⇔ FB) ∧ ( CLK_12 c ⇔ ZN1 c ∧ ¬ ZN1 c ) ∧ ( CLK_12 c ⇒ CLK_12 c )
In the second step, checking formula construction, our tool will establish the variable mapping X DEC \ X IO = α( X DEC_BASIC_TRA \ X IO ) as follows:

( ZN ⇔ N) ∧ ( ZN ⇒ ( ZN = m.N ∧ m.N ′ = Ñ)) ∧ (m.N 0 = 1) ∧ ( ZN1 ⇔ v 1 <= ⇔ ZN) ∧ ( ZN1 ⇒ ( ZN1 = v 1 <= )) ∧ ( ZN2 ⇔ v 1 -⇔ ZN) ∧ ( ZN2 ⇒ ( ZN2 = v 1 -))
In the third step, we delegate the checking validity of the formula (Φ(DEC_BASIC_TRA)∧ X DEC \ X IO = α( X DEC_BASIC_TRA \ X IO ) ⇒ Φ(DEC)), named ϕ, to the SMT solver under the logical context defined by the variable mapping and the following assertions:

( ZN = ZN c ∧ 1 = 1) ⇒ v 1 <= = v 1c <= ( ZN = ZN c ∧ 1 = 1) ⇒ v 1 -= v 1c
-With the YICES solver, we will get unsat when checking the satisfiability of ¬ϕ, which means that ϕ is valid. Thus, we can conclude that the transformation is correct.

Constant clock

We describe the additional features that have to be considered when the translation validation is applied on real SIGNAL programs. In SIGNAL, the occurrence of constants is allowed to designate a constant signal (i.e., a signal with a constant value). However, each occurrence of a constant has a particular clock since the corresponding signal is hidden, and this clock is determined by the context where the constant is used, called context clock. This makes our abstraction for SIGNAL operators above invalid in case a constant signal is used. In consequence of that, we have to provide new definitions of the abstraction when the operators use a constant signal (cst denotes a constant):

Stepwise functions

• φ (y := cst) = ŷ ⇒ ( ỹ ⇔ cst) if y is Boolean signal. • φ (y := cst) = ŷ ⇒ ( ỹ ⇔ cst) if y is non-Boolean signal,
where cst is an interpreted function.

• φ (y := x and cst) = ( ŷ ⇔ x) ∧ ( ŷ ⇒ ( ỹ ⇔ x ∧ cst)).

• φ (y

:= x or cst) = ( ŷ ⇔ x) ∧ ( ŷ ⇒ ( ỹ ⇔ x ∨ cst)). • φ (y := x cst) = ( ŷ ⇔ v i ⇔ x) ∧ ( ŷ ⇒ ( ỹ = v i )). Merge φ (y := x default cst) = ( ŷ ⇔ ( x ∨ ŷ)) ∧ ( ŷ ⇒ ( x ∧ ỹ = x ∨ ¬ x ∧ ỹ = cst)) φ (y := cst default x) = ( ŷ ⇔ ( x ∨ ŷ)) ∧ ( ŷ ⇒ ( ŷ ∧ ỹ = cst ∨ ¬ ŷ ∧ ỹ = x)) Sampling φ (y := x when true) = ( ŷ ⇔ ( x ∧ ŷ)) ∧ ( ŷ ⇒ ( ỹ = x)) φ (y := x when false) = ŷ ⇔ false φ (y := cst when b) = ( ŷ ⇔ ( b ∧ b)) ∧ ( ŷ ⇒ ( ỹ = cst))

Discussion

Beside the works which have adopted the translation validation approach in verification of a compiler as discussed in Chapter 2, the static analysis of SIGNAL programs for efficient code generation [START_REF] Gamatié | Static analysis of synchronous programs in signal for efficient design of multi-clocked embedded systems[END_REF] can be considered as our closest related work.

The common semantics framework which are used to construct the translation validation of clock models in this chapter is inspired by the interval-Boolean abstraction of [START_REF] Gamatié | Static analysis of synchronous programs in signal for efficient design of multi-clocked embedded systems[END_REF]. The objective of this paper was to propose a method to make the code generated by the Signal compiler more efficient by detecting and removing the dead-code segments (e.g., segment of code to compute a data-flow which is always absent). The technique allows to detect empty clocks, mutual exclusion of clocks, or clock inclusions, by reasoning on an interval-Boolean model using an SMT solver. The choice of SMT solvers is explained by the fact that it is more judicious than the Interval Decision Diagram (IDD) technique used in [START_REF] Gamatié | Towards static analysis of signal programs using interval techniques[END_REF]. In IDDs, intervals are defined on integers. To deal with other data types, IDDs require an encoding into integers. Using SMT solving, the story is different, since the solvers support a large range of algebras. From a practical point of view, SMT solving is also easier to integrate in the current Signal compiler. In our work, we used an interval-Boolean abstraction to represent the condition of dependencies among signals to make a more efficient deadlock detection technique.

On the other hand, Pouzet et al. [START_REF] Biernacki | Clock-directed modular code generation of synchronous data-flow languages[END_REF] introduce a generic machine-based intermediate presentation to describe the transition functions in the modular compilation of SCADE/LUS-TRE. The formalization of the intermediate presentation appears as a fundamental need in order to develop a certified compiler using a proof assistant. However, as we mentioned above, this approach yields a situation where any change of the compiler requires redoing the proof. Moreover, a realistic compiler is in general a much bigger and more difficult object to verify than a single translation function.

The present chapter provides a proof of correctness of a multi-clocked synchronous programming language compiler for clock semantics preservation and applies this approach to the synchronous data-flow language SIGNAL compiler. We have presented two approaches based on model checking and the use of SMT solving to prove the preservation of clock semantics during the compilation. The clock semantics of a given source program and its transformed program are represented as PDSs over the finite field modulo 3, Z/ 3 Z. A refinement relation between the source program and its compiled program is used to express the preservation. A proof based on the simulation technique is presented to establish the existence of the refinement relation. In the second approach based on the use of SMT solver, the clock semantics is represented as a clock model. A refinement relation between two clock models is used to express the preservation, which is checked by using a SMT solver.

A compilation phase, followed by the refinement verification process, guarantees that the clock semantics of the source program is preserved in the compiled program. We have proposed methods to implement and integrate our verification process within the POLY-CHRONY toolset by extending the functionality of the existing model checker SIGALI, and the use of SMT solver to prove the correctness of the first two phases of the SIGNAL compiler.

Thanks to this experiment, we observed that the approach based on model checking suffers from the increasing state-space when it deals with large programs (the programs contain a huge amount of variables). The number of states grows exponentially with the number of program variables. On the contrary, in the approach based on the use of SMT solver, the clock semantics is presented as a first-order logic formula over Boolean variables and uninterpreted functions. Thanks to the efficiency of the SMT implementation, this approach can deal with programs whose number of variables is very big. CHAPTER

TRANSLATION VALIDATION OF SDDG

In this chapter, we describe how the preservation of data dependencies among signals in the compilation of SIGNAL can be proved by showing that for every pair of signals x and y in the source program, if there exists a data dependency between x and y, then this dependency is also in the compiled program. The data dependencies among signals in the program are represented by a formal representation, called Synchronous Data-flow Dependency Graph (SDDG).

A SDDG is a labeled directed graph in which each node is a signal or a clock, each edge from a node to another node represents the dependency between nodes that is labeled by a condition, called clock constraint. Therefore, a dependency between two signals is conditioned: the dependency is effective whenever the condition holds. For instance, the basic process y := x when b specifies that at any instant such that x is present, b is present, and b holds the value true, y cannot be set before the evaluation of x. We can use a Boolean expression x ∧ b ∧ b to encode the fact that x is present, b is present, and b holds the value true, where x, b, b are Boolean variables. Hence, the value of y depends on the current value of x whenever the condition x ∧ b ∧ b is satisfied. Given two SDDGs of the source and compiled programs, a refinement relation between them is formally defined which expresses the semantic preservation of data dependency. We delegate checking the refinement to a SMT solver. Figure 5.1 shows our validation and its integration into the SIGNAL compilation process. If the validator points out that there does not exit a refinement then a "compiler bug" message is emitted. Otherwise, the compiler continues its work.

The remainder of this chapter is organized as follows. The definition of synchronous data-flow dependency graph and the encoding scheme from SIGNAL programs into SDDGs are studied in Section 5.2. The translation validation of SDDGs is described in Section 5.3.

Fig. 5.1 Translation validation of SDDG

We also address the mechanism of the verification process, the application of the verification process to the SIGNAL compiler, and its integration in the POLYCHRONY toolset [START_REF]Polychrony toolset[END_REF]. Section 5.4 introduces an application of SDDG to build a precise deadlock detection for SIGNAL compiler. We present some related works, conclusion and future research in Section 5.5.

The data dependency analysis in SIGNAL compiler

The second phase of the SIGNAL compiler, static scheduling, aims to make the precise determination of dependencies among signals in programs. The analysis of such dependencies provides some important functions of the compiler. The first function is to detect that the program does not contain any cyclic definition, called deadlock detection. The deadlock detection is studied in detail in Section 5.4.1. The other function is to statically calculate the scheduling for a multi-processor implementation. In order to do the above functions, the SIGNAL compiler constructs a graph which represents the data dependencies among signals, called Graph of Conditional Dependencies (GCD) as described in [START_REF] Benveniste | Hybrid dynamical systems theory and the signal language[END_REF]. For any pair of signals (x, y), it specifies under what condition the signal x depends instantly on the signal y.

To detect a cyclic definition, for a cycle in the graph, the compiler computes the conjunction of all the conditions associated with this cycle, and checks that the conjunction is identically false.

The scheduling can be statically calculated by defining subgraphs of the GCD that maybe distributed on different processors. For instance, the computation of two output signals x and y can be distributed on two different cores of a single processor or on two different processors if there is no data dependencies between them.

Dependency

Encoding in GCD

x C x C x -→ x x 2 x 2 -→ x c (Boolean signal) c [c] -→ [c], c [¬c] --→ [¬c] c -c-c 2 ----→ (-c -c 2 ) c c-c 2 ---→ (c -c 2 ) x c - → y [c] [c] -→ y (-c -c 2 ) -c-c 2 ----→ y y := f (x 1 , ..., x n ) x 1 C y -→ y ... x n C y -→ y x 1 y 2 -→ y ... x n y 2 -→ y y := x$1 init a y := x when b x C y -→ y, b C y -→ C y x y 2 -→ y, b y 2 -→ y 2 y := x default z x C x -→ y, z C z \C x ---→ y x x 2 -→ y, z z 2 (1-x 2 )
-----→ y Table 5.1 The implicit dependencies and their encoding in GCD

We first recall the analysis of implicit dependencies among signals of the primitive operators as in Section 3.3.2. We use x c -→ y to denote the fact that there is a dependency between y and x at the condition c. In particular, the following dependencies apply implicitly.

• Any signal is preceded by its clock. Then, we have the implicit dependencies among signals for the core language that are given in Table 5.1. As an example, for the basic process y := x when b, the signal y depends on the signal x whenever y is present. The clock C y depends on the Boolean signal b whenever y is present.

A GCD calculated by the SIGNAL compiler is a labeled directed graph, in which the vertices are the signals or clock variables. The edges indicate the data dependencies among signals and clock variables, and the labels are clocks which are polynomials whose coefficients range over the finite field of integers modulo 3, Z/ 3 Z. These clocks represent the conditions at which the dependencies are valid.

For example, we consider the program DEC in Section 3.3.2 which emits a sequence of values FB, FB -1, ..., 2, 1, from each value of a positive integer signal FB coming from its environment. The data dependencies among the signals FB, ZN and N can be represented by the graph in Figure 5.2, where we introduce two fresh variables ZN1 and ZN2 to replace the expressions ZN <= 1 and ZN -1, respectively. The clocks which label the edges in the graph are encoded as polynomials over Z/ 3 Z related as follows.

ZN1 2 = ZN2 2 = ZN 2 = N 2 FB 2 = -ZN1 -ZN1 2 N 2 = FB 2 + (1 -FB 2 )ZN2 2 FB 2 FB N ZN1 2 ZN ZN1 ZN2 FB 2 ZN2 2 (1 -FB 2 ) FB 2 ZN 2 ZN1 2 ZN2 2 ZN2 2 ZN1 2 FB 2 FB 2

Synchronous data-flow dependency graph

We will describe the data dependencies among signals in terms of SDDGs. In presenting the construction of a SDDG below, we first explain that a usual Data Dependency Graph (DDG) is not sufficient to represent the dependencies among signals in a polychronous program. Next, we show how clock constraints which are represented as first-order logic formulas as in Section 4.4.1 can be used to express the conditional dependencies. Let us consider again the sampling operator, y := x when b, the dependency of y on x is conditioned by the formula x ∧ b ∧ b. That means that at a given instant, y depends on x only when this formula is evaluated to be true.

Data dependency graphs

As in [START_REF] Allen | Control flow analysis[END_REF], a DDG is a directed graph which contains nodes that represent locations of definitions and uses of variables in basic blocks, and edges that represent data dependencies between nodes. Once the DDG is constructed, the dependencies among variables are fixed. They do not vary along the time, in other words, DDGs can only be used to represent the data dependencies which are static in terms of the time.

Considering the pseudo-code of the following program Sum. Figure 5.3 partially shows its DDG (the figure shows only the data dependencies that are related to variable i). Data dependency edges are depicted by dotted lines which are added to the Control Flow Graph (CFG) [START_REF] Cooper | Engineering a Compiler[END_REF][START_REF] Nielson | Principles of Program Analysis[END_REF], and labeled by the name of the variable that creates the dependency. Node numbers in the CFG correspond to statement numbers in the program (we treat each statement as a basic block). Each node that represents a transfer of control (e.g., node 5) has two edges with labels true and false, all others are unlabeled.

SIGNAL program as synchronous data-flow dependency graph

Data dependency graphs would not really represent the data dependencys of a SIGNAL program since the presence of signals may vary along time (which is defined by their clock), in consequence, the dependencies among signals in the program are not static, they also vary. To deal with that, the dependencies must be conditioned by the clocks at which the dependencies are effective.

To illustrate the definition of SDDGs, we consider a process which involves the basic process corresponding to the merge operator: The statements (2), ( 3) and ( 5) represent the expressions defining the signal x, z and y, respectively. The signal x is defined at statement 2 and is fetched at statement 5 if the signal x is present. Considering the basic process y := x default z (and the clock constraints between signals), the "valid" states are: x is present and y is present; or x is absent, z is present, and y is present; or x, y and z are absent. They can be expressed by ŷ ⇔ ( x ∨ ẑ) in our abstraction as in Section 4.4.1. According to the valid states of the signals, the different data dependencies among signals are depicted in Figure 5.4, where the labels represent the conditions at which the dependencies are effective. For instance, when x = true, y is de-

y x z x ¬ x ∧ ẑ Fig. 5.4
The SDDG of merge operator fined by x; otherwise it is defined by z when x = false and ẑ = true. The graph has the following property: an edge cannot exist if one of its extremity nodes is not present (or the corresponding signal holds no value). In our example, this property can be translated in our abstraction of clock semantics as:

x ⇒ ŷ ∧ x and ¬ x ∧ ẑ ⇒ ŷ ∧ ẑ A SDDG for a given program is a labeled directed graph in which each node is a signal or clock variable and each edge represents the dependency between nodes. Each edge is labeled by a first-order logic formula that represents the clock at which the dependency between the extremity nodes is effective. Formally, a SDDG is defined as follows:

Definition 21 (SDDG) A SDDG associated with a SIGNAL program is a labeled directed graph G = ⟨N, E, I, O,C, m N , m E ⟩, where:

• N is a finite set of nodes. Each node is a signal or a clock variable.

• E ⊆ N × N is the set of edges. They describe the data dependencies among signals and clock variables in the program. Each edge is labeled by a clock constraint that is a first-order logic formula in our abstraction.

• I ⊆ N is the set of input nodes. They are the set of input signals.

• O ⊆ N is the set of output nodes. They are the set of output signals.

• C is the set of conditions, called clock constraints. The conditions are encoded as the expressions of clocks in the abstraction in Section 4.4.1.

• m N : N -→ C is a mapping labeling each node with a clock contraint. It defines the existence condition of a node.

• m E : E -→ C is a mapping labeling each edge with a clock constraint. It defines the existence condition of an edge.

In contrast with DDG, the clock labeling in SDDG provides a dynamic dependency feature. This clock labelling imposes two properties which are implicit:

• An edge cannot exist if one of its two extremity nodes does not exist. This property can be translated in our abstraction as:

∀(x, y) ∈ E, m E (x, y) ⇐ (m N (x) ∧ m N (y)) Operators Encoding in SDDG x x x - → x, m N ( x) = x, m N (x) = x c (Boolean signal) c [c] -→ [c], m N (c) = ĉ, m N ([c]) = [c], c [¬c] --→ [¬c], m N (c) = ĉ m N ([¬c]) = [¬c] x c - → y [c] [c] -→ y, m N ([c]) = [c], m N (y) = ŷ y := f (x 1 , ..., x n ) x 1 ŷ - → y ... x n ŷ - → y, m N (x i ) = x i , m N (y) = ŷ, i = 1, ..., n y := x$1 init a m N (x) = x, m N (y) = ŷ y := x when b x ŷ - → y, m N (x) = x, m N (y) = ŷ, b ŷ - → ŷ, m N (b) = b, m N ( ŷ) = ŷ y := x default z x x - → y, m N (x) = x, m N (y) = ŷ, z ẑ∧¬ x ---→ y, m N (z) = ẑ, m N (y) = ŷ Table 5.2
The dependencies of the core language

• A cycle of dependencies does not stand for a deadlock if the conjunction of all the conditions associated with the cycle is identically false. It can be expressed as:

x 1 , ..., x n , x 1 is not a deadlock if m E (x 1 , x 2 ) ∧ m E (x 2 , x 3 ) ∧ ... ∧ m E (x n , x 1 ) is false
We denote the fact that there exists a dependency between two nodes x and y at a clock constraint m E (x, y) = ĉ by x ĉ -→ y. Then, a dependency path from x to y is any set of nodes s = ⟨x 0 , x 1 , ..., x k ⟩ such that x i+1 depends on x i for all i from 0 to k -1. The clock constraint at which the dependency path is effective is c = k-1 i=0 c i , where c i = m E (x i , x i+1 ). When the number of nodes is two, the path is an edge. We also write

x = x 0 c 0 -→ x 1 c 1 -→ ... c k-1 --→ x k = y
to denote a path from x to y.

In Table 5.2, we construct the dependencies among signals for the core language, where the sub clocks [c] and [¬c] are encoded as ĉ ∧ c and ĉ ∧ ¬ c, respectively, in our abstraction. The edges are labeled by clocks which are represented by a first-order formula. For instance, the basic process of the primitive operator sampling satisfies that ŷ ⇒ x ∧ ŷ and ŷ ⇒ b ∧ ŷ.

We assume that all considered SIGNAL programs are written with the primitive operators, meaning that derived operators are replaced by their definition with primitive ones, and there are no nested operators (these nested operators can be broken by using fresh signals). Following the above construction rules, we can obtain the SDDG in Figure 5.5 for the program DEC in Section 3.3.2, where we introduce two fresh variables ZN1 and ZN2 to replace the expressions ZN <= 1 and ZN -1, respectively. Note that we omit some parts of the graph such as the signal N depends on its clock N. The clocks which label the edges in the graph are encoded as the first-order formulas given as follows.

ZN1 = ZN2 = ZN = N FB = ZN1 ∧ ZN1 N = FB ∨ ZN2

Translation validation of SDDG

In this section, we adopt the translation validation approach to prove the correctness of the compiler in the static scheduling phase of the compilation process. Given two SDDGs, we first formalize the notion of "correct implementation" as a dependency refinement relation. This refinement expresses the semantic preservation of data dependencies. Then, we propose a method to implement our verification framework by the use of a SMT solver for checking the existence of the above refinement relation.

Definition of correct implementation: Dependency refinement

Let SDDG(A) = ⟨N A , E A , I A , O A ,C A , m N A , m E A ⟩ and SDDG(C) = ⟨N C , E C , I C ,O C ,C C , m N C , m E C ⟩,
to which we refer respectively as the data dependency representations of the source program and its transformed counterpart produced by the SIGNAL compiler. Let x and y be two signals in both programs A and C. A dependency path from the signal x to the signal y in SDDG(C) is a reinforcement of the dependency path from x to y in SDDG(A) if at any instant t, the dependency path in SDDG(A) is effective (meaning that the conjunction of all the conditions associated with the path is evaluated to be true at t), then the corresponding dependency path in SDDG(C) is also effective. The formal definition of reinforcement is given as follows.

Definition 22 (Reinforcement) Let d p 1 = ⟨x 0 , x 1 , ..., x n ⟩ and d p 2 = ⟨x ′ 0 , x ′ 1 , ..., x ′ m ⟩ be two dependency paths in SDDG(A) and SDDG(C), respectively, where x =

x 0 = x ′ 0 , y = x n = x ′ m and c i , c ′ j denote the clock constraints m E A (x i , x i+1 ) and m E C (x ′ j , x ′ j+1 ). It is said that d p 2 is a reinforcement of d p 1 iff the following formula is valid. |= n-1 i=0 c i ⇒ m-1 j=0 c ′ j We write d p 2 ≼ dep d p 1 to denote the fact that d p 2 is a reinforcement of d p 1 . The assertion |= n-1 i=0 c i ⇒ m-1 j=0 c ′ j indicates that if the dependency path d p 1 in SDDG(A
) is effective at any instant, then the dependency path d p 2 in SDDG(C) is also effective. In the special case

when m = n = 1, x c ′ 0 -→ y is a reinforcement of x c 0 -→ y iff |= c 0 ⇒ c ′ 0 .
Consider a dependency path from x to y in a SDDG graph. Assume that there exists a path from y to x, that makes a dependency cycle between x and y. We say that such cycle is a deadlock iff the dependencies of x to y and vice-versa are effective at the same time. The formal definition of deadlock is given as follows.

Definition 23 (Deadlock) Let d p = ⟨x 0 , x 1 , ..., x n , x 0 ⟩ be a cycle in a SDDG graph. The dependency cycle d p stands for a deadlock if the conjunction of all the clock constraints associated with the cycle is satisfiable, meaning that there exists some interpretation that makes the conjunction formula m

E (x 0 , x 1 ) ∧ m E (x 1 , x 2 ) ∧ ... ∧ m E (x n , x 0 ) true.
Obviously, a dependency cycle does not stand for a deadlock if the conjunction of all the clock constraints associated with the cycle, in which the dependencies are effective, is identically false. That means the dependencies of the cycle cannot be present at the same time. It can be expressed as:

M ̸ |= n i=0 c i
, where c i is the clock constraint associated with the cycle.

It indicates that there is no interpretation that makes the conjunction of all the clock constraints associated with the cycle true. Based on the above definition of deadlock, a SDDG is deadlock-free if every dependency cycle in the graph does not stand for a deadlock.

Definition 24 (Deadlock-consistent) Let d p 1 and d p 2 be two dependency paths from the signal x to the signal y in SDDG(A) and SDDG(C), respectively. The dependency path d p 2 is deadlock-consistent with d p 1 if the following condition is satisfied: if every dependency cycle between x and y in SDDG(A) is not a deadlock then all dependency cycles between x and y in SDDG(C) are not deadlocks.

Let d p 1 = ⟨x 0 , x 1 , ..., x n ⟩ and d p 2 = ⟨x ′ 0 , x ′ 1 , ...,
x ′ m ⟩ be two dependency paths in SDDG(A) and SDDG(C), respectively, where x = x 0 = x ′ 0 , y = x n = x ′ m and c i , c ′ j denote the clock constraints m E (x i , x i+1 ) and m E (x ′ j , x ′ j+1 ). The Definition 24 can be expressed as follows. For any dependency path d p inv 1 = ⟨x inv 0 , x inv 1 , ..., x inv p ⟩, where x inv 0 = y, x inv p = x, that forms a cycle between x and y in SDDG(A), then for every dependency path d p inv 2 = ⟨x inv ′ 0 , x inv ′ 1 , ..., x inv ′ q ⟩, where x inv ′ 0 = y, x inv ′ q = x, that forms a cycle between x and y in SDDG(C), it satisfies:

|= ( n-1 i=0 c i ∧ p-1 j=0 c inv j ) ⇔ false ⇒ ( m-1 k=0 c ′ k ∧ q-1 l=0 c inv ′ l ) ⇔ false
We write d p 2 ≍ dep d p 1 to denote the fact that d p 2 is deadlock-consistent with d p 1 . Deadlock consistency expresses the fact that if there is a cycle between two signals x and y in the graph of the source program such that it does not stand for a deadlock, then in the graph of the compiled program, every cycle between x and y must not stand for a deadlock. In the special case where m = n = p = q = 1,

x c ′ 0 -→ y is deadlock-consistent with x c 0 -→ y if |= (c 0 ∧ c inv 0 ⇔ false) ⇒ (c ′ 0 ∧ c inv ′ 0 ⇔ false).
Recall that SDDG(A) and SDDG(C) are two synchronous data-flow dependency graphs, to which we refer respectively as the data dependency representations of the source program and its transformed counterpart produced by the SIGNAL compiler. We assume that they have the same set of nodes, N A = N C . Let x and y be two signals, we say that C preserves the data dependencies among signals in A if the following conditions are satisfied.

• For every dependency path from the signal x to the signal y in A, there exists a dependency path from x to y in C.

• If there is no deadlock in A, then C introduces no deadlock. In other words, if A is deadlock-free, then it is required that C is deadlock-free.

These conditions can be expressed in terms of the synchronous data-flow dependency graphs as follows.

• For every dependency path from the signal x to the signal y in SDDG(A) at a clock constraint c 1 , then there exists a dependency path from x to y at a clock constraint c 2 in SDDG(C) such that the dependency path in SDDG(C) is effective whenever the dependency path in SDDG(A) is effective.

• If SDDG(A) is deadlock-free, then SDDG(C) is also deadlock-free.

If two SDDGs satisfy the above conditions, we say that SDDG(C) is a dependency refinement of SDDG(A) on N A and C is a correct implementation of A. We write SDDG(C) ⊑ dep SDDG(A) to denote the fact that there exists a dependency refinement relation between SDDG(C) and SDDG(A). We formalize the definition of dependency refinement as follows.

Definition 25 (Dependency refinement) Let SDDG(A) and SDDG(C) be two synchronous data-flow dependency graphs, SDDG(C) is a dependency refinement of SDDG(A) if:

1. for every dependency path d p 1 = ⟨x 0 , x 1 , ..., x n ⟩ in SDDG(A), there exists a dependency path d p 2 = ⟨x ′ 0 , x 1 , .

(|= n-1 i=0 c i ⇒ m-1 j=0 c ′ j ) and (|= m-1 j=0 c ′ j ⇒ p-1 k=0 c ′′ k ). Thus, (|= n-1 i=0 c i ⇒ p-1 k=0 c ′′ k ),
( n-1 i=0 c i ∧ p-1 j=0 l j ) ⇔ false ⇒ ( m-1 u=0 c ′ u ∧ q-1 v=0 l ′ u ) ⇔ false and |= ( m-1 u=0 c ′ u ∧ q-1 v=0 l ′ u ) ⇔ false) ⇒ ( r-1 t=0 c ′′ t ∧ s-1 z=0 l ′′ z ) ⇔ false. Therefore, |= ( n-1 i=0 c i ∧ p-1 j=0 l j ) ⇔ false ⇒ ( r-1 t=0 c ′′ t ∧ s-1 z=0 l ′′ z ) ⇔ false, or d p 1 ≍ dep d p 3 .

Dependency refinement

Adaptation to the SIGNAL compiler

We shall adapt the above definition of dependency refinement to the case of the SIGNAL compiler to prove the preservation of data dependencies among signals when the compiler transforms one SIGNAL program into the intermediate representation form also written in SIGNAL language. We need to consider the following factors as described previously in Section 4.4.3.

A first consideration is that the SIGNAL programs take the inputs from their environment and the register values. Then, they calculate the outputs to react with the environment. In general, the programs can use some local variables to make the output calculations. However, from the outside, the natural observation of the programs is the snapshot of the values of the input and output signals. In our context, it is the snapshot of the dependencies among the input and output signals. For example, for the program DEC, the observation is the dependencies between the signals (FB, N) at a considered instant.

A second consideration is that in the compilation process of the SIGNAL compiler, the local signals in the source program do not necessarily have counterparts in the compiled program. However, all input and output signals are preserved in the transformations and are represented by identical names in the transformed program. Therefore, it is natural to choose also the observation for the transformed program as the snapshot of the dependencies among the input and output signals.

Proving dependency refinement by SMT

We now discuss a method to check the existence of a refinement between two SDDGs in Definition 25 with the use of a SMT solver. Let SDDG(A) and SDDG(C) be the synchronous data-flow dependency graphs of given input and compiled programs. The set of all common input and output signals between A and C is represented by the common set of input and output nodes in the graphs, I A ∪ O A . For all signals or clock variables in SDDG(C) except the common input and output signals, we added "c" as superscript to distinguish them from the signals in SDDG(A). The variable mapping that maps the non input, output signals from SDDG(A) to the non input, output signals in SDDG(C) is constructed as described in Section 4.4.4. Our aim is proving that SDDG(C) refines SDDG(A) on

I A ∪ O A .
To check the existence of the dependency refinement, we traverse the entire graphs SDDG(A) and SDDG(C) to verify the following.

• For every path d p 1 from x to y such that x, y ∈ I A ∪ O A in SDDG(A), there exists a reinforcement path d p 2 from x to y in SDDG(C).

• And for every path d p 1 from x to y such that x, y ∈ I A ∪ O A in SDDG(A), any path d p 2 from x to y in SDDG(C) is deadlock-consistent with the path d p 1 .

Consider two dependency paths d p 1 = ⟨x 0 , x 1 , ..., x n ⟩ and d p 2 = ⟨x ′ 0 , x 1 , ..., x ′ m ⟩ in SDDG(A) and SDDG(C), respectively, where c i and c ′ j denote the clock constraints m E (x i , x i+1 ) and m E (x ′ j , x ′ j+1 ). As in Definition 22, d p 2 is a reinforcement of d p 1 iff the following formula is valid.

n-1 i=0 c i ⇒ m-1 j=0 c ′ j (5.1)
In the same way, to check the deadlock consistency between d p 1 and d p 2 , we have to check the validity of the following formula.

( n-1 i=0 c i ∧ p-1 j=0 c inv j ) ⇔ false ⇒ ( m-1 k=0 c ′ k ∧ q-1 l=0 c inv ′ l ) ⇔ false (5.2)
To solve the validity of the formula above under the variable mapping, a SMT solver is needed since this formula involves non-Boolean variables and uninterpreted functions as in our abstraction of clock semantics. In our case, we shall ask the solver to check whether the formula ¬(5.1) is unsatisfiable, since this formula is unsatisfiable iff |= (5.1). We do the same for the formula (5.2) meaning that we ask the solver to check whether the formula ¬(5.2) is unsatisfiable.

The clock constraints which are constructed from Boolean or numerical variables and uninterpreted functions belong to a part of first-order logic which has a small model property according to [START_REF] Borger | The classical decision problem[END_REF]. This means that satisfiability can be established by examining a certain finite cardinality of models, and it can be solved efficiently.

Implementation

Let A and C be the source and compiled programs. Cp denotes an unverified compiler which compiles the source program A into the compiled program C = IR(A) or a compilation error. We now associate Cp with a validator that checks that the compiled program preserves the data dependencies among signals in A. Accordingly, we get the following derived compiler: Checking formula construction Consider the graphs SDDG(A) and SDDG(C). This step first establishes the variable mapping. Then, it traverses the graphs to construct the formulas as the formula 5.1 for every pair of paths from x to y in the graphs, and the formula 5.2 for every cycle in the graph SDDG(A). The formulas are the input of the solving phase for checking their validity. In the first step, we shall construct the synchronous data-flow dependency graphs which are depicted in Figure 5.5 and Figure 5.7. Two fresh variables FB1 and ZN3 are used to replace the expressions FB when C_FB and ZN2 when C_CLK_12. We omit the dependencies among the signals FB, FB,C_FB c and C_FB c in the graph of the program

SMT-based proof

DEC_SEQ_TRA. FB FB1 c N FB1 c ZN3 c C_FB c ZN1 c ZN3 c ZN2 c ZN c C_CLK_12 c FB1 c ¬ FB1 c ∧ ZN3 c FB1 c FB1 c FB1 c C_FB c ZN1 c ZN3 c ZN2 c ZN3 c ZN3 c C_CLK_12 c
Fig. 5.7 The SDDG of DEC_SEQ_TRA In the second step, checking formula construction, our tool will establish the variable mapping X DEC \ X IO = α( X DEC_BASIC_TRA \ X IO ) as in Section 4.4.5.1. Next, it finds all dependency paths from the signal FB to the signal N, and the cycles in the graphs SDDG(DEC) and SDDG(DEC_SEQ_TRA) to generate the formulas for checking the dependency refinement. In this example, we get the following formula:

FB ⇒ ( FB1 c ∧ FB1 c )
In the third step, we delegate the checking validity of the formula to YICES solver. We get unsat when checking the satisfiability of ¬( FB ⇒ ( FB1 c ∧ FB1 c )), which means the formula is valid. Therefore, we can conclude that SDDG(DEC_SEQ_TRA) ⊑ dep SDDG(DEC) on the signals FB and N.

Precise deadlock detection for SIGNAL compiler

The SIGNAL compiler constructs the data dependencies among signals in a program, represented as a labeled directed graph, in which the labels are polynomials in Z/ 3 Z. For each dependency cycle in the graph, it checks the product of the cycle labels. If this product, which is represented as a polynomial, is equal to the null clock, then it does not stand for a deadlock. However, consider the sampling operator y := x when b, in which the clock of the signal y is defined by the condition clock [b], which defines the instants where b is present and has value true. If the Boolean expression b is a non Boolean relation (e.g., a comparison between numerical expressions), then the Z/ 3 Z abstraction considers the expression's clock instead. This yields an approximation of the actual dependency which may cause the compiler to approximate dependencies, like in the example above.

In this section, we propose a more precise deadlock detection approach. Our approach permits the compiler to detect deadlocks with numerical expressions. The data dependencies among signals are represented by a synchronous data-flow dependency graph-like, called SDDG + . A SDDG + is a labeled directed graph in which each node is a signal or clock variable and each edge represents a dependency between two nodes. Each edge is labeled by a condition at which the dependency is effective. We use the Boolean-interval abstraction that was originally proposed by Gamatié et al. [START_REF] Feautrier | Enhancing the compilation of synchronous data-flow programs with combined numerical-boolean abstraction[END_REF] to encode the clock labels. That means every signal is associated with a pair of the form (clock, value), where clock is a Boolean function and value is a Boolean or numerical function, abstracted as an interval. We use a SMT solver to reason on the labels when deciding a dependency cycle in a SDDG + to stand for a deadlock. We show how our approach addresses the limitation of the current deadlock detection used in the SIGNAL compiler through a concrete example.

Deadlock detection in the SIGNAL compiler

Before generating the executable code on a given architecture, the compilation performed by the SIGNAL compiler aims at proving the reactivity and the determinism of programs by modeling the synchronization relations and checking the absence of cyclic data dependencies in program specifications. In our consideration, the compiler needs to answer the following question: "Is the program deadlock-free?". To answer this question, the Signal compiler uses the Graph of Conditional Dependencies (GCD) in which a dependency be- This naturally yields over-approximated detection when dealing with non Booleans values.

u v v 1 y u 2 (-c 2 -c 2 2 ) v 2 (-c 1 -c 2 1 ) v 2 1 u 2
The CycleDependency program and its dependencies among the signals y, u and v in Figure 5.8 exemplify the over-approximated detection (we omit the dependencies among v, v 1 , y and u). These dependencies introduce a cycle in the graph. To verify that this cycle is not a deadlock, the SIGNAL compiler calculates the following product of the labels is null clock:

v 2 (-c 1 -c 2 1 ) * v 2 1 * u 2 * u 2 (-c 2 -c 2 2 )
Replacing the definitions of v 2 , v 2 1 and u 2 , we have:

x 2 (-c 2 -c 2 2 )(-c 1 -c 2 1 ) * x 2 (-c 2 -c 2 2 )(-c 1 -c 2 1 ) * x 2 * x 2 (-c 2 -c 2 2 )
With the current clock calculus, the compiler concludes that this cycle may cause a deadlock since at some instants the above product is different from 0 (e.g. when the signals x, c 1 , c 2 are present and both c 1 and c 2 hold the value true, or x 2 = 1, c 1 = 1, and c 2 = 1). But in fact, c 1 and c 2 cannot hold the value true at the same time.

The above limitation makes the SIGNAL compiler reject some possibly valid programs. To address this issue, we propose a new deadlock detection to better handle numerical operators.

A more precise deadlock detection

In this section, we will present a more precise deadlock detection technique compared to the technique currently used by the SIGNAL compiler. This technique uses the concept of SDDG + to express the data dependencies among the signals in a program.

In presenting our deadlock detection below, we first describe the abstraction which is used to encode the clock relations of a SIGNAL program and the construction of a SDDG + .

A Boolean-interval abstraction for clock semantics

Let X = {x 1 , ..., x n } be the set of all signals in program P. With each signal x i , we attach a Boolean variable x i to encode its clock and a variable x i of same type as x i to encode its value. Formally, the abstract values which represent the semantics of the program can be computed using the following functions: ˆ: X -→ B associates a signal with a Boolean value ˜: X -→ D associates a signal with a value of the same type The composition of SIGNAL processes corresponds to logical conjunctions. Thus the abstract model of P will be a conjunction Φ(P) = n i=1 φ (eq i ) whose atoms are x i , x i , where φ (eq i ) is the abstraction of statement eq i (statement using the Signal primitive operators), and n is the number of statements in the program. In the following, we present the abstraction corresponding to each SIGNAL operator. There are two definitions of Φ according to the type of the signal on the left hand side in each equation: (1) stands for numerical type and ( 2) is for logical type. The Boolean-interval abstraction preserves the behaviors of the program being abstracted, in other word, it is sound. The details of the abstraction and the soundness proof are presented in [START_REF] Feautrier | Enhancing the compilation of synchronous data-flow programs with combined numerical-boolean abstraction[END_REF].

Stepwise functions The functions which apply on signal values in the primitive stepwise functions are usual logic operators (not, and, or), numerical comparison functions (<, >, =, <=, >=, /=), and numerical operators (+, -, *, /) (denoted by ). In our implementation, we replace the operation results by intervals and their representation in logic context by uninterpreted functions.

The abstraction φ (y := f (x 1 , ..., x n )) of stepwise functions is defined as follows:

n i=1 ( ŷ ⇔ xi ) ∧ ( ŷ ⇒ ỹ ∈ φ ( f (x 1 , ..., x n ))) (1) n i=1 ( ŷ ⇔ xi ) ∧ ( ŷ ⇒ ỹ ⇔ φ ( f (x 1 , ..., x n ))) (2)
where the abstraction φ ( f (x 1 , ..., x n ) is defined by induction as follows:

• φ (true) = true and φ (false) = false.

Clock relations Given the above rules, we can obtain the following abstraction for derived operators on clocks. Here, z is a signal of type event:

• φ (z :=ˆx) = (ẑ ⇔ x) ∧ (ẑ ⇒ z) • φ (xˆ= y) = x ⇔ ŷ • φ (z := xˆ+ y) = (ẑ ⇔ ( x ∨ ŷ)) ∧ (ẑ ⇒ z) • φ (z := xˆ * y) = (ẑ ⇔ ( x ∧ ŷ)) ∧ (ẑ ⇒ z) • φ (z := xˆ-y) = (ẑ ⇔ ( x ∧ ¬ ŷ)) ∧ (ẑ ⇒ z) • φ (z := when b) = (ẑ ⇔ ( b ∧ b)) ∧ (ẑ ⇒ z)
Example Assume that the intervals for the signals are given as

x ∈ (-∞, +∞), c ∈ (-∞, +∞), y ∈ (-∞, +∞), u ∈ (-∞, +∞), v ∈ (-∞, +∞).
Applying the abstraction rules above, the abstraction of the program CycleDependency is represented by the following first-order logic formula, where we introduce three fresh variables c 1 , c 2 and v 1 to replace the expressions (c <= 0), (c >= 1) and (v when c 1 ), respectively:

( ŷ ⇔ v 1 ∨ x) ∧ ( ỹ ∈ (-∞, +∞)) ∧ ( v 1 ⇔ v ∧ c 1 ∧ c 1 ) ∧ ( v 1 ∈ (-∞, +∞)) ∧( c 1 ⇔ ĉ) ∧ ( c 1 ⇔ ( c ∈ (-∞, 0])) ∧ ( û ⇔ ŷ ⇔ x) ∧ ( ũ ∈ (-∞, +∞)) ∧( v ⇔ û ∧ c 2 ∧ c 2 ) ∧ ( ṽ ∈ (-∞, +∞)) ∧ ( c 2 ⇔ ĉ) ∧ ( c 2 ⇔ ( c ∈ [1, +∞)))
A SDDG + for a given program is a labeled directed graph in which each node is a signal or clock variable and each edge represents the dependency between nodes. Each edge is labeled by a first-order logic formula which represents the clock at which the dependency between the extremity nodes is effective. Formally, a SDDG + is defined as follows:

Definition 26 (SDDG + ) A SDDG + associated with a process P is a tuple G = ⟨N, E, I, O,C, m N , m E ⟩
where:

• N is a finite set of nodes, each of which represents the equation defining a signal or a clock.

• E ⊆ N × N is the set of dependencies between nodes.

• I ⊆ N is the set of input nodes.

• O ⊆ N is the set of output nodes.

• C is the set of first-order logic formulas over a set of clocks in the Boolean-interval abstraction.

• m N : N -→ C is a mapping labeling each node with a clock; it defines the existence condition of a node.

• m E : E -→ C is a mapping labeling each edge with a clock constraint; it defines the existence condition of an edge.

The clock labeling in SDDG + provides a dynamic dependency feature. This clock imposes the following property: An edge cannot exist if one of its two extremity nodes does not exist. This property can be translated in our Boolean-interval abstraction as:

∀(x, y) ∈ E, m E (x, y) ⇐ (m N (x) ∧ m N (y))
We denote the fact that there exists a dependency between two nodes x and y at a clock condition m E (x, y) = ĉ by x ĉ -→ y. A dependency path from x to y is any set of nodes s = {x 0 , x 1 , ..., x k } such that (an edge is a special case when k = 1):

x = x 0 c 0 -→ x 1 c 1 -→ ... c k-1 --→ x k = y
The dependencies among signals for the primitive operators of the SIGNAL language are the same as the encoding in Table 5.2 except that the clock constraints which label the edges in the graph are represented in the Boolean-interval abstraction.

Following the above construction rules, we can obtain the SDDG + in Figure 5.9, for the simple program CycleDependency (we omit the parts of the graph that represent the dependencies of c 1 and c 2 on c). In this graph, the clock labels are defined in the above Boolean-interval abstraction.

v u v 1 y c 2 c 1 x v 1 v 1 v û ¬ v 1 ∧ x û v v 1
Fig. 5.9 The SDDG + of CycleDependency

Precise deadlock detection

In this section, we shall present a more precise deadlock detection technique which is based on the concept of SDDG + along with the Boolean-interval abstraction. We shall show the performance comparison of our technique with the current technique of the SIGNAL compiler using a concrete example.

Deadlock definition

Let G be a SDDG + , and x ĉ -→ y be an edge in G. Assume that there exists a path from y to

x, that makes a dependency cycle between x and y. A cycle of dependencies, standing for a deadlock, is defined with a similar meaning to the one in GCD. We say that such cycle is a deadlock in G iff the dependencies of x to y and vice-versa are effective at the same time.

Transposing the notion of deadlock to SDDG + graphs, we have the following definition:

Definition 27 (Deadlock) Let G = ⟨N, E, I, O,C, m N
, m E ⟩ be a SDDG + , and p c = x 1 , ..., x n , x 1 be a cycle in G. p c is said a deadlock in G if there exists some interpretations that make the first-order logic formula m

E (x 1 , x 2 ) ∧ m E (x 2 , x 3 ) ∧ ... ∧ m E (x n , x 1 ) true.
Based on the definition of deadlock in SDDG + graphs, we can have the definition of deadlockfree of a SDDG + as follows:

Definition 28 (Deadlock-free) Let G = ⟨N, E, I, O,C, m N , m E ⟩ be a SDDG + . G is deadlockfree iff for every cycle (x 1 , ..., x n , x 1 ) in G, the conjunction of all the conditions associated with the cycle m

E (x 1 , x 2 ) ∧ m E (x 2 , x 3 ) ∧ ... ∧ m E (x n , x 1 ) ⇔ false is identically false.
Obviously, the fact that the conjunction of first-order logic formulas associated with the cycle, in which the dependencies are effective, is false indicates that a deadlock does not exist if all the dependencies of the cycle in the SDDG + graph cannot be present at the same time.

Proving deadlock free by SMT

Given the SDDG + of a program, we introduce an approach to check that the graph is deadlock-free. It is implemented with a SMT solver [START_REF] Dutertre | Yices smt solver[END_REF][START_REF] Stump | Smt-comp[END_REF]. A SMT solver decides the satisfiability of arbitrary logic formulas of linear real and integer arithmetic, scalar types, other user-defined data structures, and uninterpreted functions. If the formula belongs to the decidable theory, the solver gives two types of answers: sat when the formula has a model (there exists an interpretation that satisfies it); or unsat otherwise. In our case, the formulas which label the edges of the graph are over Boolean variables and uninterpreted functions, thus the solving is decidable and very efficient [START_REF] Ackerman | Solvable cases of the decision problem[END_REF][START_REF] Biere | Handbook of Satisfiability[END_REF].

Following Definition 28, we shall traverse the entire graph to find all cycles such as (x 1 , ..., x n , x 1 ) and for each of them, we verify the following property. Notice that here, we do not provide any specific algorithm to find the cycles in a directed graph, interested readers can be refer to any research on this problem (e.g. the work of Johnson [START_REF] Johnson | Finding all the elementary circuits of a directed graph[END_REF]).

m E (x 1 , x 2 ) ∧ m E (x 2 , x 3 ) ∧ ... ∧ m E (x n , x 1 ) ⇔ false
It means that the basic element we have to prove is that given a dependency cycle and the conjunction of its labels, this conjunction formula is always evaluated to the value false.

Consider a dependency cycle x

1 c 1 -→ x 2 c 2 -→ ... c n-1 --→ x n c n -→ x 1 .
This cycle does not stand for a deadlock iff the formula ( n i=0 c i ⇔ f alse) is valid within the logical context defined by the abstraction of P. The checking of this condition can be implemented by asking a SMT solver to check |= ( n i=0 c i ⇔ false). In the equal way, we can ask the SMT solver to check the formula ¬( n i=0 c i ⇔ false) is unsatisfiable, or M ̸ |= ¬( n i=0 c i ⇔ false).

Implementation and illustrative example

We describe the main steps of our approach, and the techniques we use to implement them. This implementation can be integrated in the existing Polychrony toolset [START_REF]Polychrony toolset[END_REF] to check that a SDDG + graph is deadlock-free.

At a high level, our tool, which is depicted in Figure 5.10, works as follows. First, it takes the input program P, and constructs the corresponding SDDG + graph. It finds all cycles in the graph. Finally, in the solving phase, it checks the validity of the formula ( n i=0 c i ⇔ false) for each cycle (x 1 , ..., x n , x 1 ).

Signal Program Interval Analyzer

Boolean-intervval Abstraction SDDG+ Construction and Proven Formulas SMT Solver 1 2 3 4 Fig. 5.10 An overview of our approach exists a dependency cycle (v, v 1 , y, u, v) in the graph, the tool then generates the formula, referred to as ϕ, to delegate to the SMT solver as follows:

( v 1 ∧ v 1 ∧ û ∧ v) ⇔ false
In the logical context defined by Φ, replacing the definitions of c 1 , c 2 , û, v and v 1 in the program abstraction model, we get:

( x ∧ ĉ ∧ ( c ∈ [1, +∞)) ∧ ĉ ∧ ( c ∈ (-∞, 0]) ∧ x ∧ ĉ ∧ ( c ∈ [1, +∞)) ∧ ĉ ∧ ( c ∈ (-∞, 0]) ∧ x ∧ x ∧ ĉ ∧ ( c ∈ [1, +∞))) ⇔ false
With the Yices solver, we will get unsat when checking the satisfiability of ¬ϕ, which means that ϕ is valid. Thus, the graph is deadlock-free.

Our deadlock detection technique is more precise than the current technique used by the SIGNAL compiler when dealing with numerical expressions. It admits less erroneous (or "spurious") decision on deadlock detection than the current technique. That means that when our approach is applied on the SIGNAL compiler, it will make the compiler avoid rejecting valid programs. The reason why our technique is more expressive than the current one is that it uses a more suitable and precise abstraction for numerical expressions. For instance, here, our tool can detect that the two signals v and v 1 cannot be present at the same time.

Discussion

Much work has been performed before in the area of dependency-based program representations. Dennis opened up the area of data flow computation in [START_REF] Dennis | First version of a data flow procedure language[END_REF]. The data flow graph [START_REF] Ottenstein | An intermediate program form based on a cyclic data-dependence graph[END_REF][START_REF] Ottenstein | The program dependence graph in a software development environment[END_REF] represents global data dependency at the operator level, called the atomic level in [START_REF] Kuck | Dependence graphs and compiler optimizations[END_REF]. Transformations that involve both control and data dependency cannot be specified in a consistent manner with this form since control is represented by a conventional control flow graph. The data dependencies among variables are presented statically in the graph.

The GCD [START_REF] Benveniste | Hybrid dynamical systems theory and the signal language[END_REF][START_REF] Maffeïs | Distributed implementation of signal: Scheduling and graph clustering[END_REF] is used to check deadlocks in a SIGNAL program and schedule instructions. The edges of a GCD indicate the data dependencies among signals and clock variables, they are labeled by clocks. These clocks are polynomials whose coefficients range over the finite field Z/ 3 Z. These clocks represent the conditions at which the dependencies are valid, meaning that the dependencies can be represented dynamically. Based on the concept of GCD, we have defined synchronous data-flow dependency graph in which the dependencies among signals can be represented dynamically by conditioning the dependency between two signals with a Boolean expression. They differ from GCD in the labels of the edges in the graphs. In synchronous data-flow graphs, the labels are clocks which are encoded as first-order logic formulas. The synchronous data-flow dependency graphs are used as the common semantics framework of our translation validation for the scheduling phase of the SIGNAL compiler. We formalize the notion of "correct transformation" as a refinement relation between two synchronous data-flow dependency graphs. This relation expresses the preservation of the dependencies, whose existence can be checked by using a SMT solver. We also propose a technique to implement and integrate our validator within the POLYCHRONY toolset by the use of YICES solver.

In addition, we also propose a more precise deadlock detection approach for deadlockfree checking of synchronous programs written in SIGNAL language. Our approach permits the compiler avoiding emitting spurious decision on deadlock detection while the current technique does when dealing with numerical expressions. In our solution, the data dependencies among signals are represented by SDDG graphs, in which the nodes are signals or clock variables, edges are dependencies. Each edge is labeled by a condition expressed as a first-order logic formula at which the dependency is effective. We use a SMT solver to reason on the labels when deciding a dependency cycle in a SDDG to stand for a deadlock. In our work, we use the interval-Boolean abstraction as a more suitable abstraction to represent the condition of dependencies among signals to make a more efficient deadlock detection technique. The concept of interval-Boolean abstraction was introduced in [START_REF] Feautrier | Enhancing the compilation of synchronous data-flow programs with combined numerical-boolean abstraction[END_REF] by Gamatié et al. to make a more efficient static analysis of SIGNAL compiler.

The deadlock detection analysis presented in this chapter to the project POP [START_REF] Polychrony On | An eclipse project of the polarsys industry working group[END_REF], as such, it complements the case study of [START_REF] Nanjundappa | Synthesizing embedded software with safety wrappers through polyhedral analysis in a polychronous framework[END_REF] on synthesis safety wrappers for polychronous specifications through polyhedral analysis, and generalises the work presented in [START_REF] Jose | Smt based false causal loop detection during code synthesis from polychronous specifications[END_REF] on false-loop detection using SMT-solving to the case of a polyhedral analysis. This graph symbolically represents the computation of the outputs in the original program and their counterparts in the transformed program. The same structures are shared in the graph, meaning that they are represented by the same nodes. Assume that we want to show that two output variables have the same value. We simply need to check that they are represented by graphs which are rooted at the same graph node. We manage to realize the check by normalizing SDVGs using some rewrite rules.

For a transformation, our validator takes the input program and its transformed counterpart and constructs the corresponding SDVG for each output variable. Then it checks that for every output variable in the input program and its counterpart in the transformed program, they have the same values. If the result says that there exists any non-equivalence then the compiler emits a compilation error. Otherwise, the compiler continues its work. The integration of this verification process into the compilation process can be depicted as in Figure 6.1. The remainder of this chapter is organized as follows. Section 6.1 describes how code can be generated, as the final step of the compilation process, following different schemes. Section 6.2 illustrates the concept of SDVG and the verification procedure. In Fig. 6.1 A bird's-eye view of the verification process Section 6.3, we consider the formal definition of SDVG and the representation of SIGNAL program and generated C code as SDVGs. Section 6.4 addresses the mechanism of the verification process based on the rewrite rules and the normalization of a SDVG. It also presents the application of the verification process to the SIGNAL compiler, and its integration in the Polychrony toolset [START_REF]Polychrony toolset[END_REF]. Section 6.5 discusses some related works, concludes our work and outlines future directions.

Code generation in SIGNAL compiler

Code generation is the final step in the compilation process of SIGNAL compiler as depicted in Figure 6.2. When a program P has no deadlocks and is free of clock constraints one can generate code for P with the code generation functionalities of the POLYCHRONY toolset. The code can be generated for different general purpose languages (C, C ++ , and JAVA) on different architectures. The generated code in this case is called reactive code. However, one can generate a defensive code when the program has clock constraints; in this mode, alarms are emitted when a contraint is violated during the simulation.

The principle

The principle of code generation [START_REF] Besnard | Compilation of polychronous data-flow equations[END_REF] is based on the use of the clock hierarchy and the graph of conditional dependencies. The code generation follows the general scheme that is depicted in Figure 6.2. The generated code contains a main program which controls the step block. The step block consists of a step scheduler that drives the execution of its step component and updates the state variables corresponding to delay operators and local variables. The execution of the step block is scheduled by the step scheduler. The step component can be hierarchical, which consists of a set of sub-components called clusters.

The step component has its own local step scheduler. The step block communicates with its environment through the IO container.

I/O Container

State Variables

Step Component (Hierarchical)

Step Scheduler

Local Variables Main Fig. 6.2 Code generation: General scheme

In general, the generated program consists of several files. We consider that the target language code is C. For a process P, a main program is defined in the file P_main.c, the program which contains the step block called body program is defined in the file P_body.c. An input-output program which contains the IO container is defined in the file P_io.c. Each component of the generated code can be seen as a SIGNAL process. Then they can be reused in an embedding SIGNAL process.

The main program

The pseudo-code in Listing 6.1 shows the structure of the main program. It first opens the IO communication channels with the program environment and calls the initialization function. If everything goes fine then it calls the step function repeatedly in an infinite loop to interact with the environment. The infinite loop can be stopped if the step function returns the error code 0, meaning that the input stream is empty. And the main program will close the communication channels. All the called functions are defined in the body program. In the same way, we use a gated φ -function to represent the branching in C code. For instance, if C_N is true then the value of variable N is defined by the value of FB1 multiplied by 4. Otherwise, the value of N is never updated. This computation can be replaced by the following gated φ -function:

N = φ (C_N, 4 * FB1, ⊥)
We replace the variables C_CLK_36 and C_N by their definition, and we obtain the synchronous data-flow value-graph for the output N that is presented in Figure 6 Suppose that we want to verify that the signal N in the WHENOP and WHENOP_step (denoted by N c ) will have the same value. This can be done by showing that they are represented by the same subgraph. That means that they are labels of the same node in the graph. In the following, we say that they point to the same node in the graph. In Figure 6.3, we cannot conclude that they are equivalent, however we can transform the value-graph by applying normalization rules. First, by exploiting the generated program, C_FB1,C_FB2 are clocks of FB1 and FB2, respectively (the values of inputs FB1, FB2 are updated only when C_FB1,C_FB2 are valid). The first rule we shall apply is that: "If x is an input and the clock of x is read as input parameter (it is not defined in the program) then its clocks in SIGNAL program and C code are represented by the same node". Thus, FB1 and C_FB1 We shall go into details about the rules in the next section. After this replacement, and maximizing the variable sharing, the variable N in both programs points to the same node in the resulting graph (Figure 6.5). Therefore, we can conclude that the outputs are equivalent.

Synchronous data-flow value-graph

In this section, we describe the computation of a signal in a SIGNAL program and the corresponding variable in the generated C code in terms of SDVGs. Let us recall the computation of the output signal y in the equation y := x when b in the previous section. At any instant, the signal y holds the value of x if the following conditions are satisfied:

• x and b are defined.

• b holds the value true. Otherwise, it holds no value. Thus, at a given instant, to represent the underlying control conditions and the computation of this equation, we can use the following gated φ -function:

y = φ ( x ∧ b ∧ b, x, ⊥)
The condition ( x ∧ b ∧ b) represents the state in which x holds a value ( x = true), and b holds the value true ( b = true ∧ b = true). This section explores a method to construct that shared value-graph for both SIGNAL and generated C code programs, which is the computational model of our translation validation approach.

Definition of SDVG

Graphs can be used to describe many structures in computer science: program control flows, communication processes, computer networks, pointer structure on the heap and many others. In fact, for most activities in software development, many types of visual notations have been introduced, including UML, state diagrams, control flows graphs, block diagrams. These notations construct models that can be seen as graphs. This section intends to focus on graphs which represent expressions for computing the variable values in programs. We present basic definitions, including the notion of gated φ -function, and introduce a linear syntax presentation for terms represented as graphs. Finally, we provide the definition of our considered type of graph, synchronous data-flow value-graph. The interested readers can refer to [START_REF] Ehrig | Handbook of Graph Grammars and Computing by Graph Transformation[END_REF] for more detailed discussion on term graphs and linear syntax presentation for graphs.

Gated φ -function

In Static Single Assignment (SSA), a φ -node is placed at the confluence of a program control flow to represent the different choices of a variable. However, it does not contain the condition to determine which incoming branch reaching a confluence node is chosen. By contrast, gating functions are defined with some extra parameters to represent the conditions for choosing. To construct a SDVG, we shall employ the notation of gating function to capture the branching statements in computation of signals in synchronous data-flow programs and variables in the generated C code. Gating functions were first introduced by Ballance et al. in [START_REF] Ballance | The program dependence web: A representation supporting control, data, and demand driven interpretation of imperative languages[END_REF] to represent the conditions that guard the paths to a φ -node. There are several types of gating functions as follows:

• The gated φ -function, which is an if -then -else representation. It captures the condition for choosing a branch of the confluence node. For instance, x 3 = φ (c, x 1 , x 2 ) returns the value x 1 or x 2 depending on the value of c. If c is true, x 3 = x 1 and

x 3 = x 2 if c is false.
• The µ function is used to capture the initial and loop-carried values at the header of a loop. For instance, x 2 = µ(i = 1, n, x 0 , x 1 ) represents that x 2 's initial value is x 0 when i is the first iteration and its subsequent value is x 1 .

• The η function is placed at the loop exit. It selects the last value at the end of the loop. For instance, x 2 = η(i > n, x 1 ) means that x 2 takes the last value computed by the loop, x 1 .

Terms as trees and graphs

Let X and F be an infinite set of variables and a (finite or infinite) set of function symbols such that X ∩ F = / 0. Each f ∈ F, denoted by f (x 1 , x 2 , ..., x n ), where n is the arity of f , has a number of arguments (or arity) greater or equal to 0. Function symbols of arity 0 are called constants. Then the set of terms T is inductively defined by the following rules:

• Any variable is a term.

• Any expression f (t 1 ,t 2 , ...,t n ), where f ∈ F and t 1 , ...,t n ∈ T , is a term.

Given a term t, the substerms of t are t and if t = f (t 1 , ...,t n ), all subterms of t 1 , ...,t n . For example, let X = {x, y} and F = { f , g}, then T = {x, y, f (x), g(y), f (x, y)...}. Note that we do not assume that function symbols have fixed arities.

Definition 29 A directed term graph over X and F is a pair ⟨N, succ⟩ involving a (finite or infinite) set N of nodes which can be labeled by an element in X ∪ F and a function succ : N -→ N * . The set of nodes n 1 , ..., n k = succ(n) is the set of successors of n.

We write succ(n) i to denote the i th element of succ(n). The pair of nodes e = (n, succ(n) i ) is called an edge, the set of all edges is denoted by E. When we draw the visual representation of graphs, a directed edge e will go from n to succ(n) i , the ordering of the edges from n to succ(n) is left-to-right corresponding to the ordering of the elements of succ(n). Given a directed graph G = ⟨N, succ⟩, a path in G is a list of nodes (n 0 , n 1 , ..., n k ) where k ≥ 0 and n i+1 is a successor of n i . This path is said to be from n 0 to n k and k is the length of the path. A path of length greater than 0 from a node to itself is called a cycle, and the repeated node is called cyclic node. A graph which contains a cycle is a cyclic graph, otherwise it is acyclic. In a term graph, a path from the root is said to be rooted. The term graph is root-cyclic if there is a cycle containing the root. Given a directed graph G = ⟨N, succ⟩, let n be a node in G. The subgraph of G rooted at n is the term graph ⟨N ′ , succ ′ , n⟩ where N ′ = {n ′ ∈ N| there is a path from n to n ′ } and succ ′ is the restriction of succ to N ′ . We write

G | n = ⟨N G| n , succ G| n ⟩ to denote the fact that G | n is the subgraph rooted at n of G.
Consider, for example, the following directed graph which is depicted on the left of Figure 6.7. The subgraph rooted at the node labeled + is depicted as the second graph in the figure. The third graph is a root-cyclic graph. f and x are respectively a symbol function in F and a variable in X; nid ranges over a set, disjoint from X and F, of node identifiers. Any node identifier nid in a graph which identifies a node must occur exactly once in the context nid : x or nid : f (node, ..., node).

The constants are simply represented by symbol functions with arities equal to 0. This syntax is similar to the syntax for graphs in [START_REF] Barendregt | Towards an intermediate language based on graph rewriting[END_REF]. For instance, the three graphs of the examples in Figure 6.6 can be expressed in this syntax as follows: Note that multiple uses of the same node identifier mean that there are multiple references to the same node.

+(a
Definition 31 A tree is a term graph at the node r such that there is exactly one path from r to each node in the graph.

Based on the above definition, in Figure 6.7 the first and second graphs are trees and the third one is not. Thus it is obvious that a tree is always acyclic.

Homomorphisms of graphs and trees

Let G 1 = ⟨N 1 , succ 1 , r 1 ⟩ and G 2 = ⟨N 2 , succ 2 , r 2 ⟩ be two graphs, the definition of homomorphism is given as follows:

Definition 32 An homomorphism from G 1 to G 2 is a map f : N 1 -→ N 2 such that for all n ∈ N 1 ,
• f (n) and n have the same label

• succ 2 ( f (n)) = f (succ 1 (n))
where f (n 1 , ..., n k ) = ( f (n 1 ), ..., f (n k )). This definition states that homomorphisms preserve node labels, successors and their order. We write G 1 -→ G 2 to denote the fact that there is an homomorphism from G 1 to G 2 . Figure 6.8 shows an example of homomorphism. • An homomorphism f from G 1 to G 2 is rooted if f (r 1 ) and r 2 have the same label.

• An isomorphism is an homomorphism which is inverse. We denote an isomorphism from G 1 to G 2 by G 1 ∼ G 2 .

• When there is a rooted isomorphism from G 1 to G 2 , we say that they are equivalent, denoted by G 1 ≈ G 2 .

Proposition 6 For all graphs G 1 and G 2 , we have

G 1 ≈ G 2 implies G 1 ∼ G 2 .
Every rooted homomorphism from one tree to another is an isomorphism.

Synchronous data-flow value-graph

Let X be the set of all variables which are used to denote the signals, clocks and variables in a SIGNAL program and its generated C program. In our consideration, the functions which apply on signal values in the primitive stepwise functions are usual logic operators (not, and, or), numerical comparison functions (<, >, =, <=, >=, /=) and numerical operators (+, -, *, /). A constant is defined as a function symbol of arity 0. Thus in this chapter, we consider the set of function symbols which consists of the above functions and the gated φ -function, denoted by F.

As it is illustrated in Section 6.2, the computation of signals in a SIGNAL program and variables in the corresponding generated C code can be represented as a directed graph, in which a node can have multiple parents, and identical subgraphs are reused. That makes the maximal sharing among graph nodes. We shall consider the definition and examine some basic properties of SDVG. Formally, a SDVG is defined as follows:

Definition 34 A SDVG associated with a SIGNAL program and its generated C code is a directed graph G = ⟨N, E, I, O, l N , m N ⟩, where:

• N is a finite set of nodes.

• E ⊆ N × N is the set of edges. It describes the computation relation between the nodes.

• I ⊆ N is the set of input nodes. They are the input signals and their corresponding variables in the generated C code.

• O ⊆ N is the set of output nodes. They are the output signals and their corresponding variables in the generated C code.

• l N : N -→ X ∪ F is a mapping labeling each node with an element in X ∪ F. A node represents a clock, a signal, a variable, an operator or a gated φ -node function. And the subgraph rooted at a node is used to describe the computation of the corresponding element labeled at the node.

• m N : N -→ P(V ) is a mapping labeling each node with a finite set of clocks, signals, and variables. It defines the set of clocks, signals or variables in the SIGNAL program and the generated C code such that they are equivalent to the label of the node.

In the rest of this chapter, we denote the fact that there exists an edge between two nodes x and y by x -→ y. A path from x to y is any set of nodes s = {x 0 , x 1 , ..., x k } such that ∀i = 0, .., k -1, x i -→ x i+1 . An edge is a special case when k = 1. In a shared value-graph, the set of clocks, signals or variables {x 0 , ..., x n } that they are equivalent to the node labeled by y is written as a node with label {x 0 , ..., x n } y.

SDVG of SIGNAL programs

Let P be a SIGNAL program, we write X = {x 1 , ..., x n } to denote the set of all signals in program P which consists of input, output, state (corresponding to delay operator) and local signals, denoted by I, O, S and L, respectively. For each x i ∈ X, we use D x i to denote its domain of values, and D ⊥ x i = D x i ∪ {⊥} to denote its domain of values with the absent value, where ⊥ ̸ ∈ D x i . Then, the domain of values of X with absent value is defined as follows:

D ⊥ X = n i=1 D x i ∪ {⊥}
With each signal x i (Boolean or non-Boolean type), we attach a Boolean variable x i to encode its clock at a given instant (true: x i is present, false: x i is absent), and x i with the same type as x i to encode its value. Formally, the abstract values to represent the abstract clock and value of a signal can be represented by a gated φ -function, x i = φ ( x i , x i , ⊥), where x i and x i are computed using the following functions:

ˆ: X -→ B associates a signal with a Boolean value, ˜: X -→ D X associates a signal with a value of same type as the signal.

Assume that the computation of signals in processes P Suppose that we have the subgraphs that represent the equations y := x * x1 and x1 := x + 1 as depicted in Figure 6.9 (here, we omit to represent the abstract clocks of x and x1 at the node ŷ, x1 at the node +). We replace the node x1 by the subgraph which defines it while reusing the identical node x. As a result, the shared synchronous data-flow value-graph of P is depicted in Figure 6.10. A SIGNAL program is built through the set of primitive operators. Therefore, it is obvious that to construct SDVGs of SIGNAL programs, we shall construct a subgraph for each primitive operator. In the following, we present the value-graph corresponding to each SIG-NAL primitive operator. Consider the operator y := f (x 1 , ..., x n ), it indicates that if all signals from x 1 to x n are defined, then the output signal y is defined by the result of the function f on the values of x 1 , ..., x n . Otherwise, it is assigned no value. Thus, the computation of y can be represented by the following gated φ -function:

y = φ ( ŷ, f ( x 1 , x 2 , ..., x n ), ⊥) where ŷ ⇔ x 1 ⇔ x 2 ⇔ ... ⇔ x n
The synchronous data-flow value-graph of the stepwise functions is depicted in Figure 6.11. Note that in the graph, { x 1 , ..., x n }, ŷ means that the subgraph representing the computation of ŷ is also the computation of x 1 , ..., and x n . In other words, x 1 , ..., x n and ŷ are equivalent, meaning that they label the same node in the graph. For instance, consider the following SIGNAL equation:

y := x default (z + 1)
It can be represented by the nested φ -function, y = φ ( ŷ, φ ( x, x, z 1 ), ⊥), where we replace (z + 1) by the fresh signal z 1 . Thus the graphic representation is depicted in Figure 6.16.

{ ŷ} ∨ φ ⊥ { ỹ} φ x {ẑ} z 1 x φ { z 1 } + φ z φ 1
Fig. 6. [START_REF] Berry | Real-time programming: Special purpose or general purpose languages[END_REF] The graph of y := x default (z + 1)

Sampling

Consider the basic process which corresponds to the sampling operator y := x when b. If the signal x, b are defined and b holds the value true, then the signal y is defined and holds the value of x. Otherwise, y holds no value. The computation of y can be represented by the following node:

y = φ ( ŷ, x, ⊥) where ŷ ⇔ ( x ∧ b ∧ b)
The synchronous data-flow value-graph of the sampling operator is depicted in Figure 6.17. Note that in the graph, the clock ŷ points to the root of the subgraph of ( x ∧ b ∧ b). For instance, consider the following SIGNAL equation:

y := x when (z >= 1)
It can be represented by the gated φ -function, y = φ ( ŷ, x, ⊥), where ŷ ⇔ ( x ∧ z 1 ∧ z 1 ) and we replace (z >= 1) by the fresh signal z 1 . Thus the graphic representation is depicted in Figure 6.18.

Restriction

The shared synchronous data-flow value-graph of restriction process P 1 \x is the same as the graph of P 1 .

Clock relations

Given the above graph representations of the primitive operators, we can obtain the shared value-graphs for derived operators on clocks as depicted in Figure 6.19 and Figure 6.20.

Here, z is a signal of type event. Its computation can be represented by the following gated φ -function:

z = φ (ẑ, true, ⊥) { ŷ} ∧ φ ⊥ { ỹ} x φ x ∧ {ẑ} z 1 { z 1 } >= z 1 φ φ
Fig. 6.18 The graph of y := x when (z >= 1)

The clock relations between signals are given as follows:

z :=ˆx : ẑ ⇔ x xˆ= y : x ⇔ ŷ z := xˆ+ y : ẑ ⇔ ( x ∨ ŷ) z := xˆ * y : ẑ ⇔ ( x ∧ ŷ) z := xˆ-y : ẑ ⇔ ( x ∧ ¬ ŷ) z := when b : ẑ ⇔ ( b ∧ b) {ẑ} x {z} true ⊥ φ { x} ŷ {ẑ} ∨ {z} true ⊥ φ x ŷ (1)
(3)

SDVG translation validation

In this section, we introduce the set of rewrite rules to transform the shared value-graph resulting from the previous step. This procedure is called normalizing. At the end of the normalizing procedure, for any output signal x and its corresponding variable x c in the generated C code, we check whether x and x c point to the same node in the graph. That means they are represented by the same subgraph, meaning they have the same values. We also provide a method to implement the representation of synchronous data-flow value-graph and adapt the normalizing procedure with any future optimization of the compiler.

We introduce the graph rewriting techniques in Section 6.4.1. Section 6.4.2 provides the set of rewrite rules which is used to perform the normalizing procedure on the shared value-graph. In Section 6.4.3, we consider a method to implement the data structure of synchronous data-flow value-graph and the normalizing procedure.

An introduction to graph rewriting

Graphs provide a simple and powerful approach to a variety of problems of software engineering, and system modeling in particular. These graphs are mostly static descriptions of system states. Adding dynamics requires some ways to express state changes and thus graph transformations are involved, either explicitly or behind the scenes. In fact, the theory of graph transformation has found many applications in implementing functional languages based on term rewriting [START_REF] Turner | A new implementation technique for applicative languages[END_REF], in modeling of concurrent systems [START_REF] Ehrig | Handbook of Graph Grammars and Computing by Graph Transformation[END_REF] and in other areas such as software engineering, hardware designs and visual languages.

First, we recall the basic concepts of term rewriting, and we explain informally how it works in a simple example. We then define our notion of graph rewriting. For a comprehensive introduction of term rewriting and graph rewriting, the interested reader may consult the textbook [START_REF] Ehrig | Handbook of Graph Grammars and Computing by Graph Transformation[END_REF]. Consider, for example, the following rewrite rules for definition of natural number multiplication:

x * 0 -→ 0 x * (y + 1) -→ (x * y) + x

We shall apply the second rewrite rule to the expression t * (u + 1), where t and u are subex-pressions, which is represented by the graph on the left of Figure 6.23. When applying the above rewrite rule, the subexpression t is represented two times in the graph as depicted on the right of the figure. The subexpression t is evaluated two times if it has not been yet evaluated when we evaluate the expression. To solve this problem, an easy solution is, instead of copying the subexpression t, to create two references to the existing subexpression t, meaning that the repeated subterms are shared. Then the result of applying the above rewrite rule is given in Figure 6.24. Let X and F be the set of variables and function symbols, such that X ∩ F = / 0. We denote the set of all terms over X and F by T X,F . A mapping σ : T X,F -→ T X,F is called a substitution if σ (c) = c and σ ( f (t 1 , ...,t n ) = f (σ (t 1 ), ..., σ (t n )) for every constant c and term f (t 1 , ...,t n ).

Definition 35 A term rewrite rule over T X,F is a pair of terms (t l ,t r ), written as t l → t r , such that:

• t l is not a variable, and

• ∀x ∈ X.(x ∈ t r ⇒ x ∈ t l ).
The terms t l and t r are, respectively, the left and right-hand sides of the rewrite rule. A rewrite rule is left-linear (resp. right-linear) if no variable occurs more than once in its left-hand side (resp. right-hand side). A term rewriting system is a tuple ⟨F, R⟩, in which F is a set of function symbols and R is the set of term rewrite rules over T X,F . A term rewriting system is said to be left-linear (resp. right-linear) if all its rules are.

Given two terms t 1 and t 2 , we say that there exists a rewrite relation on T X,F for (t 1 ,t 2 ) induced by ⟨F, R⟩, denoted by t 1 t 2 , if it satisfies:

• There exists a rule (l, r) ∈ R and a substitution σ such that σ (l) is a subterm of t 1 .

• The term t 2 is obtained from t 1 by replacing the occurrence of σ (l) by σ (r).

We now define the application of term rewriting rules to graph, in other words, we make the graph representation of term rewriting rules. Let G = ⟨N G , succ G , r G ⟩ be a graph and n and n ′ be nodes of G, a triple (G, n, n ′ ) is called a graph rewrite rule and n, n ′ are the left root and the right root of the rule.

Given a graph G

0 = ⟨N 0 , succ 0 , r 0 ⟩, a pair ∆ = (r, f ) is a redex in G 0 if r is a graph rewrite rule (G, n, n ′ ) and f is an homomorphism from G | n to G 0 .
The homomorphism is called an occurrence of the rule r. We first begin with some example to illustrate the definition of graph rewriting technique by showing how the translation of term rewrite rules to graph rewrite rules works.

Let t l → t r be a term rewrite rule, we shall construct the corresponding graph rewrite rule (G, n, n ′ ). The construction works as follows. First we take the graphs representing both left and right hand sides of the term rewrite rule to form the union of these graphs, sharing those nodes which represent the same structures in t l and t r . This resulting shared graph is G. Then we take the roots of t l and t r to be n and n ′ , respectively. For example, we illustrate the construction of the graph rewrite rule for the following term rewrite rule:

φ (c, x, false) → c ∧ x
We first make the graph representing of φ (c, x, false) and c∧x on the left of the Figure 6.25. Then the union graph sharing the same nodes (c and x) is depicted on the right. Finally, the left root n and right root n ′ are the nodes labeled φ and ∧. Thus the graph rule is represented as follows:

(n : φ (n c : c, n x : x, false)

+ n ′ : ∧(n c , n x ), n, n ′ )
Let ((G, n, n ′ ), f : G| n → G 0 ) be a redex in the graph G 0 . We now present a formal definition of the general construction of the graph rewriting from a graph rewrite rule (G, n, n ′ ). The construction consists of three phases: build, redirection and garbage collection, which are defined as follows. The build phase The resulting graph

G 1 = ⟨N 1 , succ 1 , r 1 ⟩ in this phase, denoted by G 1 = G 0 + f (G, n, n ′ )
, is constructed as follows.

•

N 1 = N 0 ⊎ (N G| n ′ \ N G| n ),
where ⊎ denotes the disjoint union of two sets. For any node m ∈ N 1 , it has the same label as in G 0 if m ∈ N 0 . Otherwise, it has the same label as in G.

• r 1 = r 0 .

• for every node

m i = succ 1 (m) i , m i =          succ 0 (m) i if m ∈ N 0 succ G (m) i if m, succ G (m) i ∈ N G| n ′ \ N G| n f (succ G (m) i ) if m ∈ N G| n ′ \ N G| n , succ G (m) i ∈ N G| n
The redirection phase In this step all references to the node f (n) are replaced by the references to the node n ′ , the resulting graph is denoted by

G 2 = ⟨N 2 , succ 2 , r 2 ⟩ = G 1 [ f (n) := n ′ ].
This replacement is defined by a substitution of the node f (n) for the node n as follows:

• for every node c ∈ N 1 and c ∈ N 2 , they have the same label.

• for every node

c ∈ N 1 , succ 2 (c) i = n ′ if succ 1 (c) i = f (n), otherwise succ 2 (c) i = succ 1 (c) i . • r 2 = n ′ if r 1 = f (n), otherwise r 2 = r 1 .
The garbage collection phase In this last step, we define G 3 = G 2 | r 2 which is a part of the graph G 2 accessible from its root. We denote the graph G 3 by GC(G 2 ). Given a redex ∆ = (r, f ) and a graph G 0 , the construction of the graph resulting from reducing the redex ∆ in the graph G 0 , denoted by RED(∆, G 0 ), is defined as:

RED(((G, n, n ′ ) f ), G 0 ) = GC((G 0 + f (G, n, n ′ ))[ f (n) := n ′ ])
To illustrate the above construction of graph rewriting, we consider a graph rewriting rule (G, n, n ′ ), a graph G 0 , and an homomorphism f from G| n to G 0 as depicted in Figure 6.26. The graph rewriting rule (G, n, n ′ ) and G 0 are given as follows:

(G, n, n ′ ) = (n : φ (n c : c, n x : x, false) + n ′ : ∧(n c , n x ), n, n ′ ) G 0 = ∨(φ (c, x, false), y) c n : φ x f alse n ′ : ∧ c φ x f alse ∨ y Fig. 6.

An example of graph rewriting

We first copy the part of G| ′ n which is not contained in G| n to G 0 , with node labels, successors, and root defined in the build phase. We obtain the resulting graph G 1 . Then all edges of G 1 pointing to f (n) are replaced by edges pointing to the copy of n ′ , giving the graph G 2 as depicted in Figure 6.27. The root of G 2 is the root of G 1 if that node is not equal to f (n). Otherwise, the root of G 2 is the copy of n ′ as described in the redirection phase. From the graph G 2 , we remove all nodes which are not accessible from the root, giving the c copy of n':∧

x f (n) : φ f alse ∨ y c ∧ x φ f alse ∨ y (G 1 ) (G 2 )
Fig. 6.27 Graph rewriting: Build and redirection phases result of the rewrite, the graph G 3 as depicted in Figure 6.28.

rules that can be applied.

We classify our set of rewrite rules into three basic types: general simplification rules, optimization-specific rules and synchronous rules. In the following, we shall present the rewrite rules of these types, and we assume that all nodes in our shared value-graph are typed. Note that we only write the rewrite rules in form of term rewrite rules, t l → t r .

General simplification rules

The general simplification rules contain the rules which are related to the general rules of inference of operators, denoted by the corresponding function symbols in F. In our consideration, the operators used in the primitive stepwise functions and in the generated C code are usual logic operators (not, and, or), numerical comparison functions (<, >, =, <=, >=, /=), and numerical operators (+, -, *, /). When applying these rules, we will replace a subgraph rooted at a node by a smaller subgraph. In consequence of this replacement, they will reduce the number of nodes by eliminating some unnecessary structures. The first set of general simplification rules simplifies applied numerical and Boolean comparison expressions. In these rules, the term t represents a structure of value computing (e.g., the computation of expression b = x ̸ = true). The rules 6.3, 6.4, 6.5, and 6.6 only apply on the Boolean type. These rules are self explanatory, for instance, with any structure represented by a term t, the expression t = t can always be replaced with the value true.

The second set of general simplification rules eliminates unnecessary nodes in the graph that represent the φ -functions, where c, c 1 and c 2 are Boolean expressions. For better representation, we divide this set of rules into several subsets as follows.

φ (true, x 1 , x 2 ) → x 1 (6.7) φ (false, x 1 , x 2 ) → x 2 (6.8)
The rules in this set replace a φ -function with its left branch if the condition always holds the value true. Otherwise, if the condition holds the value false, it is replaced with its right branch.

φ (c, false, true) → ¬c (6.9)

φ (c, true, false) → c (6.10)

The rules operate on Boolean expressions represented by the branches. When the branches are Boolean constants and hold different values, the φ -function can be replaced with the value of the condition c.

φ (c, false, x) → ¬c ∧ x (6.11) φ (c, true, x) → c ∨ x (6.12) φ (c, x, false) → c ∧ x (6.13) φ (c, x, true) → ¬c ∨ x (6.14)
The rules operate on Boolean expressions represented by the branches. When one of the branches is Boolean constant, the φ -function can be replaced with a Boolean expression of the condition c and the non-constant branch. For instance, when the left branch is a constant and holds the value true, then the φ -function is replaced with the Boolean expression c ∨ x.

φ (c, x, x) → x (6.15)

The rule 6.15 removes the φ -function if all of its branches contain the same value. A φfunction with only one branch is a special case of this rule. It indicates that there is only one path to the φ -function as happens with branch elimination.

φ (c, φ (c, x 1 , x 2 ), x 3 ) → φ (c, x 1 , x 3 ) (6.16) φ (c, x 1 , φ (c, x 2 , x 3 )) → φ (c, x 1 , x 3 ) (6.17) φ (c, φ (¬c, x 1 , x 2 ), x 3 ) → φ (c, x 2 , x 3 ) (6.18) φ (c, x 1 , φ (¬c, x 2 , x 3 )) → φ (c,
φ (c 1 ∨ c 2 , x 1 , φ (c 1 , x 2 , x 3 )) → φ (c 1 ∨ c 2 , x 1 , x 3 ) (6.26) φ (c 1 ∨ c 2 , x 1 , φ (c 2 , x 2 , x 3 )) → φ (c 1 ∨ c 2 , x 1 , x 3 ) (6.27)
Consider a φ -function such that one of its branches is another φ -function. The rules 6.16 to 6.27 remove the φ -function in the branch if one of the following conditions is satisfied:

• The conditions of the φ -functions are the same (as in the rules 6.16 and 6.17).

• The condition of the first φ -function is equivalent to the negation of the condition of the second φ -function (as in the rules 6.18 and 6.19).

• The condition of the first φ -function either implies the condition of the second φfunction or its negation (as in the rules 6.20 to 6.23).

• The negation of the condition of the first φ -function either implies the condition of the second φ -function or its negation (as in the rules 6.24 to 6.27).

The following code segment in C illustrates the use of the above rewrite rules: If we analyze this code segment the return value is 0. In fact, a and b have the same value in both branches of the first "if" statement. Thus in the second "if" statement the condition is always true, then x always holds the value of d which is 0. We shall apply the general simplification rules to show that the value-graph of this code segment can be transformed to the value-graph of the value 0. We represent the value-graph in form of linear notation. The value-graph of the computation of x is φ (= (a, b), d, 0). Replacing the definition of a, b and d, and normalizing this graph, we get:

x →φ (= (φ (c, 0, 1), φ (c, 0, 1)), φ (c, φ (c, 0, 1), 0), 0) φ (true, φ (c, φ (c, 0, 1), 0), 0) by (6.1) φ (c, φ (c, 0, 1), 0) by (6.7)

φ (c, 0, 0) by (6.16) 0 by (6.15)

Optimization-specific rules

Based on the optimizations of the SIGNAL compiler, we have a number of optimizationspecific rules in a way that reflexes the effects of specific optimizations of the compiler. These rules do not always reduce the graph or make it simpler. One has to know specific optimizations of the compiler when she wants to add them to the set of rewrite rules. In our case, the set of rules for simplifying constant expressions of the SIGNAL compiler is given as follows.

• Specific rules for constant expressions with numerical operators: Consider the generated C code, we observe that the value of the variable z is always updated. It holds the value of x if C x is true, otherwise it is 0. Hence, we have the following rule that mirrors the above situation.

+(cst
x c → φ (true, x c , ⊥) → x → φ (true, x, ⊥) (6.38)

We write x → φ (true, x, ⊥) to denote that x points to the subgraph rooted at the node labeled by φ -function. The rule 6.38 indicates that if a variable in the generated C code is always updated, then we require that the corresponding signal in the source program is present at every instant, meaning that the signal never holds the absent value. In consequence of this rewrite rule, the signal x and its value when it is present x (resp. the variable x c and its updated value x c in the generated C code) point to the same node in the shared value-graph. Every reference to x and x (resp. x c and x c ) point to the same node.

For example, consider the value-graph in Figure 6.29, we rewrite the subgraph representing the clock ẑ and pz into a single node labeled by the value true. Then, we apply the rule 6.7 on the resulting graph, and we obtain the reduced graph in Figure 6.30.

A second synchronous rule mirrors the semantics of the delay operator. For instance, we consider the equation pz := z$1 init 0 in Listing 6.9. We use the variable m.z to capture the last value of the signal z. In the generated C program, the last value of the variable z c is The rule 6.39 indicates that for any signal x which is involved in a delay operator, and its corresponding variable in the generated C program, then it is required that the last values of x and x c are the same. Therefore, every reference to m.x c and m.x points to the same node.

Consider the value-graph in Figure 6.30, m.z c and m.z point to the same node by rule 6.39. Then, C_x and x are represented by the same subgraph. And any reference to C_x and x points to the same node in the graph as depicted in Figure 6.31. Finally, we add rules that mirror the relation between input signals and their corresponding variables in the generated C code. First, for any input signal x and the corresponding variable x c in the generated C code, if x is present, then the value of x which is read from the environment and the value of the variable x c after the reading statement must be equivalent. That means x c and x are represented by the same subgraph in the graph. Second, if the clock of x is also read from the environment as a parameter, then the clock of the input signal x is equivalent to the condition in which the variable x c is updated. It means that we represent x and C_x c by the same subgraph.

x c → G 1 + x → G 2 → x c , x → G 1 (6.40) C_x c → G 1 + x → G 2 → C_x c , x → G 1 (6.41)
Consequently, every reference to x and C_x c (resp. x and x c ) points to the same node.

Considering the value-graph of the program in Listing 6.10 and its generated C code, by rule 6.40 we obtain the final normalized graph that is depicted in Figure 6.32. We can observe that the value of the signal z and the corresponding variable z c are represented by the same subgraph. Therefore, we can safely conclude that the value of output signal z and the corresponding variable z c in the generated C code are equivalent.

Implementation

Given a SIGNAL program A, with an unverified compiler Cp, we consider the following derived compiler that is followed by a validator. The validator checks that for any output signal x in the source program A and the corresponding variable x c in the C program, they have the same values ( x = x c ). In other words, x and x c point to the same node in the shared value-graph. We denote this fact by C ⊑ val A. The main components of the validator are depicted in Figure 6.33. The validator works as follows. First, it constructs a shared value-graph that represents the computation of all signals and variables in both programs. The value-graph can be considered as a generalization of symbolic evaluation. The shared value-graph is transformed by applying some graph rewrite rules, this process is called normalization. The set of rewrite rules reflexes the general rules of inference of operators, or the optimizations of the compiler. For instance, consider the 3-node subgraph representing the expression 1 > 0, the normalization will transform that graph into a single node subgraph representing the value true, as it reflexes the constant folding.

Finally, it compares the values of the output signals and the corresponding variables in the C program. For every pair of output signal and its corresponding variable, the validator checks whether they point to the same node in the shared graph. Therefore, in the best case, when semantics has been preserved, this checking has constant time complexity O(1). In fact, it is always expected that most transformations and optimizations are semanticspreserving, thus the best-case complexity is important. In the second step, we shall normalize the above initial graph. Below is a potential normalization scenario, meaning that there might have more than one normalization scenario, and the validator can choose one of those. For example, given a set of rules that can be applied, the validator can apply these rules with different order. Figure 6.35 depicts the intermediate resulting graph of this normalization scenario. And Figure 6.36 is the final normalized graph from the initial graph when we cannot perform any more normalization.

• The clock of the output signal N is a master clock which is indicated in the generated C by the variable N c being always updated. By rule 6.38, the node { N, ZN} ∨ is rewritten into true.

• By rule ∧(true, x) → x, the node { FB} ∧ is rewritten into { FB} <=.

• The node φ -function representing the computation of N is removed and N points to the node { Ñ} φ by rule 6.7.

• The node φ -function representing the computation of ZN is removed and ZN points to the node { ZN} m.N by rule 6.7.

• The nodes FB c and FB are rewritten into a single node { FB} FB c by rule 6. In the final step, we check that the value of the output signal and its corresponding variable in the generated code merge into a single node. In this example, we can safely conclude that the output signal N and its corresponding variable N c is equivalent since they point to the same node in the final normalized graph.

Discussion

There is a wide range of works for value-graph representations of expression evaluations in a program. For example, in [START_REF] Weise | Value dependence graphs: Representation without taxation[END_REF], Weise et al. present a nice summary of the various types of value-graph. In our context, the value-graph is used to represent the computation of variables in both source program and its generated C code and identical structures are shared. We believe that this representation will reduce the required storage and make the normalizing process more efficient. Another remark is that the calculation of clocks as well as the special value, the absent value, are also represented in the shared graph.

Another related work which adopts the translation validation approach in verification of optimizations, Tristan et al. [START_REF] Tristan | Evaluating value-graph translation validation for llvm[END_REF], recently proposed a framework for translation validation of LLVM optimizer. For a function and its optimized counterpart, they compute a shared value-graph. The graph is normalized (the graph is reduced). After the normalizing, if the outputs of two functions are represented by the same sub-graph, they can safely conclude that both functions are equivalent.

On the other hand, Tate et al. [START_REF] Tate | Equility saturation: A new approach to optimization[END_REF] proposed a framework for translation validation. Given a function in the input program and the corresponding optimized version of the function in the output program, they compute two value-graphs to represent the computations of the variables. Then they transform the graph by adding equivalent terms through a process called equality saturation. After the saturation, if both value-graphs are the same, they can conclude that the return value of two given functions are the same. However, for the translation validation purpose, our normalization process is more efficient and scalable since we can add some rewrite rules into the validator that reflects what a typical compiler intends to do (e.g., a compiler will do the constant folding optimization, then we can add the rewrite rule for constant expressions such as three nodes subgraph 1 + 2 is replaced by a single node 3).

The present chapter provides a proof of the preservation of value-equivalence and applies this approach to the synchronous data-flow compiler SIGNAL. With the simplicity of the graph normalization, we believe that translation validation of synchronous data-flow value-graph for the industrial compiler SIGNAL is feasible and efficient. Moreover, the normalization process can always be extended by adding new rewrite rules. That makes the translation validation of SDVG scalable and flexible.

The proof of the preservation of value-equivalence might be extended to the whole compilation process of the SIGNAL compiler. To realize that, we shall prove that for every signal in the source program, if it is present then the corresponding variable in the generated C code is updated. Otherwise, if the signal is absent then the corresponding variable is never updated. In other words, for every clock associated with a signal and the corresponding Boolean value in the generated C code, thay are represented by the same subgraph. However, we have claimed in Chapter 1 that it is better to separate the concerns and proving for each phase the preservation of different kinds of semantics. CHAPTER 7 CONCLUSION

Summary of the contribution

Our aim in this dissertation was to present an approach to compiler verification that adopts translation validation to build a formally verified compiler verifier within the existing SIG-NAL toolset as described in Figure 1.5. By further decomposing translation validation following the successive compilation steps of the SIGNAL compiler, we were able to narrow down the problem to simpler proofs on simpler properties that observational equivalence. Moreover, the validator is smaller, modular and insensitive to minor updates of the compiler. In consequence, this works experiments with a solution that is in total significantly lighter in terms of efforts than a formal compiler verification, while providing, if not the same, a tangible level of assurance with respect to DO-330 requirements.

To realize this aim, we did not prove that all source programs and their generated code have the same semantics. Instead, we separated the proof into three smaller, independent, sub-problems: the proof of clock semantic preservation, the proof of data dependency preservation, and the proof of value-equivalence preservation of variables. These smaller proofs apply on different, successive, phases of the compilation process.

We have designed three special-purpose validators for each phase of the compilation process to carry out the proof of correctness. The validators benefit from the advantages of the translation validation approach and satisfy correctness requirements. The design of the validators is novel and constitutes the primary contribution of this work.

When solving the preservation of clock semantics problem, we defined a common semantic representation, called clock model, that is inspired by the interval-Boolean abstraction to represent clock semantics. With the efficiency of SMT solving, we found that representing the clock semantics with clock models is suitable and profitable compared to the approach based on model checking. The validator can deal with large programs and avoid the state-space explosion problem.

We define the concept of SDDGs as the common semantic framework in the translation validation to prove the preservation of data dependencies. The dependencies are dynamically represented by conditioning the dependencies with Boolean expressions. SDDGs differ from GCDs in the labels of the edges in the graphs. A refinement relation between two graphs expresses the preservation of the dependencies, whose existence can be checked, again, by using an SMT solver. In addition, a synchronous data-flow dependency graph in which the labels between nodes are encoded in the interval-Boolean abstraction, is used to make a more precise deadlock detection for the SIGNAL compiler.

For an output program of the static scheduling phase and its generated C program, we construct a shared value-graph to represent the computation of all signals and variables in both programs. This shared graph is normalized using a set of rewriting rules. An output signal x and its corresponding variable are checked equivalent iff they are represented by the same sub-graph. Symbolic evaluation and graph rewriting turn out to be valuable techniques to build validators. We believe that the use of symbolic evaluation and graph rewriting to prove the preservation of value-equivalence is novel. Moreover, normalization makes proofs scalable and flexible.

Finally, we have shown that it is possible to construct a validator to prove the correctness of the whole compilation process of the SIGNAL compiler. This validator can be considered as the modular composition of special-purpose validators. It ensures that the clock semantics, data dependencies among signals, and value-equivalence of variables are preserved when the compiler compiles a SIGNAL program into the corresponding generated C program. Should a new compilation module or phase be added, such as desynchronization, one could add another dedicated validator to prove its specific transformation correct.

The work on clock semantics has been published in the proceedings of the 9th International Conference on Integrated Formal Methods [START_REF] Ngo | Formal verification of compiler transformations on polychronous equations[END_REF] and presented in June 2012 in Pisa, Italy. The work on clock semantics of the code generation phase was accepted for presentation at IEEE International High-Level Design, Validation and Test Workshop HLDVT'12 in California, USA [START_REF] Ngo | Formal verification of automatically generated c-code from polychronous data-flow equations[END_REF]. The combined work on clock semantics and data dependencies has been published in Frontiers of Computer Science with special issue on Synchronous Programming, Springer journal in 2013 [START_REF] Ngo | Formal verification of synchronous data-flow program transformations toward certified compilers[END_REF]. The deadlock detection technique in Section 5.4 has been published in the proceedings of the 2014 Electronic System Level Synthesis Conference, ESLsyn 2014 [START_REF] Ngo | Efficient deadlock detection for polychronous data-flow specifications[END_REF] and presented in June 2014 in San Francisco, USA. The translation validation of synchronous data-flow value-graph is being prepared for some international conference and peer-review journal.

Future work

There is a number of possible directions for extending the proof of correctness of synchronous compiler. This work showed the use of SMT solver to prove the preservation of clock semantics and data dependencies. One possible next work is to fully implement the validators and the sets of experiments which demonstrate the capability of dealing with very large programs.

Considering the last phase of the compilation process, the executable code generation from SIGNAL to sequential C code, we provide a proof of correctness of the SIGNAL compiler for the preservation of value-equivalence. A possibility is to extend this proof to use with the other code generation schemes including cluster code with static and dynamic scheduling, modular code, and distributed code. One path forward is the combination of the work in Chapter 5 and Chapter 6. That means that we use synchronous data-flow dependency graphs and synchronous data-flow value-graphs as a common semantic framework to represent the semantics of the generated code. The formalization of the notion of "correct transformation" is defined as the refinements between two synchronous data-flow dependency graphs and in a shared value-graph as described in previous chapters.

Another possibility is that we use a SMT solver to reason on the rewriting rules. For example, we recall the following rules:

φ (c 1 , φ (c 2 , x 1 , x 2 ), x 3 ) → φ (c 1 , x 1 , x 3 ) if c 1 ⇒ c 2 φ (c 1 , φ (c 2 , x 1 , x 2 ), x 3 ) → φ (c 1 , x 2 , x 3 ) if c 1 ⇒ ¬c 2
To apply these rules on a shared value-graph to reduce the nested φ -functions (e.g., from φ (c 1 , φ (c 2 , x 1 , x 2 ), x 3 ) to φ (c 1 , x 1 , x 3 )), we have to check the validity of first-order logic formulas, for instance, we check that |= (c 1 ⇒ c 2 ) and |= c 1 ⇒ ¬c 2 . We consider the use of SMT to solve the validity of the conditions as in the above rewrite rules to normalize value-graphs.

The SME environment based on Model-Driven Engineering (MDE) technologies in the ECLIPSE environment is a front-end of the POLYCHRONY toolset that relies on the Eclipse Modeling Framework (EMF). It allows developers to write SIGNAL programs as graphical models based on the TOPCASED modeling facilities [134]. It would be interesting to construct a validator for the translation from graphical models into SIGNAL programs. It would

Listing 1 . 1

 11 Bug 15549 1 int lt ( _Bool b , unsigned char c )

Fig. 1 .

 1 Fig. 1.3 A bird's-eye view of translation validation framework

  Calculates the clock of all signals in the program and defines a Boolean abstraction of the program. The clock of a signal defines exactly when a signal shall be evaluated in a program. The intermediate representation of this phase is written in SIGNAL language. Static scheduling Based on the clock information and the Boolean abstraction obtained at the first stage, the compiler constructs the Conditional Dependency Graph (CDG) to represent the static schedule of all signals' evaluation.

  and Val(A,C) = true Error if Cp(A) = C and Val(A,C) = false Error if Cp(A) = Error

Fig. 1 . 5

 15 Fig. 1.5 The translation validation for the SIGNAL compiler

  and Val clk (A,C) = true Error if Cp sig (A) = C and Val clk (A,C) = false Error if Cp sig (A) = Error where Val clk (A,C) = true if and only if C ⊑ clk A.

  and Val dep (A,C) = true Error if Cp sig (A) = C and Val dep (A,C) = false Error if Cp sig (A) = Error where Val dep (A,C) = true if and only if C ⊑ dep A.1.4.3 Preservation of value-equivalence of variablesThis work focuses on proving that every output signal in the source program and the corresponding variable in the compiled program, the generated C program, have the same values. The computations of all signals and their compiled counterparts are represented by a shared value-graph, called Synchronous Data-flow Value-Graph (SDVG).

  and Val val (A,C) = true Error if Cp sig (A) = C and Val val (A,C) = false Error if Cp sig (A) = Error where Val val (A,C) = true if and only if C ⊑ val A.

  Clock extraction from Boolean signal: when b indicates the sub-clock [b]. It is the shortcut for b when b.

Example

  The following Signal program emits a sequence of values FB, FB -1, ..., 2, 1, from each value of a positive integer signal FB coming from its environment.

1 process 3

 3 DEC = 2 (? integer FB1 , FB2 , FB3 ; 3 ! integer N1 , N2 , N3 ) 4 (| N1 := DEC ( FB1 ) 5 | N1 := DEC ( FB2 )

Definition 10 (

 10 Stretch equivalence) The behaviors b and c are stretch-equivalent, written b ≶ c, iff there exists a behavior d such that d ≤ B b and d ≤ B c. For a behavior b, the class of all behaviors that are stretch-equivalent is denoted by b * . The stretch closure of a set of behaviors p, denoted by p * , is defined as p * = b∈p b * . In particular, it is interesting to consider the class of processes which contain all possible stretches of a given behavior. Definition 11 (Stretch closure) A process p is stretching-closed iff for all b ∈ p and all c ∈ B, c ≶ b ⇒ c ∈ p. A stretching-closed process p admits a set of strict behaviors, denoted (p) ≶ , such that (p) ≶ ⊂ p. It satisfies that for all behavior b ∈ p, there exists a unique behavior c ∈ (p) ≶ such that c ≶ b.

  the transition relation. Each transition is labeled by a polynomial over the set Y .

  ∀i ∈ I. (P ⇒ ∏ i∈I P i ) ≡ 0 denotes that the polynomial (P ⇒ ∏ i∈I P i ) is equivalent to the zero polynomial, which means that Sol((P ⇒ ∏ i∈I P i )) = Sol(0) = (Z/ 3 Z) m or Sol(P) ⊆ Sol(∏ i∈I P i ).

Fig. 4 . 2

 42 Fig. 4.2 The PDS translation validation

Listing 4 . 4

 44 Symbolic simulation implementation in SIGALI1 % internal function P1 = > P2 % 2 def implies ( P1 , P2 ) : 3 union ( complementary ( P1 ) , P2 ) ; 4 5 def states_simulat ion ( X_1 , Y_1 , X_1_nexts , Rel_1 , 6 ( X_1 , X_2 ) , X_1 _nexts_Y _1_bar = union_lvar ( X_1_nexts , Y_1_bar ) , X_2 _nexts_Y _2_bar = union_lvar ( X_2_nexts , Y_2_bar ) , X_1_X_2_nexts = union_lvar ( X_1_nexts , X_2_nexts ) do % compute the simulation %

  For the Boolean signal b, two Boolean variables b and b are used to represent its status: • ( b = true ∧ b = true) means b is present and holds a value true. • ( b = true ∧ b = false) means b is present and holds a value false. • ( b = false) means b is absent. Hence, at a given instant, the implicit control relations of the basic process above can be encoded by the following formula: ŷ ⇔ ( x ∧ b ∧ b) Let X = {x 1 , ..., x n } be the set of all signals in program P consisting of input, output, register (corresponding to delay operator), and local signals, denoted by I, O, R and L, respectively.

. 4 . 1 . 8 ExampleTwo uninterpreted function symbols v 1 <= and v 1 -

 41811 Applying the abstraction rules above, the clock semantics of the SIGNAL program DEC in Listing 3.3 is represented by the following first-order logic formula Φ(DEC), where ZN <= 1 and ZN -1 are replaced by two fresh variables ZN1 and ZN2, respectively. are used to encode the stepwise functions ZN1 := ZN <= 1 and ZN2 := ZN -1.

  the following sections, we denote input, output, register, memorization and local variables in a clock model by I clk , O clk , R clk , M clk and L clk , respectively. Note that the memorization variables are introduced only by the translation into clock models, they are not original in the SIGNAL programs. 4.4.1.9 Clock configuration Consider a clock model Φ(P) of the program P. Let X = I clk ∪ O clk ∪ R clk ∪ M clk ∪ L clk be the set of variables which is used to construct the clock model Φ(P). A clock configuration I is an interpretation over X such that it is a model of the first-order logic formula Φ(P). For instance,

  and ∀t, T c (t) ∈ S E c X (Φ(P))} Definition 20 Given the abstraction Φ(P), a property ϕ defined over the set of clocks X is satisfied by Φ(P) if for any interpretation Î, Î |= Φ(P) whenever Î |= ϕ, denoted by Φ(P) |= ϕ.

Proposition 3 Proof 6

 36 Let P, Φ(P) be a program and its abstraction, respectively, and ϕ is a property defined over the clocks. If Φ(P) |= ϕ then [[P]] c ⊆ Γ(ϕ). The proof of Proposition 3 is done by using Lemma 2. Given a clock trace T c ∈ [[P]] c , applying Lemma 2, T c ∈ Γ(Φ(P)) means that ∀t, T c (t) ∈ S E c X (Φ(P)). Since Φ(P) |= ϕ, then every interpretation Î satisfying Φ(P) also satisfies ϕ. Thus, any clock event I

  )) and [[P 2 ]] c ⊆ Γ(Φ(P 2 )), we have ∀t, T c (t) ∈ S E c X (Φ(P 1 )) and T c (t) ∈ S E c X (Φ(P 2 )). That means ∀t, T c (t) ∈ S E c X (Φ(P 1 ) ∧ Φ(P 2 )), or T c ∈ Γ(Φ(P)).

4. 4 . 3

 43 Definition of correct transformation: Clock refinement 4.4.3.1 Clock refinementLet Φ(A) and Φ(C) be two clock models of programs A and C, to which we refer respectively as a source program and its transformed counterpart produced by the compiler. We denote the sets of all signals in A, C by X A and X C , respectively. The corresponding sets of variables which are used to construct the clock models are denoted by X A and X C .

  IR(A)) ⊑ clk Φ(A)) return IR (

2 Fig. 4 . 4

 244 Fig. 4.4 The clock model translation validation

Listing 4 . 5

 45 DEC_BASIC_TRA in Signal 1 (| CLK := CLK_N ˆ-CLK_FB |) 2 | (| CLK_N := CLK_N ˆ+ CLK_FB 3 | CLK_N ˆ= N ˆ= ZN 4 In the first step, we will construct the clock models which are presented by the following first-order logic formulas Φ(DEC) and Φ(DEC_BASIC_TRA), respectively, where ZN <= 1, ZN c <= 1, ZN -1 and ZN c -1 are replaced by the fresh variables ZN1, ZN1 c , ZN2 and ZN2 c . The uninterpreted function symbols v 1 <= , v 1c <= , v 1 -and v 1c -are used to encode the step-wise functions ZN1 := ZN <= 1, ZN1 c := ZN c <= 1, ZN2 := ZN -1 and ZN2 c := ZN c -1:

•

  For a Boolean signal c, [c] and [¬c] depend on c. • Any dependency x c -→ y implies implicitly a dependency [c] [c] -→ y.

Fig. 5 . 2

 52 Fig. 5.2 The GCD of DEC

Fig. 5 .

 5 Fig. 5.3 CFG for Sum, with data dependency edges for i (dotted lines)

Fig. 5 . 5

 55 Fig. 5.5 The SDDG of DEC

  For every dependency path d p ∈ SDDG(P), we have d p ≼ dep d p and d p ≍ dep d p, thus SDDG(P) ⊑ dep SDDG(P). For every dependency path d p 3 ∈ SDDG(P 3 ), there exists a dependency path d p 2 ∈ SDDG(P 2 ) such that d p 2 ≼ dep d p 3 . Then, there exists a dependency path d p 1 ∈ SDDG(P 1 ) such that d p 1 ≼ dep d p 2 . Following the transitivity of the reinforcement, we have d p 1 ≼ dep d p 3 . In the same way, for every dependency path d p 3 ∈ SDDG(P 3 ), any dependency path d p 1 ∈ SDDG(P 1 ) satisfies d p 1 ≍ dep d p 3 . Therefore, SDDG(P 1 ) ⊑ dep SDDG(P 3 ).

  These considerations let us adapt the above definition of clock refinement as follows. Let SDDG(A) and SDDG(C) be two synchronous data-flow dependency graphs such that they have same set of input and output nodes, I A = I C and O A = O C . We say that C is a correct implementation of A if at any instant, the dependencies among the signals in I A ∪ O A are also the dependencies among the signals in I C ∪ O C . In other words, SDDG(C) ⊑ dep SDDG(A) on I A ∪ O A .

Figure 5 . 3 Fig. 5 .

 535 Figure 5.6 shows the main components of the validator. First, it takes the input program A and the counterpart transformed program C. It constructs the corresponding syn-

  We delegate checking the validity of the formulas in the previous step to a SMT solver. Let us illustrate the above process on the program DEC and its transformed program DEC_SEQ_TRA in Listing 5.1 at the scheduling phase of the SIGNAL compilation process. Listing 5.1 DEC_SEQ_TRA in Signal 1 (| when Tick ˆ= ZN ˆ= C_FB ˆ= C_CLK_12 2 | (| when C_FB ˆ= FB |) 3 | (| N := ( FB when C_FB ) default (( ZN -1) when C_CLK_12 ) 4 | ZN := N$1 init 1 5 | C_FB := ZN <= 1

Fig. 5 . 8

 58 Fig. 5.8 Dependencies among y, u, v

CHAPTER 6 EVALUATING

 6 SDVG TRANSLATION VALIDATION:FROM SIGNAL TO CIn Chapter 4 and Chapter 5, we provide approaches that are based on translation validation technique to prove the preservation of clock semantics and data dependency in the compilation process of the SIGNAL compiler. In this chapter, we describe how the preservation of value-equivalence of variables can be proved based on translation validation of synchronous data-flow value-graphs. It focuses on proving that every output variable in the original program and its counterpart in the transformed program, the generated C code, have the same values. The computation of all output variables and their counterparts is represented by a formal representation, called Synchronous Data-flow Value-Graph (SDVG).

  .3. Notice that the compiler prefers to write C_CLK_36 = (C_FB2?(FB2 >= 3) : FALSE) instead of C_CLK_36 = C_FB2&&(FB2 >= 3), which can be represented by the following gated φ -function: C_CLK_36 = φ (C_FB2, FB2 >= 3, false) The dashed arrows are not parts of the graph. They only mean that for each node, there is a set of labels that indicates which nodes of the graph correspond to which signals, clocks or variables in the programs. The SIGNAL program and its generated C program have been represented in the same graph. The nodes which represent the same structures (clocks, signals, variables and function symbols) have been reused. The unique occurrence of a reused node is said to be shared. For example, the nodes labeled >= and ⊥ are shared in the graph.The values of input signals and their corresponding variables in the generated C code are represented by the same nodes in the shared graph. In general, it is safe to assume that the values of input signals and the corresponding variables in the generated C code are equal. Thus, in the shared graph, the input signal values FB1, FB2 and the variables FB1, FB2 in the C code are represented by the same nodes.

6. 3 123 {N}FB2Fig. 6 . 3

 312363 Fig. 6.3 The shared value-graph of WHENOP and WHENOP_step

Fig. 6 . 4 Fig. 6 . 5

 6465 Fig. 6.4 The resulting transformed value-graph

  For example, let X = {a, b, c}, F = {+, * } be the set of variables and the set of function symbols, respectively. The set of nodes and the function succ is defined as follows:N = {+, * , a, b, c} succ(+) = (a, * ), succ( * ) = (b, c), succ(a) = (), succ(b) = (), succ(c) = ()This defines a directed graph which is depicted on the left of Figure6.6. Other directed graphs over F and X are depicted on the right side of the figure. Note that in the third graph, the nodes with repeated label b are represented by a same node, and the label is shared in the graph.

Fig. 6 . 6

 66 Fig. 6.6 The directed graphs of a + b * c and a + b, b * c

Fig. 6 . 7

 67 Fig. 6.7 The subgraph rooted at node labeled + and a root-cyclic graph

  , * (b, c)), +(a, b) + * (b, c) and + (a, nid 1 : b) + * (nid 1 , c)

Fig. 6 . 8

 68 Fig. 6.8 An example of homomorphism

Fig. 6 . 9

 69 Fig. 6.9 The subgraphs of y := x * x1 and x1 := x + 1

Fig. 6 .

 6 Fig. 6.10 The SDVG graph of P

{ x 1 ,Fig. 6 .Fig. 6 .

 166 Fig. 6.11 The graph of y := f (x 1 , ..., x n )

Fig. 6 .

 6 Fig. 6.17 The graph of y := x when b

Fig. 6 .Fig. 6 .

 66 Fig. 6.19 The graphs of (1) z :=ˆx, (2) xˆ= y and (3) z := xˆ+ y

Fig. 6 .

 6 Fig. 6.23 The transformation of the graph of t * (u + 1)

Fig. 6 .

 6 Fig.6.[START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF] The transformation of graph of t * (u + 1) with sharing of repeated subterms

Fig. 6 .

 6 Fig. 6.25 The graph rule of the term rule φ (c, x, f alse) → c ∧ x

  Fig. 6.29 The shared value-graph of MasterClk and MasterClk_step

  Fig. 6.30 The resulting graph of MasterClk and MasterClk_step by applying the rule 6.38

1 {zFig. 6 .

 16 Fig. 6.31 The resulting graph of MasterClk and MasterClk_step by applying the rule 6.39

Fig. 6 .

 6 Fig. 6.32 The final normalized graph of MasterClk and MasterClk_step

Fig. 6 .

 6 Fig. 6.33 A bird's-eye view of the SDVG translation validation

1 {NFig. 6 .

 16 Fig. 6.35 The resulting value-graph of DEC and DEC_step

{Fig. 6 .

 6 Fig. 6.36 The final normalized graph of DEC and DEC_step

  The tool interprets the test set definition and test run parameters. Then, it feeds the tests to the compiler. It might run the resulting programs to assert that the compiler passed by the test. As an example, the self-testing program of the SUPERTEST suite in Listing 2.1 checks the correctness of bit clear[START_REF]C++ Programming Language. Bitwise operators and bit manipulation[END_REF] implementation of a C ++ compiler.

	Listing 2.1 Bit clear test case with SUPERTEST
	1 # define COUNT	6
	2 int clear [ COUNT ] = {2 , 3 , 5 , 7 , 11 , 13};
	3
	4 void test_bitclear ( void ) {
	5	int i , bits , c ;
	6	bits = 0 xffff ;
	7
	8	for ( i = 0; i < COUNT ; i ++) {
	9	c = clear [ i ];
		bits &= ~(1 << c ) ;
		}
		/* the assertion */
		CVAL_VERIFY ( bits == 0 xd753 ) ;
	}

Table 3

 3

	.1 The implicit clock relations and dependencies
	• Clock difference: xˆ-y defines a clock as the set C x \ C y , which can be rewritten as
	when (not(ˆy) defaultˆx).
	Implicit clock relations and dependencies The above basic processes induce clock rela-
	tions and dependencies among signals. Table 3.1 shows these clock constraints for the prim-
	itive operators. In this table, the sub-clock [c] (resp. [¬c]) is defined as {t ∈ C c |c(t) = true}
	(resp. {t ∈ C c |c(t) = false}). Notice that a clock can be viewed as a signal with type event
	(which has only one value, true, when it is present), thus the condition C c means that the
	signal c is present.

  ZN t 0 t 1 t 2 t 3 t 4 t 5 t 6 t 7 t 8 t 9 7 C N t 0 t 1 t 2 t 3 t 4 t 5 t 6 t 7 t 8 t 9

			1 2
	5 C FB t 0	t 6	t 9
	6 C

  consider the program Altern in Listing 4.1. It is translated in the PDS model with variables a, b, x and zx corresponding to the signals A, B, X and ZX, and a state variable m.x introduced by the delay operator. The PDS model is given in Listing 4.2.

	6	| A ˆ= when X
	7	| B ˆ= when ZX
	8	|)
	9 where boolean X , ZX init false
	10 end ;
		Listing 4.2 PDS of ALTERN
	1 /* initial equation */
	2 m.x = -1
	3 /* evolution equation */
	4 m.x ′
	Listing 4.1 ALTERN in Signal

Table 4 .

 4

	Correct

1 Translation validation of PDSs: Experimental results

  If SDDG(P 1 ) ⊑ dep SDDG(P 2 ) and SDDG(P 2 ) ⊑ dep SDDG(P 3 ) then SDDG(P 1 ) ⊑ dep Reinforcement For every dependency path d p, we always have d p ≼ dep d p. Assume that d p 1 ≼ dep d p 2 and d p 2 ≼ dep d p 3 , we have

	SDDG(P 3 )
	Proof 10 The proof is based on the definitions of reinforcement, deadlock consistency and
	dependency refinement.
	Proposition 5 The reinforcement, deadlock consistency and dependency refinement are re-
	flexive and transitive:
	1. ∀d p, d p ≼ dep d p
	2. ∀d p, d p ≍ dep d p
	3. ∀SDDG(P), SDDG(P) ⊑ dep SDDG(P)

.., x ′ m ⟩ in SDDG(C) such that d p 2 ≼ dep d p 1 , 2. for every dependency path d p 1 = ⟨x 0 , x 1 , ..., x n ⟩ in SDDG(A), for any dependency path d p 2 = ⟨x ′ 0 , x 1 , ..., x ′ m ⟩ in SDDG(C), it satisfies d p 2 ≍ dep d p 1 .

Based on the definitions of reinforcement, deadlock consistency, and dependency refinement relations, important properties are given in Proposition 5.

4. If

d p 1 ≼ dep d p 2 and d p 2 ≼ dep d p 3 then d p 1 ≼ dep d p 3 5. If d p 1 ≍ dep d p 2 and d p 2 ≍ dep d p 3 then d p 1 ≍ dep d p 3 6.

  or d p 1 ≼ dep d p 3 . Deadlock consistency For every dependency path d p, we always have d p ≍ dep d p. Because d p 1 ≍ dep d p 2 and d p 2 ≍ dep d p 3 , we have |=

  1 , P 2 is represented as shared valuegraphs G 1 and G 2 , respectively. Then the value-graph G of the synchronous combination process P 1 |P 2 can be defined as G = ⟨V, E, I, O, m N ⟩ in which for any node x, we replace it by the subgraph that is pointed by x in G 1 , G 2 . And in G 1 and G 2 , every identical subgraph is reused, in other word, we maximize sharing among graph nodes in G 1 and G 2 . Thus, the shared value-graph of a SIGNAL program P can be constructed as a combination of the sub-value-graphs of its equations as above.

	To demonstrate the above combination rule, we consider a simple SIGNAL program P
	as follows:
	Listing 6.5 Simple Program in SIGNAL
	1 process P =
	2 (? integer x ;
	3 ! integer y )
	4 (| y := x * x1
	5 | x1 := x + 1
	6 |)
	7 where integer x1
	8 end ;

  x 1 , x 2 ) (6.19) φ (c 1 , φ (c 2 , x 1 , x 2 ), x 3 ) → φ (c 1 , x 1 , x 3 ) if c 1 ⇒ c 2 (6.20) φ (c 1 , φ (c 2 , x 1 , x 2 ), x 3 ) → φ (c 1 , x 2 , x 3 ) if c 1 ⇒ ¬c 2 (6.21) φ (c 1 ∧ c 2 , φ (c 1 , x 1 , x 2 ), x 3 ) → φ (c 1 ∧ c 2 , x 1 , x 3 ) (6.22) φ (c 1 ∧ c 2 , φ (c 2 , x 1 , x 2 ), x 3 ) → φ (c 1 ∧ c 2 , x 1 , x 3 ) (6.23) φ (c 1 , x 1 , φ (c 2 , x 2 , x 3 )) → φ (c 1 , x 1 , x 2 ) if ¬c 1 ⇒ c 2 (6.24) φ (c 1 , x 1 , φ (c 2 , x 2 , x 3 )) → φ (c 1 , x 1 , x 3 ) if ¬c 1 ⇒ ¬c 2 (6.25)

  1 , cst 2 ) → cst, where cst = cst 1 + cst 2 (6.28) * (cst 1 , cst 2 ) → cst, where cst = cst 1 * cst 2(6.29)

-(cst 1 , cst 2 ) → cst, where cst = cst 1cst 2 (6.30) /(cst 1 , cst 2 ) → cst, where cst = cst 1 /cst 2 (6.31)

Les langages synchrones tels que SIGNAL, LUSTRE et ESTEREL sont dédiés à la conception de systèmes critiques. Leurs compilateurs, qui sont de très gros programmes complexes, peuvent a priori se révéler incorrects dans certains situations, ce qui donnerait lieu alors à des résultats de compilation erronés non détectés. Ces codes fautifs peuvent invalider des propriétés de sûreté qui ont été prouvées en appliquant des méthodes formelles sur les programmes sources. En adoptant une approche de validation de la traduction, cette thèse vise à prouver formellement la correction d'un compilateur optimisé et industriel de SIGNAL. La preuve de correction représente dans un cadre sémantique commun le programme source et le code compilé, et formalise une relation entre eux pour exprimer la préservation des sémantiques du programme source dans le code compilé.

process ALTERN =

(? event A , B ;

!)

(| X := not ZX

| ZX := X$1

(|

| x := expression

| z := expression

ACKNOWLEDGEMENTS

I would like to express my gratitude to my advisor, Jean-Pierre Talpin. Thanks for all his support, my three years of Ph.D. have been a very useful time. I learnt much from his

Code generation

The clocked and scheduled Signal program is ready to directly generate executable code (e.g., sequential code in C or JAVA).

Chapter plan

In the remainder of this dissertation, the chapter structure is as follows:

• Chapter 2 surveys related works in the field of verification of the correctness of the compilation process.

• Chapter 3 introduces the concept of synchronous programming. We study the SIGNAL language as an instance of multi-clocked synchronous data-flow languages used to describe reactive systems, specially safety-critical systems.

• Chapter 4 presents our methods of proving the preservation of clock semantics when the SIGNAL compiler calculates the clock information and makes the Boolean abstraction.

Translation validation of transformations on clocks loop x = intersection (x , forall ( forall ( exist ( implies ( Rel_1 , exist ( intersection ( Rel_2 , rename (x , X_1_X_2 , X_1_X_2_nexts ) ) , X_2_nexts_Y_2_bar ) ) , Y_1_bar ) ,Y ) , X_1_nexts ) ) init 0; def ilts_simulation ( S_I1 , S_I2 ) : with % get the components of iLTS1 % I_1 = initial_I ( S_I1 ) , X_1 = state_var_I ( S_I1 ) , X_1_nexts = state_var_next_I ( S_I1 ) , Y_1 = event_var_I ( S_I1 ) , Rel_1 = trans_rel_I ( S_I1 ) , % get the components of iLTS2 % I_2 = initial_I ( S_I2 ) , X_2_d = state_var_I ( S_I2 ) , X_2_nexts_d = state_var_next_I ( S_I2 ) , Y_2 = event_var_I ( S_I2 ) , Rel_2_d = trans_rel_I ( S_I2 ) , % rename the states variables % X_2 = declare_suff ( X_2_d ) , X_2_nexts = declare_suff ( X_2_nexts_d ) , Rel_2 = rename ( Rel_2_d , union_lvar ( X_2_d , X_2_nexts_d ) , union_lvar ( X_2 , X_2_nexts ) ) , states_sim = states_simulation ( X_1 , Y_1 , X_1_nexts , Rel_1 , X_2 , Y_2 , X_2_nexts , Rel_2 ) do % compute the systems simulation % intersection ( states_sim , forall ( implies ( I_1 , exist ( intersection ( states_sim , I_2 ) , X_2 ) ) , X_1 ) ) ;

We provide an implementation of algorithm in Listing 4.3 to compute the greatest simulation for two ILTSs. The implementation uses some useful functions from the kernel of the checker SIGALI. The inputs are the concrete and abstract ILTSs S_I1 and S_I2, respectively.

Process P Clock semantics

where

where

Detected bugs

So far, our validator has revealed two previously unknown bugs in the compilation of the SIGNAL compiler. One of them is related to the multiple constraints of clocks. Another one is a syntax error of generated C code from a SIGNAL program in which a constant signal is used.

The first problem was introduced when multiple constraints condition a clock such as in the following segment of SIGNAL program and its clock calculation part in transformed programs: In the transformed counterpart P_BASIC_TRA, the introduction of signal XZX_24 and the synchronization between CLK and XZX_24 cause the incorrect specification of clocks (in program P_BASIC_TRA, the signal x might be absent when XZX_24 is absent, which is not the case in the source program P, nor in P_BOOL_TRA). This bug was caught by our validator when it found that Φ(P_BOOL_TRA) ̸ ⊑ clk Φ(P_BASIC_TRA). In addition, signal XZX_24 is introduced without declaration, which makes a syntax error in P_BASIC_TRA.

The second problem detected was not found by the translation validation but was indirectly discovered when trying to apply it. It occurred in a SIGNAL program in which a merge operator with a constant signal was used, such as y := 1 default x. In this case, the code generation phase of the compiler dealt wrongly with the clock context of a constant signal by introducing a syntax error in the generated C code. The bug and its fix are given by: tween data is conditioned by a clock. We will illustrate this technique with an example (a more detailed discussion is presented in [START_REF] Maffeïs | Distributed implementation of signal: Scheduling and graph clustering[END_REF]).

The SIGNAL program in Listing 5.2 emits an integer sequence v whose ith value v i is the double of the input x i depending on the other input c. A possible run of the program is depicted by the following trace: Apply the Z/ 3 Z encoding scheme on the program CycleDependency, we have the following algebraic coding, where we introduce three fresh variables c 1 , c 2 and v 1 to replace the expressions (c <= 0), (c >= 1) and (v when c 1 ), respectively:

Given the algebraic encoding above, the SIGNAL compiler can establish the dependencies among signals y, u and v as a graph of conditional dependencies which is depicted in Figure 5.8. Based on GCD graphs, the SIGNAL compiler identifies the potential deadlocks in the program. Such a bad dependency between signals will appear as a cycle in the graph if the product of the labels of its edges is not the null clock.

• φ (x) = x if x is of Boolean type; φ (x) = true if x is of event type.

• φ (x) = inv(x) if x is of non-Boolean type, where inv(x) is the interval of x.

), an approximation of numerical operations on intervals, corresponding to as in [START_REF] Alefeld | Introduction to interval computation[END_REF]. For example, for addition operation i + j ≡ [i -+ j -, i + + j + ], where i -and i + are respectively the lower and upper bounds of the interval i.

Delay Considering the delay operator, y := x$1 init a, its encoding φ (y := x$1 init a)

contributes to Φ(P) with the following conjunct. This encoding requires that at any instant, signals x and y have the same clock. If they are numerical signals, then they have the same interval. Otherwise, we introduce a memorization variable m.x that stores the last value of x. The next value of m.x is m.x ′ and it is initialized to a in m.x 0 .

Merge The encoding of the merge operator, y := x default z, contributes to Φ(P) with the following conjunct:

Sampling The encoding of the sampling operator, y := x when b, contributes to Φ(P) with the following conjunct:

Composition Consider the composition of two processes P 1 and P 2 . Its abstraction φ (P 1 |P 2 ) is defined by φ (P 1 ) ∧ φ (P 2 ).

Interval analyzer This step determines the interval of every signal in the program. For every input signal, it is assumed that its interval is known. This step applies the algorithm presented in [START_REF] Gonnord | Abstract acceleration to improve precision on linear relation analysis[END_REF]. The tool in [START_REF] Lalire | Interproc: An inter-procedural analyzer for imperative languages[END_REF] is used to compute an over-approximation of the variation interval of each numerical signal.

Abstraction The input program is encoded according to the Boolean-interval abstraction scheme in Section 5.4.2.1. The output of this step is a first-order logic formula.

SDDG + construction After obtaining the interval analysis and the abstract model of the input program, this step will construct the corresponding SDDG + graph according to the rules in Table 5.2. The labels of edges in the graph are encoded as first-order logic formulas based on the above Boolean-interval abstraction scheme. In this step, the tool also detects all dependency cycles in the graph and produces the conjunction formula of all clock labels for each cycle as input for the solver.

SMT-based proof

We delegate checking the validity of the formulas to a SMT solver. Our implementation uses the Yices [START_REF] Dutertre | Yices smt solver[END_REF] solver.

Let us illustrate the above deadlock detection technique on the program CycleDependency.

In the first step, we shall determine the variation interval for all signals in the program. We assume that the variation intervals for input signals x and c are (-∞, +∞), (-∞, +∞). After the analysis, we get: x ∈ (-∞, +∞), c ∈ (-∞, +∞), y ∈ (-∞, +∞), u ∈ (-∞, +∞), v ∈ (-∞, +∞). Recall that we rewrite equation at lines (4) and (6) as follows:

In the second step, Boolean-interval abstraction, our tool will translate the program into a logic formula Φ according to the above abstract scheme. Let us focus on the clocks of signals y, u, and v, which are given as follows:

In the third step, we construct the SDDG + graph in Figure 5.9. Here, we detect that there Evaluating SDVG translation validation: from SIGNAL to C 8 P_stepIO_begin () ; 9 code = P_step () ; P_stepIO_end () ; } P_CloseIO () ; }

The step block

Once the IO communication channels and the initialization are completed, the step function P_step() is responsible for the calculation of the effect of one synchronous step of the system to interact with the environment. It is the essential part of the concrete code. It reads data from the input streams, computes the outputs and writes the results to the output streams. In the POLYCHRONY toolset, the implementation of the step function can be done in many schemes based on the clock hierarchy and the graph of conditional dependencies. These code generation schemes consist of:

• Global code generation: sequential code, clustered code with static scheduling, clustered code with dynamic scheduling.

• Modular code generation.

• Distributed code generation.

The next section will describe the sequential, inlining code generation of the step block. For other code generation schemes, interested readers can refer to [START_REF] Aubry | Synchronous distribution of signal programs[END_REF][START_REF] Gautier | Code generation in the sacres project[END_REF][START_REF] Maffeïs | Distributed implementation of signal: Scheduling and graph clustering[END_REF].

The IO container

The IO container implements the communication of the generated program with the environment in case the being compiled process contains input and output signals. In the simulation mode, each input or output signal communicates with the environment via a file as the input stream or output stream. The IO container in Listing 6.

Sequential code generation

In the context of this work, we shall consider the sequential, inlining code generation scheme for the step function that directly interprets the SIGNAL process obtained after the clock calculation, Boolean abstraction, and scheduling phases of the compiler front-end. We describe the code structure of the step function for a simple process represented in Listing 6.3. The step function obtained by compiling it is given in Listing 6.4. The C code introduces an explicit variable for each signal to represent the clock. Variable C_N is the clock of N and C_FB1,C_FB2 are the clocks of FB1 and FB2, respectively. As soon as the clock is evaluated and is true, the signal is read if it is an input signal or updated, otherwise. The precedence of the statements must be consistent with the graph of conditional dependencies, and one can observe the tree structure of conditional if-then-else statements which expresses directly the clock hierarchy. Taking into account that N in C code is the value of the corresponding signal in SIGNAL program, we have an observation that in a run of the step function, the value of N is unchanged when C_N, the clock of N, has the value false. Intuitively, based on this observation, we can say that if there is a variable in the generated C program whose value is never updated in a run of the step function. Then it will be assigned no value, denoted as ⊥. In the next sections, we shall show how this assumption can be formalized to represent the computation of step function as a shared value-graph.

Illustrative example

We begin by showing how our verification process works for an illustrative example. Consider the synchronous program WHENOP written in SIGNAL language which is given in Listing 6. In this example, we use the concept of gated φ -function such as x = φ (c, x 1 , x 2 ) that is mentioned in more details in the next sections. It is used to represent a branching in a program, which means x takes the value of x 1 if the condition c is satisfied, and the value of x 2 , otherwise. Since the generated C programs use persistent variables (i.e. variables that always have some values), while SIGNAL programs which use volatile variables. We shall assume that if a variable (including the input and output variables) in the generated C program is such that its value is never updated then it will be assigned the absent value, denoted as ⊥. If a statement involves a variable x before its value update then the value of this variable is the previous value, denoted as m.x.

Considering the equation N := 4 * FB1 when (FB2 >= 3), at a considered instant t, the signal N is present if the signals FB1, FB2 are present and FB2 is greater than or equal to 3. When N is present, its value is defined by the value of FB1 multiplied by 4. The value of N is ⊥ when it is absent. The computation of this equation can be replaced by the following gated φ -function:

where For instance, consider the following SIGNAL equation:

and c

It can be represented by the gated φ -function, y = φ ( ŷ, x 1 ∧ c, ⊥), where we replace (x >= 1) by the fresh signal x 1 . Thus the graphic representation is depicted in Figure 6.12.

φ c φ Fig. 6.12 The graph of y := (x >= 1) and c

Delay

Consider the basic process which corresponds to the delay operator y := x$1 init a. The output signal y is defined by the last value of the signal x when the signal x is present. Otherwise, it is assigned no value. Thus, the computation of y can be represented by the following nodes: y = φ ( ŷ, m.x, ⊥) and m.x 0 = a where ŷ ⇔ x m.x and m.x 0 are the last value of x and the initialized value of y. The synchronous data-flow value-graph of the delay operator is depicted in Figure 6.13. Note that in the graph, { x} ŷ means that the clocks x and ŷ are equivalent, meaning that they point to the same node in the graph.

For instance, consider the following SIGNAL equation:

Merge

Consider the basic process which corresponds to the merge operator y := x default z. If the signal x is defined then the signal y is defined and holds the value of x. The signal y is assigned the value of z when the signal x is not defined and the signal z is defined. When both x and z are not defined, y holds no value. The computation of y can be represented by the following node:

The representation uses a nested φ -function which indicates that when ŷ is true, y is defined by the gated φ -function φ ( x, x, z). Otherwise, it holds no value. The synchronous data-flow value-graph of the sampling operator is depicted in Figure 6.15. Note that in the graph, the clock ŷ is represented by the subgraph of x ∨ ẑ.

function repeatedly in an infinite loop to interact with the environment.

• A_body.c is the implementation of the initialization function and the step function.

The initialization function is called once to provide initial values to the program variables. The step function, which contains also the step initialization and finalization functions, is responsible for the calculation of the outputs to interact with the environment. This function, which is called repeatedly in an infinite loop, is the essential part of the concrete code.

• A_io.c is the implementation of the IO communication functions. The IO functions are called to setup communication channels with the environment.

The scheduling and the computations are done inside the step function of the generated C program. Therefore, it is natural to construct a sub value-graph of this function in order to prove that its variables and the corresponding signals have the same values. To construct the value-graph of the step function, the following considerations need to be studied. An original signal named x has a corresponding Boolean variable named C_x in the step function. Then the computation of x is implemented by conditional if -then -else statements as follows:

If x is an input signal then its computation is the reading operation which gets the value of x from the environment. In case x is an output signal, after computing its value, it will be written to the IO communication channel with the environment. Note that the C programs use persistent variables (e.g. variables which always have some value) to implement the input SIGNAL programs which use volatile variables. As a result, there is a difference in the types of a signal in a SIGNAL program and of the corresponding variable in the C program. When a signal has the absent value, ⊥, at a given instant, the corresponding C variable always has a value. For instance, in the step function WHENOP_step(), we observe that the value of variable N is maintained when the Boolean variable C_N has the value false as in the following code segment:

This consideration implies that we have to detect that a variable in the C program whose value is never updated. In this case, it will be assigned the absent value, ⊥. Thus, the computation of such variables, called x c , can fully be represented by a gated φ -function as follows:

x c = φ (C_x c , x c , ⊥)

where x c denotes the newly updated value of the variable. For example, we consider the generated code of basic process corresponding to the primitive operator merge in Listing 6.6.

Listing 6.6 SDVGMerge in SIGNAL The generated C code of the step function is given in Listing 6.7. The computation of variable z in this function can be represented by the following gated φ -function:

The shared value-graph of SDVGMerge_step() is depicted in Figure 6.21. In this graph, we replace the node φ (C_cx c , φ ( cx c , x c , ⊥), ⊥) by φ (C_cx c ∧ cx c , x c , ⊥). We do the same for the node φ (C_cy c , φ ( cy c , y c , ⊥), ⊥).

Listing 6.7 Generated C code of SDVGMerge φ φ In the generated C program, the computation of the variable whose clock is the master clock, which ticks every time the step function is called, is implemented without the condi-tional if -then -else statement and it is always updated when the step function is invoked. The computation of such variables can be represented by a node in the shared value-graph as follows:

That means that the the variable x c is always updated and holds the value x c . For instance, we consider the following C code segment, it is generated from the program DEC in Listing 3.3 which computes the values of the output signal N.

The computation of N can be represented by the sub value-graphs in Figure 6.22, where m.N c denotes the previous value of the variable N. Considering the following code segment, the observation is that the variable x is involved in the computation of the variable y before the updating of x. The normalizing algorithm indicates that we apply the rewrite rules to each graph node individually. When there is no more rules that can be applied to the resulting graph, we maximize the shared nodes. The process terminates when there exists no more sharing or • Specific rules for constant expressions with numerical comparison functions:

where = <, >, =, <=, >=, /=, and the Boolean value cst is the evaluation of the constant expression (cst 1 , cst 2 ) which can hold either the value false or true.

We also may add a number of rewrite rules that are derived from the list of rules of inference for propositional logic. For example, we have a group of laws for rewriting formulas with and operator, such as:

We consider the following SIGNAL program and its generated C code, the input signal x is present when the other Boolean input signal cx holds the value true. The computation of x is represented by x = φ ( x, x, ⊥), where x ⇔ cx ∧ cx. In the generated C code, the value of x is read only when the condition C_cx ∧ cx is true. That is represented by x = φ (C_cx, φ (cx, x, ⊥), ⊥). This observation makes us add the following rewrite rule Evaluating SDVG translation validation: from SIGNAL to C into the systems to mirror the above rewriting of the SIGNAL compiler.

(6.37)

Synchronous rules

In addition to the general and optimization-specific rules, we also have a number of rewrite rules that are derived from the semantics of the code generation mechanism of the SIGNAL compiler. To illustrate why the synchronous rules need to be added in our validator, we consider the SIGNAL program in Listing 6.9 and the corresponding generated C code in Listing 6.10. The shared value-graph of the SIGNAL program and its generated C code is given in Figure 6.29. Listing 6.9 MasterClk in SIGNAL

ABSTRACT

Synchronous languages such as SIGNAL, LUSTRE and ESTEREL are dedicated to designing safety-critical systems. Their compilers are large and complicated programs that may be incorrect in some contexts, which might produce silently bad compiled code when compiling source programs. The bad compiled code can invalidate the safety properties that are guaranteed on the source programs by applying formal methods. Adopting the translation validation approach, this thesis aims at formally proving the correctness of the highly optimizing and industrial SIGNAL compiler. The correctness proof represents both source program and compiled code in a common semantic framework, then formalizes a relation between the source program and its compiled code to express that the semantics of the source program are preserved in the compiled code.