Zhibin Yang

Jean-Paul Bodeveix

Mamoun Filali

Towards a Simple and Safe Objective Caml Compiling Framework for the Synchronous Language SIGNAL

Keywords: Synchronous Languages, SIGNAL, Synchronous Clocked Guarded Actions (S-CGA), Objective Caml, Functional Programming

This paper presents a simple and safe compiler, called MinSIGNAL, from a subset of the synchronous dataflow language SIGNAL to C, as well as its existing enhancements. The compiler follows a modular architecture, and can be seen as a sequence of source-to-source transformations applied to an intermediate representation which is named Synchronous Clocked Guarded Actions (S-CGA) and translation to sequential imperative code. Objective Caml (OCaml) is used for the implementation of MinSIGNAL. As a modern functional language, OCaml is adapted to symbolic computation and so, particularly suitable for compiler design and implementation of formal analysis tools. In particular, the safety of its type checking allows to skip some verification that would be mandatory with other languages. Additionally, this work is a basis for the formal verification of the compilation of SIGNAL with a theorem prover such as Coq.

Introduction

Safety-critical systems are widely used in the fields of avionics, space systems, and nuclear power plants. Many of them are also considered as reactive systems [START_REF] Harel | On the development of reactive systems[END_REF], because they al-E-mail: yangzhibin168@163.com, bodeveix@irit. f r, f ilali@irit. f r ways continuously interact with their environment. The environment can be some physical devices to be controlled, a human operator, or other reactive systems. These systems receive from the environment input events, and compute the output information, which are finally returned to the environment. Synchronous programming is an important choice to design these systems, which relies on the synchronous hypothesis [START_REF] Potop-Butucaru | The synchronous hypothesis and synchronous languages[END_REF]. Firstly, the computation time is abstracted as zero, that lets system behaviors be divided into a discrete sequence of instants. At each instant, the system does inputcomputation-output, which takes zero time. Secondly, the different arrival time of events are abstracted as the relative order between events. Even if the physical time is abstracted, the inherent functional properties are not changed, so we can say this method focuses on functional behaviors at a platform-independent level.

There are several synchronous languages, such as ES-TEREL [START_REF] Boussinot | The Esterel language[END_REF], LUSTRE [START_REF] Halbwachs | The synchronous dataflow programming language Lustre[END_REF], SIGNAL [START_REF] Benveniste | Synchronous programming with events and relations: the Signal language and its semantics[END_REF], and QUARTZ [START_REF] Schneider | The synchronous programming language QUARTZ[END_REF], which can be considered as different implementations of the synchronous hypothesis. They adopt different programming styles, e.g., ESTEREL and QUARTZ have an imperative style suitable for control dominant applications while LUSTRE and SIGNAL respectively borrow functional and relational styles suitable for dataflow-oriented applications. Moreover, as a main difference from other synchronous languages, SIGNAL naturally considers a mathematical time model, in terms of a partial-order relation, to describe multiclocked systems without the necessity of a global clock. This feature permits the description of globally asynchronous locally synchronous systems (GALS) [START_REF] Teehan | A Survey and Taxonomy of GALS Design Styles[END_REF][START_REF] Benveniste | From synchrony to asynchrony[END_REF] conveniently.

The compilation process of synchronous languages is not limited to code generation: some analyses are first applied to determine if the specification is indeed executable. Let us mention the LUSTRE and ESTEREL causality analyses, the LUSTRE clock analyses and the ESTEREL constructive analysis. The SIGNAL compilation process contains two major analyses called clock calculus and data-dependency graph construction from which code generation directly follows. Moreover the clock calculus contains several steps, such as the synchronizations of each process, i.e., the generation of a set of equational constraints over clocks; the resolution of a system of clock equations; and the construction of a clock hierarchy on which the automatic code generation strongly relies.

In the SIGNAL compiler, the control flow expressed by abstract clocks serves to derive a control structure in automatic code generation. Thus, the quality of clock calculus has a strong impact on the correctness and efficiency of implementations. There are several optimizations of the clock calculus have been proposed to improve the quality of the code generated by the compiler, e.g., a code executed more efficiently or a code with smaller footprint. Optimizations aim at increasing the depth of the clock hierarchy in order to avoid useless tests in the generated code. They rely on discovering logical implications between boolean expressions, a conjunction being inserted as a descendent of one of its conjuncts. Several techniques have been considered: in the SIG-NAL compiler-Polychrony 1) rewriting techniques tempt to normalize boolean or arithmetic expressions (with the option command -crew), [START_REF] Feautrier | Enhancing the Compilation of Synchronous Dataflow Programs with a Combined Numerical-Boolean Abstraction[END_REF] uses an SMT solver, [START_REF] Gamatié | Towards Static Analysis of SIG-NAL Programs using Interval Techniques[END_REF] and [START_REF] Gamatié | An Interval-Based Solution for Static Analysis in the SIGNAL Language[END_REF] an interval-based data structure referred to as Interval-Decision Diagram (IDD).

In this paper, we propose an implementation of the main concepts of the SIGNAL compilation process which is encoded in the OCaml 2) language. In our compiler, called MinSIGNAL, we have considered existing enhancements such as [START_REF] Feautrier | Enhancing the Compilation of Synchronous Dataflow Programs with a Combined Numerical-Boolean Abstraction[END_REF], [START_REF] Gamatié | Towards Static Analysis of SIG-NAL Programs using Interval Techniques[END_REF], and [START_REF] Gamatié | An Interval-Based Solution for Static Analysis in the SIGNAL Language[END_REF]. The compiler follows a modular architecture, and can be seen as a sequence of source-tosource transformations applied to an intermediate representation which is named Synchronous Clocked Guarded Actions (S-CGA) and translation to sequential imperative code.

(1) Why a new intermediate representation Guarded commands [START_REF] Dijkstra | Guarded Commands, Nondeterminacy and Formal Derivation of Programs[END_REF], also called asynchronous guarded actions by J. Brandt et al. [START_REF] Brandt | Integrating system descriptions by clocked guarded actions[END_REF], are a well-established concept for the description of concurrent systems. In the spirit of the guarded commands, J. Brandt et al. propose 1) http://www.irisa.fr/espresso/Polychrony 2) http://ocaml.org/ synchronous guarded actions [START_REF] Brandt | Separate translation of synchronous programs to guarded actions[END_REF] as an intermediate representation for their QUARTZ compiler. As the name suggests, it follows the synchronous model. Hence, the behavior (control flow as well as data flow) is basically described by sets of guarded actions of the form γ ⇒ A . The boolean condition γ is called the guard and A is called the action. To support the integration of synchronous, polychronous and asynchronous models (such as CAOS [START_REF] Brandt | Translating concurrent action oriented specifications to synchronous guarded actions[END_REF] or SHIM [START_REF] Edwards | Foundation, and the Open Project of Shanghai Key Laboratory of Trustworthy Computing under Grant 07dz22304201502[END_REF]), they propose an extended intermediate representation, that is clocked 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] where one can declare explicitly a set of clocks. They also show how clocked guarded actions can be verified by symbolic model checking (SMV) and simulated by SystemC.

Compared with the existing SIGNAL compiler, we use clocked guarded actions as the intermediate representation, to integrate more synchronous languages such as QUARTZ, AIF 3) [START_REF] Brandt | Integrating system descriptions by clocked guarded actions[END_REF] into our compiler in the future. However, in contrast to the SIGNAL language, clocked guarded actions can evaluate a variable even if its clock does not hold. We mention also that the DC+ [START_REF]Esprit project: Safety Critical Embedded Systems SACRES. The declarative code DC+[END_REF] intermediate format has been proposed as an intermediate format for compiling multiclock synchronous languages (ESTEREL, LUSTRE and SIGNAL). However, DC+ is introduced as a layer on top of DC which is a monoclock intermediate language. DC+ is characterized by a rich kernel with a monoclock guarded assignment (named at) and the equivalent of SIGNAL when and default constructs. Thus, we propose a variant of Clocked Guarded Actions, namely S-CGA, which constrains variable accesses as done by SIGNAL and where guarded assignments are multiclocked. Compared to DC+, the SIGNAL when and default are not part of S-CGA. Actually, they are compiled. The code generation from SIGNAL programs is adapted to the S-CGA context. In [START_REF] Yang | A verified transformation: from polychronous programs to a variant of clocked guarded actions[END_REF][START_REF] Yang | Towards a verified compiler prototype for the synchronous language SIGNAL[END_REF], we have already defined the abstract syntax and the formal semantics of the S-CGA language.

(2) Why using OCaml in the tooling implementation For a safety-critical system, the development process always follows strict guidelines. The development quality assurance applies as much to the final source code, as to the tools themselves. For instance, in the civil avionics the DO-178B/C airworthiness certification standard [START_REF]B Software Considerations in Airborne Systems and Equipment Certification[END_REF][START_REF]C Software Considerations in Airborne Systems and Equipment Certification[END_REF] defines all the constraints ruling the aircraft software development. Moreover, one of the supplements to DO-178C, the DO-330 (Software Tool Qualification Considerations) provides a guidance to qualify tools. This means a tool, for example a compiler also needs to be qualified. For example, the SCADE 3) Averest Intermediate Format SUITE 4) 5) KCG automatic code generator has been qualified as a development tool at DO-178B level A.

The choice of a programming language close and adapted to the tooling development is very important since a wellsuited language leads to a simpler and safer way to encode the tooling requirements and consequently, a better and simpler traceability.

OCaml is a functional, imperative and object-oriented ML dialect. As a modern functional language, OCaml is adapted to symbolic computation and so, particularly suitable for compiler design and implementation of formal analysis tools. In particular, the safety of its type checking allows to skip some verification that would be mandatory with other languages, such as the memory allocation, coherency, initialization checks. The OCaml language has been used in Lucid Synchrone [START_REF] Pouzet | Lucid Synchrone, version 3. Tutorial and reference manual[END_REF] (the Lustre language for reactive systems implementation), the compiler implementation of Prelude [START_REF] Forget | A synchronous language for critical embedded systems with multiple real-time constraints[END_REF] (a synchronous language for critical embedded systems with multiple real-time constraints), and the Coq proof assistant [START_REF] Castéran | Interactive theorem proving and program development: Coq'Art: The Calculus of inductive constructions[END_REF] implementation. The first release of the SCADE KCG code generator was implemented in C and was available in 1999. Since 2005, Esterel Technologies has designed its new SCADE SUITE 6 T M in OCaml, which contains 65k lines of OCaml code [START_REF] Pagano | Using Objective Caml to Develop Safety-Critical Embedded Tools in a Certification Framework[END_REF]. As well, the abstract interpretation tool ASTREE [START_REF] Cousot | The ASTRÉE analyzer[END_REF] is also implemented in OCaml. The experiences of SCADE SUITE and of ASTREE by Airbus show that tools written in OCaml can be integrated in a critical software development process.

In this paper, the Ocaml implementation is a basis for the formal verification of the compilation of SIGNAL with a theorem prover such as Coq. Thus we restrict to the functional subset except for hash tables. Actually, the hash table can be replaced by the map structure in OCaml. Moreover, this work would be reused by ones interested in experimenting a new strategy for clock calculus and experimenting a new proof technique for the correctness of clock calculus (in a long term).

The rest of the paper is organized as follows. Section 2 gives an overview of the SIGNAL language. An analysis of the SIGNAL compilation process and the existing enhancements are given in Section 3. The MinSIGNAL is presented in Section 4. Section 5 discusses the related work, and Section 6 gives some concluding remarks and future work. 4) A successful commercial version of the synchronous language LUS-TRE 5) http://www.esterel-technologies.com/products/scade-suite/

An Introduction to SIGNAL

In this section, we first introduce the basic concepts of the SIGNAL language such as signals and abstract clocks, then we give a sketch of its primitive constructs and a few extended constructs. Finally, a formal semantics of the primitive constructs is introduced.

Basic concepts

Signals. As declared in the synchronous hypothesis, the behaviors of a reactive system are divided into a discrete sequence of instants. At each instant, the system does inputcomputation-output, which takes zero time. So, the inputs and outputs are sequences of values, each value of the sequence being present at some instants. Such a sequence is called a signal. Consequently, at each instant, a signal may be present or absent (denoted by ⊥). In SIGNAL, signals must be declared before being used, with an identifer (i.e., signal variable or the name of signal) and an associated type for their values such as integer, real, complex, boolean, event, string, etc.

Example 1 Three signals named input1, input2, output are shown as follows.

input1 1 ⊥ 3 ⊥ • • • input2 ⊥ 5 7 9 • • • output ⊥ ⊥ 10 ⊥ • • • Abstract Clock.
The set of instants where a signal takes a value is the abstract clock of the signal. Two signals are synchronous if they are always present and absent at the same instants, which means they have the same abstract clock.

In the example given above, the abstract clock of input1, input2 and output, denoted respectively input1, input2 and output, are defined by different sets of logical instants.

SIGNAL constructs

SIGNAL uses several constructs to express the relations between signals, including relations between values and relations between abstract clocks. Moreover, SIGNAL can specify the relations between the abstract clocks of signals in two ways: implicitly or explicitly.

Primitive Constructs. The primitive constructs can be classified into two families: monoclock operators (for which all signals involved have the same abstract clock) and multiclock operators (for which the signals involved may have different clocks).

• Monoclock operators, including instantaneous function and delay. The instantaneous function x := f (x 1 , • • • , x n ) applied on a set of inputs x 1 , • • • , x n will produce the output x, while the delay operator x :=

x 1 $ init c sends the previous value of the input to the output with an initial value c.

• Multiclock operators, including undersampling and deterministic merging. The undersampling operator x := x 1 when x 2 is used to get an input at the true occurrence of another input, while the deterministic merging operator x := x 1 de f ault x 2 is used to select between two inputs to be sent as the output, with a higher priority to the first input.

Notice that, these operators specify the relations between the abstract clocks of the signals in an implicit way.

In the SIGNAL language, the relations between values and the relations between abstract clocks of the signals, are defined as equations, and a process consists of a set of equations. Two basic operators apply to processes, the first one is the composition of different processes, and the other one is the local declaration in which the scope of a signal is restricted to a process.

Extended Constructs. SIGNAL also provides some operators to express control-related properties by specifying clock relations explicitly, such as clock synchronization, set operators on clocks (union, intersection, difference) and clock comparison.

• Clock synchronization, the equation

x 1 ˆ= x 2 ˆ= • • • ˆ=x n specifies that signals x 1 , x 2 , • • • , x n are synchronous.
• Set operators on clocks, such as the equation x:= x 1 ˆ+

x 2 defines the clock of x as the union of the clocks of signals x 1 and x 2 , the equation x:= x 1 ˆ* x 2 defines the clock of x as the intersection of the clocks of signals x 1 and x 2 , the equation x:= x 1 ˆx 2 defines the clock of x as the difference of the clocks of signals x 1 and x 2 .

• Clock comparison, such as the statement x 1 ˆ< x 2 specifies a set of inclusion relations between the clocks of signals x 1 and x 2 , the statement x 1 ˆ> x 2 specifies a set of containment relations between the clocks of signals

x 1 and x 2 , the statement x 1 ˆ♯ x 2 specifies that the intersection of the clocks of signals x 1 and x 2 is empty.

A Trace Denotational Semantics

There exist several semantics for SIGNAL, such as denotational semantics based on traces (called trace semantics) [START_REF] Besnard | SIGNAL V4 Reference Manual[END_REF][START_REF] Gamatié | Designing embedded systems with the Signal programming language: synchronous, reactive specification[END_REF][START_REF] Guernic | Data-Flow to von Neumann: the Signal approach[END_REF], denotational semantics based on tags (called tagged model semantics) [START_REF] Gamatié | Designing embedded systems with the Signal programming language: synchronous, reactive specification[END_REF][START_REF] Guernic | Polychrony for system design[END_REF], operational semantics presented in a structural style [START_REF] Benveniste | Synchronous programming with events and relations: the Signal language and its semantics[END_REF][START_REF] Gamatié | Designing embedded systems with the Signal programming language: synchronous, reactive specification[END_REF], operational semantics defined by synchronous transition systems (STS) [?]. [START_REF] Talpin | Constructive polychronous systems[END_REF][START_REF] Brandt | Embedding polychrony into synchrony[END_REF] define a unified constructive semantic framework to unite QUARTZ and SIGNAL. This framework allows us to better understand the relationship between synchrony and polychrony. Here, we introduce the trace semantics. Moreover, the semantics of each of the extended constructs being defined in terms of the primitive constructs, we just consider the primitive constructs, that is core-SIGNAL. In [START_REF] Yang | A comparative study of two formal semantics of the SIGNAL language[END_REF], we have given a proof of the semantics equivalence between the trace semantics and the tagged model semantics of the core-SIGNAL.

In the following paragraphs, we first summarize the semantics domain i.e. the trace model, then the trace semantics.

(1) Trace Model Let X be a set of signal variables, and let V be the set of values that can be taken by the variables. The symbol ⊥ (⊥ V) is introduced to express the absence of valuation of a variable. Then we denote: [START_REF] Gamatié | Designing embedded systems with the Signal programming language: synchronous, reactive specification[END_REF] A signal s is a sequence (s i ) i∈I of typed values (of V ⊥ ), where I is the set of natural integers N or an initial segment of N, including the empty segment.

V ⊥ = V ∪ {⊥} Definition 1 (Signal)
A signal can be finite. However, we can extend the finite signal with infinite absences, to get an infinite one.

The definition of traces is given in the following paragraphs. Notice that, a signal is just a sequence of values corresponding to a signal variable, while a trace defines the synchronized sequences of values of a set of signal variables.

Definition 2 (Event) [START_REF] Besnard | SIGNAL V4 Reference Manual[END_REF] Considering X a non-empty subset of X, we call event on X any application e : X → V ⊥ X • e(x) = ⊥ indicates that variable x has no value in the event.

• e(x) = v indicates, for v ∈ V x , that variable x takes the value v in the event.

The absent event on X (X → {⊥}), where all the signals are absent at a logical instant, is denoted ⊥ e (X). Moreover, the set of events on X

(X → V ⊥ X ) is denoted ε X .
A trace is a sequence of events. For any subset X of X, we consider the following definition of the set τ X of traces on X.

Definition 3 (Traces) τ X is the set of traces on X, defined as the set of applications N → ε X where N is the set of natural integers.

Similarly, a trace can be finite. However, we can extend the finite sequence with infinite absent events, to get an infinite trace.

Definition 4 (Sprocess) Given a SIGNAL process, its trace semantics, denoted as Sprocess, includes a set of signal variables defining the domain of the process and a set of traces.

(

2) Trace semantics

Based on the trace model, the trace semantics of SIGNAL is presented as follows. It defines the set of traces associated to each primitive construct of SIGNAL.

Trace Semantics 1 The trace semantics of the instantaneous function

x := f (x 1 , • • • , x n ) is defined as follows: ∀t ∈ N x t = ⊥ i f x 1t = . . . = x nt = ⊥ f (x 1t , . . . , x nt ) i f x 1t ⊥ ∧ . . . ∧ x nt ⊥
At each instant t, the signals are either all present or all absent, i.e., they are synchronous, denoted x ˆ= x 1 ˆ= • • • =

x n . x t gets the value of f (x 1t , . . . , x nt ) when the signals are all present. The function f includes different mathematical operations, such as arithmetic operations, boolean operations, etc.

Trace Semantics 2 The trace semantics of the delay construct x := x 1 $ init c is defined as follows:

-(∀t ∈ N) x 1t = ⊥ ⇔ x t = ⊥ -{k | x 1k ⊥} ∅ ⇒ x min{k|x 1k ⊥} = c -(∀t ∈ N) x 1t ⊥ ∧ {k > t | x 1k ⊥} ∅ ⇒ x min{k>t|x 1k ⊥} = x 1t
Here, min(X) denotes the minimum of a non-empty set of naturals. Similarly to the instantaneous function, the delay construct also requires signals x and x 1 have the same clock, denoted x ˆ= x 1 . Given a logical instant t, x takes the most recent value of x 1 except the one at t. Initially, x takes the value c.

Trace Semantics 3 The trace semantics of the undersampling construct x := x 1 when x 2 is defined as follows:

∀t ∈ N x t =
x 1t i f x 2t = true ⊥ otherwise Here, x and x 1 have the same type and x 2 is a boolean signal. The clock of x is the intersection of the clock of x 1 and the true occurrences of x 2 , denoted x=x 1 ˆ* [x 2 ], where [x 2 ] = x 2 ∧ x 2 represents the true occurrences of x 2 .

Trace Semantics 4 The trace semantics of the deterministic merging construct x := x 1 de f ault x 2 is defined as follows:

∀t ∈ N x t = x 1t i f x 1t ⊥ x 2t otherwise
Here, signals x, x 1 and x 2 have the same type. The clock of x is the union of the clocks of x 1 and x 2 , denoted x = x 1 ˆ+

x 2 . Given a logical instant t, x t gets the merge of the values of x 1t and x 2t , and the value of x 1t has a higher priority.

Finally the semantics of parallel composition is defined as the intersection of the semantics of the components. We apply these semantics rules to a SIGNAL process, to get a complete semantics of the process, that is SProcess (Definition 4).

Remark 1. The formal semantics is used in the programs transformations of the SIGNAL compiler, and it is also the basis of the validation of the compilation process.

An Analysis of the Main Concepts of the SIGNAL Compilation

In this section, we first present two formalizations, namely clock algebra and conditional data-dependency graph, which are used in the SIGNAL compilation process. Then, the main steps of the compilation are presented. Finally, we introduce the existing enhancements of the compilation process.

Formal models for SIGNAL program analysis

A SIGNAL program is a formal specification that is basically composed of equations describing relations of both values and clocks of the signals involved. The language allows one to mathematically reason on the properties of such a specification. One clock algebra associated to SIGNAL is the algebraic domain Z/3Z, the set of integers modulo 3 (i.e., Z/3Z = {-1, 0, 1}). Here 0 denotes a signal is absent, -1 means the signal is present and its value is false, and 1 means the signal is present and its value is true. As well, the reasoning approach for SIGNAL programs also includes dependency graphs to encode data dependencies.

(1) Clock algebra

In the SIGNAL context, relations over clocks are described using the clock algebra. The clock cl of a signal denotes a series of instants. The clock x of a signal x denotes the instants at which the signal x is present. The clock [x] (resp.

[¬x]) denotes the instants at which x is present and holds the value true (resp. false). A clock expression e is either the empty clock, noted 0, a signal clock cl, or the conjunction e1 ∧ e2, the disjunction e1 ∨ e2, the symmetric difference e1\e2 of two clock expressions e1 and e2. (

2) Conditional data-dependency graph

Intuitively, a data-dependency can be understood as the necessity that the value of some signal must be known in order to calculate the value of some other signal. A program is compiled into a graph that describes the data dependencies in the following sense: the edge a → cl b specifies that the computation of the node b, a signal or a clock, cannot be scheduled before that of the node a when the clock cl is present. A clock relation cl = e specifies that the signal clock cl is present iff the clock expression e is true.

a, b ::= x | x (node) R ::= cl = e | a → cl b (data dependency) Remark 2.
At the semantics level, we mainly consider the relations between clocks and the relations between values. However, at the compiler level, we also need to consider the data-dependencies, because they determine the execution sequences in the generated code.

The main steps of the SIGNAL compilation

After a transformation from the user program (whose statements are expressed with both primitive constructs and extended constructs) to the normalized program whose statements are all expressed with primitive constructs, the SIG-NAL compilation process contains two major analyses called clock calculus and data-dependency graph construction from which code generation directly follows. Moreover the clock calculus contains several steps, such as the synchronizations of each process, i.e., the generation of a set of equational constraints over clocks; the resolution of a system of clock equations; and the construction of a clock hierarchy on which the automatic code generation strongly relies.

(1) Synchronizations of SIGNAL processes Each primitive construct inherently defines a relation over the clocks involved. Consequently, a system composed out of multiple processes describes a system of these relations, which is, an equation system of clock variables that describe the synchronizations of the system. Based on the clock algebra presented in section 3.1, for each primitive construct, the clock synchronizations are given by Table 1. Moreover, the clock synchronizations can be described equivalently using SIGNAL extended constructs (e.g., xˆ= x 1 ˆ+ x 2 ).

P synchronizations o f P in clock algebra synchronizations o f P in S IGNAL x := f (x 1 , • • • , x n ) x = x1 = • • • = xn xˆ= x 1 | ... | xˆ= x n x := x 1 $ init c x = x1 xˆ= x 1 x := x 1 when x 2 x = x1 ∧ [x 2 ] xˆ= x 1 ˆ * when x 2 x := x 1 de f ault x 2 x = x1 ∨ x2 xˆ= x 1 ˆ+ x 2
(2) Solving the clock equation system

The SIGNAL philosophy strongly emphasizes that clocks indicate the control of data-flow specifications. Accordingly the control-flow of the target executable code is synthesized from relations over clocks, or synchronizations, that is, at any given instant, before the value of a signal x is computed, a test must be made on the presence/absence of x, namely the presence/absence of its clock x. So there is a need for a resolution method that will allow to efficiently check the presence of a clock. For that purpose, the clock equation system to be solved is extracted from the system by applying the rules of Table 1. The general approach for solving this equation system is given by triangularization [START_REF] Amagbegnon | Arborescent canonical form of boolean expressions[END_REF]:

The equational system is transformed into an ordered set of so called directed definitions, that is, a system of equations of the form h = h 1 op h 2 , where h is a newly defined clock, h 1 , h 2 are previously defined clocks and op ∈ {∧, ∨, \} is some operator on clocks. This representation ensures the absence of clock-to-clock cycles. Several problems should be solved to get this representation:

• Multiple definitions: If the equation system contains more than one equation with clock h on the left side, the equality of their respective right sides must be proven.

• Clock-to-clock cycles: If the equation system contains cyclic dependencies, they have to be eliminated.

• Complex relations: If equations are not of the form h = h 1 op h 2 , e.g., given by h 1 op h 2 = k 1 op k 2 , an attempt can be made to prove the equivalence of the formulas with rewriting techniques.

The SIGNAL compilation process involves solving these problems, mainly by using a rewriting system plus some heuristics, in order to achieve triangular form. But since these problems are complex, the compiler is not complete: If no appropriate rewriting rule can be applied, an input program may be rejected although the system could be solved. In any case, if some equalities cannot be proven or if some cycle cannot be eliminated, an input program is considered temporally incorrect and rejected.

(

3) Hierarchical representation of clock equations

Efficient code generation requires a "good" representation of the solutions of the clock equations which result from the previous step. In order to efficiently apply rewriting and keep track of the triangularity (i.e., triangularization preservation) of the equation systems, a tree-based representation of the equations is used, named the clock hierarchy. Moreover, the paper [START_REF] Benveniste | From synchrony to asynchrony[END_REF] discusses the link between perfect synchrony and asynchrony, and shows that the endochrony property of a clock hierarchy is a sufficient condition to get executable and deterministic code from a given clock hierarchy.

The synthesis of clock hierarchy in SIGNAL programs relies on an efficient algorithm [START_REF] Amagbegnon | Arborescent canonical form of boolean expressions[END_REF] that has been implemented in the compiler. We summarize it as follows:

• For a Boolean signal x, the known partition [x] ⊆ x ⊇

[¬x] is represented by a basic partition tree, whose edges are the set inclusion relations.

• The representation of the whole equation system of synchronizations starts with representing all directed definitions by a forest of clock trees.

• Then, two clock trees are iteratively fusioned by inserting one tree into another: Let T, T' be two clock trees with roots r and h respectively, where h is defined by the directed equation h = h 1 op h 2 , and h 1 and h 2 are subtrees of T. Then the fusion of T' into T is applied by adding the tree T' to the immediate children of the least common ancestor of h 1 and h 2 in T. This way, the subtree T', which is defined by the operands h 1 and h 2 , is placed directly under the least common ancestor of these operands. This preserves the structural property of triangularization and gives credit to clock inclusion relations which yield more efficient nested if-tests.

Intuitively, the clock of a node is a subset of the clock of its parent. The algorithm repeatedly tries to rewrite the equations so that they match the criteria of the fusion step and then executes the fusion until this cannot be done anymore.

As shown in the report [START_REF] Amagbegnon | Arborescent canonical form of boolean expressions[END_REF], we can do optimizations on the clock hierarchy to improve the quality of the code gen-erated by the compiler, e.g., a code executed more efficiently or a code with smaller footprint. For instance, the resulting tree-based representation of the equation systems over clocks can be optimized in the sense that the insertion step during the fusion chooses a parent with greatest depth.

(4) Code generation

The code generation is based on the transformations presented in the previous sections. It is strongly guided by the clock hierarchy resulting from the clock calculus to structure the target language program, and by the conditional datadependency graph not only to locally order elementary operations in sequences, but also to schedule component activations in a hierarchical target code. This code can be obtained in different target languages, among which the most used are C, C++, and Java.

When a SIGNAL program P is proved to be endochronous, the generation of its associated code is straightforward. Each node of the clock tree corresponding to P is characterized by a Boolean expression that expresses a condition (if-thenelse structures). The statements that depend on each node are computed whenever the associated condition is evaluated to be true, meaning that the expressed clock is present. On the other hand, the code generation takes into account the conditional dependency graph that characterizes the order according to which statements are to be computed at the same clock instants.

Furthermore, the code generated especially the nesting of if-then-else structures can be optimized, if h and k are two clocks such that h ⊆ k, then for an instant t, the following clock implication holds:

t k =⇒ t h
In others words, if the test t ∈ k fails, there is no need to test if t ∈ h. Thus, code generation can take advantage of the clock inclusion relation between clocks.

As an example, the code

i f present(k) then do -action -k i f present(h) then do -action -h endi f endi f is more efficient than the code i f present(k) then do -action -k endi f i f present(h) then do -action -h endi f

Handling Numerical Expressions

For the under-sampling construct, remember that the clock of the Boolean expression x is partitioned into [x] and [¬x], which are referred to as condition-clocks. In the SIGNAL compiler, if x is defined by a numerical expression such as an integer comparison, [x] and [¬x] are seen as black boxes by default. As a consequence the relation in the numerical expression is unknown and useless comparisons are generated.

Here, we use an example to explain the handling of numerical expressions. has not been detected. If [c1 and c2] had been placed as a son of one of [c1] or [c2] while preserving "arborescent canonical form", the test of the conjunction would have been performed only when one of the argument is true. However, as mentioned in section 3.2, such optimizations could be performed by the C compiler itself.

C_z1 = a > 0 ; C_z2 = a <= 0 ; C_z3 = b > 0 ; C_s2 = c1 && c2 ; C_CLK_52 = C_z1 | | C_z2 ; C_m = C_CLK_52 | | C_z3 ; i f ( c1 ) { s 1 = x1 ; w_exp1_s1 ( s 1 ) ; } i f ( C_z1 ) { z1 = x ; w_exp1_z1 ( z1 ) ; } i f ( C_z2 ) { z2 = x ; w_exp1_z2 ( z2 ) ; } i f ( C_z3 ) { z3 = y ; w_exp1_z3 ( z3 ) ; } i f ( C_s2 ) { s 2 = x1 ; w_exp1_s2 ( s 2 ) ; } i f (C_m) { i f ( C_z1 ) m = z1 ; e l s e i f ( C_z2 ) m = z2 ;
e l s e m = z3 ; w_exp1_m (m ) ; }

• Compilation with the option -crew Even if the SIGNAL compiler does not fully handle numerical expressions, it is possible to let it do some rewriting of numerical conditions as Boolean expressions by using the option -crew. A part of code generated for the Example 2 is given as follows. With this option, comparisons are rewritten using only the operators == (for example CLK_81 = 0 == a) and <= (for example CLK_83 = 0 <= a). Thus, [a > 0] and [a <= 0] can be rewritten as C_z1 =!CLK_81&&CLK_83 and C_z2 = CLK_81||!CLK_83 respectively. As we can see, the rewriting of comparisons permits a more precise analysis on clocks.

CLK_81 = 0 == a ; CLK_83 = 0 <= a ; C_z1 = ! CLK_81 && CLK_83 ; C_z2 = CLK_81 | | ! CLK_83 ; C_z3 = ( 0 <= b ) && ! ( 0 == b ) ; C_s2 = c1 && c2 ;
• Enhancement with a combined numerical-Boolean abstraction Paul Feautrier et al [START_REF] Feautrier | Enhancing the Compilation of Synchronous Dataflow Programs with a Combined Numerical-Boolean Abstraction[END_REF] propose a combined numerical-Boolean abstraction to deal with these problems. In the new abstraction, every signal in a program is associated with a pair of the form (clock, value), where clock is a Boolean function and value is a Boolean or numeric function. They also use a SMT solver to reason on the new abstraction, and get more precise clock analysis because they treat the numerical expression as white boxes.

Inside the MinSIGNAL Compiler

In this section, we present the OCaml code of the compilation process of MinSIGNAL. First, the modular architecture of MinSIGNAL is given in a global view. Second, the compilation progress is presented step by step.

A Modular Architecture

As shown in Figure 1, the MinSIGNAL compiler has a modular architecture, and can be seen as a sequence of source-tosource transformations applied to the intermediate representation S-CGA and then translation to sequential imperative code. Specifically, the compilation process is mainly structured as five modules. At each module, there are several submodules.

• Module 1: Normalization of the user program. Beyond the usual lexical analysis, parsing and type checking, the compiler will transform the user program (using the subset of SIGNAL) whose statements are expressed with both primitive constructs and extended constructs to the normalized program whose statements are all expressed with primitive constructs.

• Module 2: Synchronizations of SIGNAL processes. As a difference with the existing SIGNAL compiler, we construct S-CGA from the normalized program. S-CGA contains control flow (the relations between clocks) as well as data flow (the relations between values).

• Module 3: Solving the clock equation system. If the system of clock equations contains more than one equation with the same clock, the execution of the generated code will check the same control condition several times, and it is inefficient. This is why we need to resolve it. We can use BDD or SMT technology to check the equivalence of two clock equations, and put the corresponding clock variables into the same equivalence class. We also check the endochrony property at this step, namely there is just one master clock.

• Module 4: Hierarchical representation of clock equations. The code generation is based on both the clock hierarchy and the data dependencies. However, there may be clock-to-data cycles. To reduce these cycles, we first sort all the guarded actions. It will be easier to construct a clock hierarchy based on deterministic sorting, and we consider the sorting as a depth first search (DFS) order.

• Module 5: Code generation and optimization. The basic idea of code generation is the same as in the SIGNAL compiler. Furthermore, we do some optimizations at the code level. Given two equations such as y = x when x 1 and z = x when (x 1 and x 2 ), there is a clock-inclusion relation: [

x 1 ∧ x 2 ] → [x 1 ], i.e., the clock of [x 1 ∧ x 2 ] is a subset of the clock of [x 1 ]
. Consequently, we can do the code optimization illustrated as follows. If control condition x 1 holds, we do not need to check x 1 again in x 1 &&x 2 . We just need to check if x 2 holds or not.

.} }

As mentioned before, the safety of the type checking of OCaml allows to skip some verification that would be mandatory with other languages. Moreover, the OCaml code is compact which allows less verification efforts. MinSIGNAL consists in about 3000 lines of OCaml code (Table 2).

Normalization of the user program

As shown in section 2.2, the definition of the extended constructs is derived from a combination of the primitive constructs to provide the user with suitable macros. So, beyond the usual lexical analysis, parsing and type checking, the compiler will transform the user program whose statements are expressed with both primitive constructs and extended constructs to the normalized program whose statements are all expressed with primitive constructs.

(1) Lexical analysis, parsing and type checking

The lexical analysis and parsing of MinSIGNAL are implemented with standard tools, OCamlLex and OCamlYacc. As usual, they translate a string of characters to a sequence of tokens and then to an abstract syntax tree, which is necessary for any complex program manipulation. We don't give the details of the lexical analysis, parsing and type checking, because of the space limitations.

Here, we give a simplified abstract syntax which is defined in OCaml. ty represents the data types of SIGNAL such as integer, real, complex, boolean, etc. A SIGNAL specification spec is a set of processes. A process proc is a set of equations (eqn list) for signals specifying relations between values, on the one hand, and clocks, on the other hand, of the signals involved. Moreover, a process also includes its name, input signals, output signals and local declarations. An equation can denote the relations between values or the relations between clocks, Ident represents the identifier of a signal, CInt, CReal, CBool, CString, and CChar represents constants defined in the equations, Func, Delay, When, and Default denote the primitive constructs, set operators on clocks such as ˆ+, ˆ* and ˆ-are also represented in Func, while clock comparison operators such as ˆ<, ˆ>, ˆ♯ and ˆ= are represented in Constraint. We first give the kernel syntax (corresponding to the core-SIGNAL) which is defined in OCaml. The abstract syntax of core-SIGNAL, of clock equation (in section 4.4), and of reduced normal form (i.e., equivalence class in section 4.5) have a common style, thus we use a type kind with three values Ksignal, Clock, and Class. In the user syntax, the expression can be iterated, while in the kernel syntax, the expression has been flattened. Transformation 2. The set operations on abstract clocks such as clock intersection, union, and difference, can be expressed by the following constructs, and then can be expressed using primitive constructs.

Set operations on clocks Corresponding constructs

x := x 1 ˆ* x 2 x := x1 when x2 x := x 1 ˆ+ x 2

x := x1 de f ault x2

x := x 1 ˆ-x 2 x := when ((not x2 ) de f ault x1 )
Notice that x := when ((not x2 ) de f ault x1 ) can be rewritten as x := ((not x2 ) de f ault x1 ) when ((not x2 )

de f ault x1 )
Transformation 3. The comparison operations of abstract clocks can be expressed using set operations on clocks, and then can be expressed using primitive constructs. Here, 0 specifies the empty clock.

Clock comparison operations Set operations on clocks

x 1 ˆ< x 2 x 1 ˆ= x 1 ˆ* x 2 x 1 ˆ> x 2 x 1 ˆ= x 1 ˆ+ x 2 x 1 ˆ♯ x 2 0 ˆ= x 1 ˆ* x 2 x 1 ˆ= x 2 clk := x1 = x2 where clk
Dealing with constant signals. In addition, we'd like to see the clock equation system defined in clock algebra directly. There is a little problem about the presence of constant signals. For example, given a process with two equations of signals,

y = 2 when b y ′ = 2 when b ′
we have the clock relations as follows,

ŷ = 2 ∧ [b] ŷ′ = 2 ∧ [b ′ ]
However, the clock 2 in ŷ = 2 ∧ [b] and in ŷ′ = 2 ∧ [b ′ ] may be not the same. Namely, the presence of constant signals depend on their usage context. To avoid conflicts, we use a new signal variable (defined in the local declaration) to replace the constant signal, and the new signal variable will be defined using a delay construct, for example x 1 = x 1 $ init 2 and x 2 = x 2 $ init 2. Then, the process will be transformed as, y = x 1 when b,

y ′ = x 2 when b ′ x 1 = x 1 $ init 2 x 2 = x 2 $ init 2
Finally, we get the clock relations as follows,

ŷ = x1 ∧ [b] ŷ′ = x2 ∧ [b ′ ]
Notice that, we compute the data-type of each new signal variable by type inference.

Based on the kernel syntax and previous transformation rules, the user program will be transformed into the normalized program and then will be flattened.

The comparison operations of abstract clocks are transformed into the set operations on clocks. Its OCaml code is given as follows.

l e t r e c e l i m _ c t r s _ i n _ e q n s e q n s = L i s t . c o n c a t ( L i s t . map ( f u n c t i o n | Ass ( s , e ) a s eq -> [ eq ] | C o n s t r a i n t ( s , e1 , e2 ) -> b e g i n match s w i t h | " ^< "-> [ C o n s t r a i n t ( " ^= " , e1 , Func ( " ^ * " , [ e1 ; e2 ] ) ) ] | " ^> "-> [ C o n s t r a i n t ( " ^= " , e1 , Func ( " ^+ " , [ e1 ; e2 ] ) ) ] | " ^# "-> [ C o n s t r a i n t ( " ^= " , Func ( " ^" , [ C I n t ( 0 ) ] ) , Func ( " ^ * " , [ e1 ; e2 ] ) ) ] | " ^= "-> l e t c1=new_var "C" ( T B a s i c " e v e n t " ) and c2=new_var "C" ( T B a s i c " e v e n t " ) and c3=new_var "C" ( T B a s i c " e v e n t " ) i n i f i s I d e n t o r C o n s t ( e2 ) t h e n [ Ass ( c1 , Func ( "==" , [ e1 ; e1 ] ) ) ; Ass ( c2 , Func ( "==" , [ e2 ; e2 ] ) ) ; Ass ( c3 , Func ( "==" , [ I d e n t c1 ; I d e n t c2 ] ) ) ] e l s e l e t c4=new_var "C" ( T B a s i c " e v e n t " ) i n [ Ass ( c1 , Func ( "=" , [ e1 ; e1 ] ) ) ; Ass ( c2 , e2 ) ; Ass ( c3 , Func ( "=" , [ I d e n t c2 ; I d e n t c2 ] ) ) ; Ass ( c4 , Func ( "=" , [ I d e n t c1 ; I d e n t c3 ] ) ) ] | _-> f a i l w i t h ( " NYI : unknown c o n s t r a i n t " ) end ) e q n s )

For the set operations on abstract clocks, they are firstly transformed into corresponding constructs, which are implemented by the constructors Func("ˆ+",[e1;e2]), Func("ˆ*",[e1;e2]) and Func("ˆ-",[e1;e2]) in the recursive function flatten. Then, all the clocks such as x will be expressed using primitive constructs, that is the constructor Func("ˆ",[e]). Finally, all the primitive constructs transformed will be flattened. l e t r e c f l a t t e n = f u n c t i o n | Func ( " ^+ " , [ e1 ; e2 ] ) -> f l a t t e n ( D e f a u l t ( Func ( " ^" , [ e1 ] ) , Func ( " ^" , [ e2 ] ) ) ) | Func ( " ^ * " , [ e1 ; e2 ] ) -> f l a t t e n ( When ( Func ( " ^" , [ e1 ] ) , Func ( " ^" , [ e2 ] ) ) ) | Func ( " ^-" , [ e1 ; e2 ] ) -> l e t e3 = D e f a u l t ( Func ( " n o t " , [ Func ( " ^" , [ e2 ] ) ] ) , Func ( " ^" , [ e1 ] ) ) i n f l a t t e n ( When ( e3 , e3 ) ) | Func ( " ^" , [ e ] ) -> l e t v1=new_var "CL" ( T B a s i c " e v e n t " ) i n l e t e1= f l a t t e n e i n a d d _ e q n ( Ass ( v1 , Func ( " := " , [ e1 ; e1 ] ) ) ) ; I d e n t v1 | Func ( f , l ) a s e -> l e t v1=new_var " F " ( T B a s i c ( g e t _ t y p e e ) ) i n a d d _ e q n ( Ass ( v1 , Func ( f , L i s t . map f l a t t e n l ) ) ) ; I d e n t v1 | D e l a y ( e1 , e2 ) a s e -> l e t v2=new_var "D" ( T B a s i c ( g e t _ t y p e e ) ) i n a d d _ e q n ( Ass ( v2 , D e l a y ( f l a t t e n e1 , e2 ) ) ) ; I d e n t v2 | D e f a u l t ( e1 , e2 ) a s e -> l e t v3=new_var "M" ( T B a s i c ( g e t _ t y p e e ) ) i n a d d _ e q n ( Ass ( v3 , D e f a u l t ( f l a t t e n e1 , f l a t t e n e2 ) ) ) ; I d e n t v3 | When ( e1 , e2 ) a s e -> l e t v4=new_var "W" ( T B a s i c ( g e t _ t y p e e ) ) i n a d d _ e q n ( Ass ( v4 , When ( f l a t t e n e1 , f l a t t e n e2 ) ) ) ; I d e n t v4 | I d e n t _ a s e -> e | e ( * t h i s i s c o n s t a n t * ) -> l e t k=new_var "K" ( T B a s i c ( g e t _ t y p e e ) ) i n a d d _ e q n ( Ass ( k , D e l a y ( I d e n t k , e ) ) ) ; I d e n t k

S-CGA Intermediate representation

In papers such as [START_REF] Brandt | Representation of synchronous, asynchronous, and polychronous components by clocked guarded actions[END_REF], clocked guarded actions have been defined as a common representation for synchronous (via synchronous guarded actions), polychronous and asynchronous (via asynchronous guarded actions) models. It has a multiclocked feature. However, in contrast to the SIGNAL language, clocked guarded actions can evaluate a variable even if its clock does not hold [18] [20]. In this case the read value is the most recently written value, while in SIGNAL read and writes can be simultaneous provided the causality is respected. As a consequence, we have introduced an intermediate representation S-CGA [START_REF] Yang | A verified transformation: from polychronous programs to a variant of clocked guarded actions[END_REF][START_REF] Yang | Towards a verified compiler prototype for the synchronous language SIGNAL[END_REF], which is a variant of clocked guarded actions. In one hand, S-CGA expresses the relations between signals, including the relations between abstract clocks and the relations between values, which are con-sistent with the SIGNAL program. In the other hand, as an intermediate representation, S-CGA permits us to integrate more synchronous languages such as QUARTZ, AIF into our compiler in the future.

(1) The definition of S-CGA S-CGA has the same structure as clocked guarded actions, but has different semantics.

Definition 6 (S-CGA) An S-CGA system is represented by a set of guarded actions of the form γ ⇒ A defined over a set of variables X. The Boolean condition γ is called the guard and A is called the action. Guarded actions can be of the following forms:

(1) γ ⇒ x = τ (immediate) (2) γ ⇒ next(x) = τ (delayed) (3) γ ⇒ assume(σ) (assumption)
where

• the guard γ is a Boolean condition over the variables of X, and their respective clocks. For a variable x ∈ X, we denote:

its clock x, -its initial clock init( x) as the clock which ticks the first time (if any) where x ticks.

• τ is an expression over X,

• σ is a Boolean expression over the variables of X and their clocks.

An immediate assignment x = τ writes the value of τ immediately to the variable x. The form (1) implicitly imposes that if γ is defined 6) and its value is true, then x is present and τ is defined.

A delayed assignment next(x) = τ evaluates τ in the given instant but changes the value of the variable x at next time clock x ticks.

The form (3) defines a constraint. It determines a Boolean condition which has to hold when γ is defined and true. All the execution traces must satisfy this constraint. Otherwise, they are ignored.

Guarded actions are composed by using the parallel operator .

A SIGNAL process includes its name, input signals, output signals, local declarations, and equations which denote the relations between clocks or the relations between values. In the OCaml code, we consider also inputs and outputs as guarded actions in S-CGA. The immediate guarded action is split into init( x) ⇒ x = τ and γ ⇒ x = τ where init( x) is not 6) An expression is said to be defined if all the variables it contains are present.

in the guard γ. The assumption guard action is also defined in the type action. We use another hash table ddes to deal with the delay guarded action.

The corresponding OCaml code is given as follows.

( ( * i n i t p a r t o f i m m e d i a t e g u a r d e d a c t i o n s * ) l e t d c e s = H a s h t b l . c r e a t e 1000 l e t h a s h 2 s t r 1 t l s = H a s h t b l . f o l d ( fun k v r -> r ^" \ n " ^" i n i t ( " ^s e x p 2 s t r k ^" ) " ^"=>" ^k e q n 2 s t r v ) t l s " " ( * d e l a y g u a r d e d a c t i o n s * ) l e t d d e s= H a s h t b l . c r e a t e 1000 l e t r e c v 2 s t r = f u n c t i o n | KAss ( ( sv , k ) , e ) -> " n e x t ( " ^s v ^" ) " ^"=" ^( s e x p 2 s t r e ) | _ -> f a i l w i t h " v 2 s t r " l e t h a s h 2 s t r 2 t l s = H a s h t b l . f o l d ( fun k v r -> r ^" \ n " ^s e x p 2 s t r k ^"=>" ^v 2 s t r v ) t l s " "

(2) From normalized program to S-CGA Clock synchronization constraints are given in Table 3. Except for the under-sampling construct, we also enhance the clock synchronization of the deterministic-merging construct. The construct x := x 1 de f ault x 2 will be split as two assignments: x = x 1 corresponding to the clock x 1 and x = x 2 corresponding to the clock de f ___x 2 = x 2 \ x 1 . Namely, a new clock variable de f ___x 2 is added. This enhancement will be useful in the construction of the clock hierarchy to avoid clock-to-data cycles (section 4.5).

:= f (x 1 , • • • , x n ) x = x 1 = • • • = x n x := x 1 $ init c x = x 1 x := x 1 when x 2 x = x 1 ∧ t___x 2 t___x 2 = x 2 ∧ x 2 x := x 1 de f ault x 2 x = x 1 ∨ x 2 de f ___x 2 = x 2 \ x 1
S-CGA expresses the relations between signals, including the relations between clocks and the relations between values, which are consistent with the SIGNAL program. Thus, in the OCaml code, the normalized program is transformed into S-CGA by using two functions: trans_eqns_clkeqv and attachEquation.

The function trans_eqns_clkeqv is used to construct the clock equations from S-CGA. KAss((s, k),ex) considers the three cases in the instantaneous function

x := f (x 1 , • • • , x n ).
The constructor KAssSig(s,es) deals with the primitive constructs delay, undersampling and deterministic merging.

Here, all the primitive constructs have been flattened. l e t t r a n s _ e q n s _ c l k e q e q s = u n i q ( L i s t . c o n c a t ( L i s t . map (

f u n c t i o n | KAss ( ( s , k ) , ex ) -> b e g i n match ex w i t h SVar ( s1 , K s i g n a l ) -> [ Dass ( SVar ( " t r u e " , K s i g n a l ) , ( s , C l o c k ) , SVar ( s1 , C l o c k ) ) ] | SFunc ( f , [ ( s1 , k ) ] ) -> [ Dass ( SVar ( " t r u e " , K s i g n a l ) , ( s , C l o c k ) , SVar ( s1 , C l o c k ) ) ] | SFunc ( f , [ ( s1 , k1 ) ; ( s2 , k2 ) ] ) ->
[ Dass ( SVar ( " t r u e " , K s i g n a l ) , ( ) ) ; Dass ( SVar ( " t r u e " , K s i g n a l ) , ( "

d e f _ _ _ " ^s2 , C l o c k ) , SFunc ( " d i f f " , [ ( s2 , C l o c k ) ; ( s1 , C l o c k ) ] ) ) ] end ) e q s ) )
Moreover, the function attachEquation is used to construct the relation between values from S-CGA. l e t a t t a c h E q u a t i o n e q n s= L i s t . ( KAss ( ( s , K s i g n a l ) , SVar ( s1 , K s i g n a l ) ) ) ( * ^y=> n e x t ( y )= x * ) | K D e f a u l t ( se1 , s e 2 ) -> H a s h t b l . add c l s e q ( SVar ( se1 , C l o c k ) ) ( KAss ( ( s , K s i g n a l ) , SVar ( se1 , K s i g n a l ) ) ) ; H a s h t b l . add c l s e q ( SVar ( " d e f _ _ _ " ^se2 , C l o c k ) )

( KAss ( ( s , K s i g n a l ) , SVar ( se2 , K s i g n a l ) ) ) | KWhen ( se1 , s e 2 ) -> H a s h t b l . add c l s e q ( SVar ( s , C l o c k ) ) ( KAss ( ( s , K s i g n a l ) , SVar ( se1 , K s i g n a l ) ) ) end | KAss ( ( s , k ) , ex ) a s e -> H a s h t b l . add c l s e q ( SVar ( s , C l o c k ) ) e ; ) e q n s ; c l s e q 4.4 Solving the clock equation system We first introduce the resolution algorithm, then we present how to compute clock equivalence classes to avoid multiple definitions of a clock, and finally get a reduced clock equation system (namely reduced normal form) based on the clock equivalence classes.

(1) Transformation to normal form

The clock equation system extracted from the S-CGA program will be solved as a system of equations of the form h = h 1 op h 2 (which is also called normal form), to efficiently check the presence of a clock. That's why, for example, if the equation system contains more than one equation with the same clock on the left side, the execution of the generated code will check the same control condition several times, which is inefficient. As shown in section 3.2, there are also other problems that need to be dealt with, such as clock-to-clock cycles and complex relations.

Given two sets NFS and UNFS, NFS is a set of normalized clock equations, and UNFS is a set of unnormalized ones for example complex relations. In NFS, each clock equation is uniquely defined to avoid multiple definitions, and the clock variable in the left-hand side (LHS) cannot be in the righthand side (RHS) to avoid clock-to-clock cycles.

Algorithm 1: Resolution of the clock equation system.

• Step 1: given any equation eq of the clock equation system, replace the clock variables in both sides of eq with the corresponding definition which has been defined in NFS (if it has been defined), and we get the new equation eq'.

•

Step 2: if the LHS of eq' is a clock expression and its RHS is a clock variable, then we reverse eq'.

•

Step 3: if the LHS of eq' is a clock variable, and it exists in the RHS, then Step 5, else Step 6.

• Step 4: if both LHS and RHS of eq' are clock expressions, namely a complex relation, then Step 5.

• Step 5: put eq' into UNFS, then Step 8.

• Step 6: put eq' into NFS, then Step 7.

• Step 7: for each equation ceq in UNFS, replace the clock variables of both sides of ceq with eq', and we get a new equation ceq', if the LHS and the RHS of ceq' are equivalent, then we eliminate it from UNFS, else we add it into UNFS.

• Step 8: repeating Step 1 -Step 7 until there is no equation in the clock equations system.

• Step 9: if UNFS is empty, then return NFS, else return a refuse information.

The corresponding OCaml expression is given as follows. Here, we have two lists UNFS and NFS. When we add a new equation to the list NFS, we need to replace other equations in NFS using the new one. l e t c l e q s 2 n f a c t i o n l i s t = l e t c l e q s l i s t = a c t i o n 2 c l e q s l i s t a c t i o n l i s t i n l e t n f e q n l i s t = s e q n 2 n f e q n l i s t c l e q s l i s t i n l e t ( u n f s , n f s )= L i s t . In the SIGNAL compiler, the clock analysis mainly relies on a Boolean abstraction of programs, internally represented as BDDs or SMTs for an efficient reasoning. In the Step 7, we reuse BDD technology to check the equivalence between LHS and RHS of a complex relation in UNFS.

(2) Computing clock equivalence class As mentioned above, each clock equation is uniquely defined in NFS to avoid multiple definitions. Here all the clock equations are considered as boolean equations, so we reuse the BDD technology to check the equivalence of boolean equations, and put the corresponding clock variables into the same equivalence class.

The OCaml expression is given as follows. Every boolean equation has a unique BDD representation (exp2bdd), which corresponds to an equivalence class. Moreover, we use a hash table (esmap) to save the corresponding relations between equivalence class and the clock variables it contains. e q _ c l a s s _ e x p c e 1 ; e q _ c l a s s _ e x p c e 2 | _ -> f a i l w i t h " e q _ c l a s s _ e x p " l e t c p t _ e q _ c l a s s c l e q s l i s t = L i s t . i t e r ( f u n c t i o n NFAss ( c l , c l e x p ) -> l e t i d = C l o c k e q 2 n f . e x p 2 q u o t i e n t c l e x p i n H a s h t b l . r e p l a c e esmap c l i d ; e q _ c l a s s _ e x p c l e x p ; )

(3) Getting reduced normal form

To further efficiently check the presence of a clock, we use the identity of the equivalence class to replace the clock variables in the normal form, and we just preserve one equation for one identity. This form is called reduced normal form. Here, we give the abstract syntax of the reduced normal form in OCaml. The construction of clock hierarchy is based on the reduced normal form, that is each node of the clock hierarchy is an identity of a clock equivalence class. As well, we associate the actions, such as inputs, outputs and value assignments, to each clock equivalence class.

Compared with other constructs, the delay construct is a dynamic operator since the properties induced on the signals refer to different values of time indexes, so we can't associate its actions statically to the clock equivalence class (it will be dealt with in the step of code generation). As shown in section 4.3, the construct x := x 1 de f ault x 2 will be split as two assignments: x = x 1 and x = x 2 . The construct x := x 1 when x 2 is translated into a unique assignment x = x 1 in the equivalence class of x.

The OCaml expression is given as follows. ) e q n s ; c l s e q l e t p l _ a t t a c h e q p l = L i s t . map ( f u n c t i o n S P r o c ( n , i s , os , eqns , ws ) -> i n p u t : = ! i n p u t @ i s ; o u t p u t : = ! o u t p u t @ o s ; l e t c l s = a t t a c h E q u a t i o n e q n s i n c l s ) p l

(2) Deterministic sorting

The code generation is based on both the clock hierarchy and the conditional data dependencies. However, there may be clock-to-data cycles when we combine the two intermediate representations. To cut the cycles, we first sort the clock relations defined by the reduced normal form and the data dependencies represented by the actions (such as inputs, outputs, and value assignments) which have been associated to the clock equivalence classes, then we can get a total order for the clock hierarchy because of the endochrony property.

The OCaml expression is given as follows. We use three values -1, 0, 1 to express the order between two equations for example eq 1 and eq 2 , if eq 1 is executed before eq 2 , then it returns -1, if eq 1 is executed after eq 2 , then it returns 1, else it returns 0. The sorting principle is defined as, for example, if the LHS of eq 1 exists in the RHS of eq 2 , then eq 1 is executed after eq 2 , if the LHS of eq 2 exists in the RHS of eq 1 , then eq 1 is executed before eq 2 . (3) Construction of a clock hierarchy It will be easier to construct a clock hierarchy based on the deterministic sorting. Here we consider the sorting as a depth first search (DFS) order. However, the resulting treebased representation of the equation systems over clocks can be optimized in the sense that the insertion step during the fusion chooses a parent with greatest depth, i.e., insertion as deep as possible.

As shown in Fig. 2, according to the algorithm [START_REF] Amagbegnon | Arborescent canonical form of boolean expressions[END_REF] that has been implemented in the compiler, C5 will be inserted at the right side of C4, C2, C4 and C5 have the same parent node C. If there exists clock inclusion C5 ⇒ C4, we can insert C5 as a son node of C4 and at the right side of C42. As shown in section 4.3, we have considered the conditionclocks ([x], [¬x]) as white boxes, so here we can get more precise clock inclusion relations. Moreover, when we insert C5, all the actions which are executed before C5 have been inserted into the hierarchy, so there is a limit branch of which we can just insert the new node into the right side. To insert as deep as possible, we can check the clock inclusion relations between C5 and all the nodes which are executed after this limit branch. We give the basic algorithm as follows.

Algorithm 2: Construction of a clock hierarchy.

• Step 1: get an element from the sorted list.

• Step 2: if the current element is an equation from reduced normal form, namely it is the relation between clock equivalence classes, we find its limit branch on the hierarchy, and find a good insertion place based on clock inclusions, then create a new node for the equivalence class of the LHS of the equation.

•

Step 3: if the current element is an action such as an input, an output, or a value assignment, we find the corresponding equivalence class which has been inserted in the hierarchy, and insert this action to the action list of the corresponding equivalence class (here we don't need to sort the action list, because they have been sorted in the sorting list).

• Step 4: Repeating Step 1-Step 3, until there is no element in the sorting list.

Code generation and optimization

Here, the basic idea of code generation (Fig. 3) is as in the SIGNAL compiler: it is strongly guided by the clock hierarchy resulting from the clock calculus to structure the target language program, and by the data dependencies not only to locally order elementary operations in sequences, but also to schedule component activations in a hierarchical target code. However, all the actions have been added in the clock hierarchy, so the code generation become simpler. Moreover, the generated code can be more optimized because of previous enhancements. Furthermore, we can also do some optimizations based on clock inclusions at the generated code level. We discuss in this section some related studies about two aspects: enhancements of the SIGNAL compilation process and validation of the SIGNAL compilation process.

Enhancements of the SIGNAL compilation process

In the SIGNAL compiler, the control flow expressed by abstract clocks serves to derive a control structure in automatic code generation. Thus, the quality of clock calculus has a strong impact on the correctness and efficiency of implementations. There is some research about the enhancement of the clock calculus of synchronous languages.

In [START_REF] Feautrier | Enhancing the Compilation of Synchronous Dataflow Programs with a Combined Numerical-Boolean Abstraction[END_REF], the authors denote that there is a limitation of the clock calculus of the SIGNAL compiler, that is the SIG-NAL compiler does not fully handle numerical expressions. This has a strong impact on the analysis precision and on the quality of generated code. Thus, the authors propose a new clock abstraction, that is combined numerical-Boolean abstraction, to eliminate this problem. In the new abstraction, every signal in a program is associated with a pair of the form (clock, value), where clock is a Boolean function and value is a Boolean or numeric function. They also use a SMT (Satisfiability Modulo Theory) solver to reason on the new abstraction.

With the same purpose, in [START_REF] Gamatié | Towards Static Analysis of SIG-NAL Programs using Interval Techniques[END_REF] and [START_REF] Gamatié | An Interval-Based Solution for Static Analysis in the SIGNAL Language[END_REF], an interval-based data structure referred to as Interval-Decision Diagram (IDD) is considered for the analysis of numerical properties in SIG-NAL programs.

In [START_REF] Jose | SMT based false causal loop detection during code synthesis from polychronous specifications[END_REF], the authors address the static analysis and code generation for applications defined in MRICDF (Multi-Rate Instantaneous Channel Connected Data Flow), which is a visual actor-oriented polychronous formalism, strongly inspired by SIGNAL. The static analysis in MRICDF also relies on a Boolean encoding of specifications, thus ignoring non-Boolean properties. Moreover, a SMT-based implementation of this static analysis is proposed as an efficient alternative to the initial implementation using a prime implicant generator.

Validation of the SIGNAL compilation process

For a safety-critical system, it is naturally required that the compiler must be formally verified as well to ensure that the source program semantics is preserved. There are many approaches to gain assurance that the transformation or the translation of a specification or a program is semantic-preserving. This can be done by directly building a theoremprover-verified compiler [START_REF] Leroy | Mechanized semantics for compiler verification[END_REF][START_REF] Leroy | Formal verification of a realistic compiler[END_REF], by using translation validation [START_REF] Pnueli | Translation validation[END_REF][START_REF] Necula | Translation validation for an optimizing compiler[END_REF], proof-carrying code [START_REF] Necula | Proof-carrying code[END_REF], semantics-anchoring method [START_REF] Chen | Semantic anchoring with model transformations[END_REF][START_REF] Narayanan | Using semantic anchoring to verify behavior preservation in graph transformations[END_REF], etc.

A. Pnueli et al. propose the approach of translation validation to verify the code generator of SIGNAL [START_REF] Pnueli | Translation validation[END_REF]. In that work, the authors define a language of symbolic models to represent both the source and target programs, called Synchronous Transition Systems (STS). A STS is a set of logic formulas which describe the functional and temporal constraints of the whole program and its generated code. Then they use BDD (Binary Decision Diagrams) representations to implement the symbolic STS models, and their proof method uses a SAT-solver to reason on the signal constraints. The drawback of this approach is that it does not capture explicitly the clock semantics and in some cases, the code generator eliminates the use of a local register variable in the generated code and then, the mapping cannot be established. Additionally, for a large program, the formula is very large, including numerical expressions that make some inefficiency. Moreover, the whole calculation of a synchronous program or the generated code is considered as one atomic transition in STS, thus it does not capture the data dependencies between signals and does not explicitly prove the preservation of abstract clocks in the compiler transformations.

In [START_REF] Talpin | Formal verification of synchronous data-flow program transformations toward certified compilers[END_REF], the authors adopt translation validation to formally verify that the clock semantics and data dependence are preserved during the compilation of the SIGNAL compiler. They represent the clock semantics, the data dependence of a program and its transformed counterpart as first-order formulas which are called Clock Models and Synchronous Dependence Graphs (SDGs) respectively. Then they introduce clock refinement and dependence refinement relations which express the preservations of clock semantics and dependence, as a relation on clock models and SDGs respectively. Finally, a SMT-solver is used for checking the existence of the correct transformation relations.

In the work of [START_REF] Talpin | Formal verification of compiler transformations on polychronous equations[END_REF], the authors encode the source SIG-NAL programs and their transformations with Polynomial Dynamical Systems (PDSs), and prove that the transformations preserve the abstract clocks and clock relations of the source programs. By using simulation based on model checking techniques, this approach suffers from the increasing of the state-space when it deals with large programs.

These existing research mainly use the method of translation validation. However, translation validation treats the compiler as a "black box", namely it checks the input and output of each program transformation to validate the semantics preservation. So it yields that one need to redo the validation when the source program is changed.

In this paper, the OCaml implementation is a basis for the formal verification of the compilation of SIGNAL with a theorem prover. This work would be reused by ones interested in experimenting a new strategy for clock calculus and experimenting a new proof technique for the correctness of clock calculus. Actually, in [START_REF] Yang | Towards a verified compiler prototype for the synchronous language SIGNAL[END_REF], we have started the proof of semantics preservation of the front-end of our compiler, which is mechanized in the theorem prover Coq.

Conclusion and Future Work

This paper presents a simple and safe compiler, called MinSIGNAL, from a subset of the synchronous dataflow language SIGNAL to C, as well as its existing enhancements. For the community of statically typed functional languages, usual arguments on quality, safety and efficiency about code written in OCaml are well known and accepted for a long time. Thus, OCaml is used for the implementation of MinSIGNAL. An analysis of the SIGNAL compilation process and the existing enhancements are first given. Then, the compiler MinSIGNAL is presented step by step in details. This work is a basis for the formal verification of the compilation of SIGNAL with a theorem prover such as Coq.

In [START_REF] Yang | Towards a verified compiler prototype for the synchronous language SIGNAL[END_REF], we have started the proof of semantics preservation of the front-end of our compiler, which is mechanized in the theorem prover Coq. Moreover, we have given the backend of the compiler, including sequential code generation and multi-threaded code generation with time-predictable properties. With the rising importance of multi-core processors in safety-critical embedded systems or cyber-physical systems (CPS), there is a growing need for model-driven generation of multi-threaded code and thus mapping on multi-core. We are currently working on the proof of semantics preservation of the back-end of our compiler.

  cl ::= x | [x] | [¬x] (clock) e ::= 0 | cl | e ∧ e | e ∨ e | e\e (clock expression) Here, we have [x] ∨ [¬x] = x and [x] ∧ [¬x] = 0.

Example 2 A

 2 process named Numerical_Expr is given: process Numerical_Expr = (? integer a, b, x1; boolean c1, c2; ! integer x, y, z1, z2, z3, m, s1, s2; ) (| aˆ= bˆ= x1ˆ= c1ˆ= c2 | x := a $ init 1 | y := b $ init 2 | z1 := x when (a > 0) | z2 := x when (a <= 0) | z3 := y when (b > 0) | m := z1 de f ault z2 de f ault z3 | s1 := x1 when c1 | s2 := x1 when (c1 and c2) |); • Default Polychrony compiler A part of the result of the clock calculus generated by the compiler in Polychrony (without the option -crew) is shown as follows. Here, [a > 0], [not (a > 0)], [a <= 0], [not (a <= 0)], [b > 0], and [not (b > 0)] are considered as black boxes. So, the compiler treats [a > 0] and [not (a <= 0)], [not (a > 0)] and [a <= 0], as different clock equivalence classes. Actually they are in the same clock equivalence class respectively. It follows that the compiler cannot analyze some static properties of a program, such as clock exclusion or clock emptiness, since numerical expressions are not suitably abstracted. A part of the C code generated by Polychrony compiler is shown as follows. It also appears that the test C_s2 associated to [c1 and c2] is performed even if [c1] or [c2] tests fail. It means that the clock inclusion property [c1 and c2] ⇒ [c1]

Figure 1 A

 1 Figure 1 A modular architecture for the formalization of the SIGNAL compilation process

|( 2 )

 2 t y p e t y = T B a s i c o f s t r i n g t y p e exp = | I d e n t o f s t r i n g| C I n t o f i n t | CReal o f f l o a t | CBool o f b o o l | C S t r i n g o f s t r i n g | CChar o f c h a r Func o f s t r i n g * exp l i s t | D el a y o f exp * exp | When o f exp * exp | D e f a u l t o f exp * exp t y p e eqn = | Ass o f s t r i n g * exp | C o n s t r a i n t o f s t r i n g * exp * exp t y p e d e c l = t y * s t r i n g t y p e p r o c = P r o c o f s t r i n g * ( d e c l l i s t ) * ( d e c l l i s t ) * ( eqn l i s t ) * ( d e c l l i s t ) t y p e s p e c = p r o c l i s t Transformation of the user syntax to the kernel syntax

  t y p e k t y = KTBasic o f s t r i n g t y p e c o n s t = | S C I n t o f i n t | SCReal o f f l o a t | SCBool o f b o o l | S C S t r i n g o f s t r i n g | SCChar o f c h a r t y p e k i n d = | K s i g n a l | C l o c k | C l a s s o f Q u o t i e n t . t t y p e v a r = s t r i n g * k i n d t y p e s e x p = | SVar o f v a r | S C o n s t o f c o n s t | SFunc o f s t r i n g * v a r l i s t t y p e k e x p S i g = | KDelay o f s t r i n g * s e x p | KWhen o f s t r i n g * s t r i n g | K D e f a u l t o f s t r i n g * s t r i n g t y p e keqn = | KAss o f v a r * s e x p | KAssSig o f s t r i n g * k e x p S i g t y p e k d e c l = k t y * s t r i n g t y p e k p r o c = KProc o f s t r i n g * ( k d e c l l i s t ) * ( k d e c l l i s t ) * ( keqn l i s t ) t y p e k s p e c = k p r o c l i s t Several rules are applied to the transformation from the extended constructs to the primitive constructs. Transformation 1. We have one basic rule: the equation clk := x can be expressed using primitive constructs as follows. Clock extraction Corresponding primitive constructs clk := x clk := (x = x)

  C l o c k ) , SVar ( s1 , C l o c k ) ) ; Dass ( SVar ( " t r u e " , K s i g n a l ) , ( s , C l o c k ) , SVar ( s2 , C l o c k ) ) ] | _ -> [ ] ( * i n c a s e o f c o n s t a n t * ) end | KAssSig ( s , e s ) -> b e g i n match e s w i t h KDelay ( s1 , e ) -> [ Dass ( SVar ( " t r u e " , K s i g n a l ) , ( s , C l o c k ) , SVar ( , C l o c k ) ) ] | KWhen ( s1 , s 2 ) -> [ Dass ( SVar ( " t r u e " , K s i g n a l ) , ( " t _ _ _ " ^s2 , C l o c k ) , SFunc ( " and " , [ ( s2 , C l o c k ) ; ( s2 , K s i g n a l ) ] ) ) ; Dass ( SVar ( " t r u e " , K s i g n a l ) , ( s , C l o c k ) , SFunc ( " and " , [ ( s1 , C l o c k ) ; ( " t _ _ _ " ^s2 , C l o c k ) ] ) ) ] | K D e f a u l t ( s1 , s 2 ) -> [ Dass ( SVar ( " t r u e " , K s i g n a l ) , ( s , C l o c k ) , SFunc ( " o r " , [ ( s1 , C l o c k ) ; ( s2 , C l o c k ) ]

  i t e r ( f u n c t i o n | KAssSig ( s , e s ) -> b e g i n match e s w i t h | KDelay ( s1 , s e 1 ) -> H a s h t b l . add d c e s ( SVar ( s , C l o c k ) ) ( KAss ( ( s , K s i g n a l ) , s e 1 ) ) ; ( * i n i t ( ^y )=> y=d * ) H a s h t b l . add d d e s ( SVar ( s , C l o c k ) )

  f o l d _ r i g h t ( fun ( NFAss ( c l , c l e x p ) ) ( u n f s , n f s )-> l e t l = n f s r e p l a c e n f s ( c l k 2 e x p c l ) and r = n f s r e p l a c e n f s c l e x p i n i f b a s i c l t h e n i f o c c u r s l r t h e n ( a d d _ u n f s l r u n f s , n f s ) e l s e ( a p p l y ( NFAss ( e x p 2 c l k l , r ) ) u n f s , a d d _ n f s l r n f s ) e l s e i f b a s i c r t h e n i f o c c u r s r l t h e n ( a d d _ u n f s r l u n f s , n f s ) e l s e ( a p p l y ( NFAss ( e x p 2 c l k r , l ) ) u n f s , a d d _ n f s r l n f s ) e l s e ( a d d _ u n f s l r u n f s , n f s )) n f e q n l i s t ( [ ] , [ ] ) i n i f u n f s = [ ] t h e nn f s e l s e f a i l w i t h ( " c l e q s 2 n f c a n n o t s o l v e t h e s y s t e m " )

  l e t r e c e q _ c l a s s _ e x p = f u n c t i o n | NFVar ( sv , k1 ) a s e -> l e t i d = C l o c k e q 2 n f . e x p 2 q u o t i e n t e i n H a s h t b l . r e p l a c e esmap ( e x p 2 c l k e ) i d | NFFunc ( f , [ c e ] ) -> e q _ c l a s s _ e x p c e | NFFunc ( f , [ c e 1 ; c e 2 ] ) ->

  t y p e c l a s s i d = C l a s s i d o f UseBDD .BDD. t t y p e c l a s s e x p r = C C l a s s i d o f UseBDD .BDD. t | N o t c l o f c l a s s e x p r | Andcl o f c l a s s e x p r * c l a s s e x p r | O r c l o f c l a s s e x p r * c l a s s e x p r | D i f f c l o f c l a s s e x p r * c l a s s e x p r t y p e c l a s s e q s = ( c l a s s i d , c l a s s e x p r ) H a s h t b l . t4.5 Hierarchical representation of clock equationsBefore the construction of clock hierarchy, we add two steps, i.e., associating actions to the clock equivalence class and deterministic sorting.

( 1 )

 1 Associating actions to the clock equivalence class

l e t c

  l s e q = H a s h t b l . c r e a t e 1000 l e t d d e s= H a s h t b l . c r e a t e 1000 l e t d c e s = H a s h t b l . c r e a t e 1000 l e t a t t a c h E q u a t i o n e q n s= L i s t . i t e r ( f u n c t i o n | S A s s S i g ( s , e s ) -> b e g i n match e s w i t h | SDelay ( s1 , s e 1 ) -> H a s h t b l . add d d e s ( S A s s S i g ( s , e s ) ) ( S A s s S i g ( s , e s ) ) | S D e f a u l t ( se1 , s e 2 ) -> l e t i d 1 = H a s h t b l . f i n d ( C p t _ e q c l a s s . esmap ) ( Hat ( s e 1 ) ) i n l e t i d 2 = H a s h t b l . f i n d ( C p t _ e q c l a s s . esmap ) ( Hat ( " d e f _ _ _ " ^s e 2 ) ) i n H a s h t b l . add c l s e q i d 1 ( SAss ( s , S I d e n t ( s e 1 ) ) ) ; H a s h b l . add c l s e q i d 2 ( SAss ( s , S I d e n t ( s e 2 ) ) ) ; H a s h t b l . add d c e s ( SAss ( s , S I d e n t ( s e 1 ) ) ) ( SAss ( s , S I d e n t ( s e 1 ) ) ) ; H a s h t b l . add d c e s ( SAss ( s , S I d e n t ( s e 2 ) ) ) ( SAss ( s , S I d e n t ( s e 2 ) ) ) | SWhen ( se1 , s e 2 ) -> l e t i d 1 = H a s h t b l . f i n d ( C p t _ e q c l a s s . esmap ) ( Hat ( s ) ) i n H a s h t b l . add c l s e q i d 1 ( SAss ( s , S I d e n t ( s e 1 ) ) ) ; H a s h t b l . add d c e s ( SAss ( s , S I d e n t ( s e 1 ) ) ) ( SAss ( s , S I d e n t ( s e 1 ) ) ) end | SAss ( s , ex ) a s e -> l e t i d 1 = H a s h t b l . f i n d ( C p t _ e q c l a s s . esmap ) ( Hat ( s ) ) i n H a s h t b l . add c l s e q i d 1 e ; H a s h t b l . add d c e s e e

e l s e compare a c t 1 a c t 2 |

 2 t y p e s a c t i o n = | Dass o f s t r i n g * s e x p | C a s s o f c l a s s i d * c l a s s e x p r | I n p u t o f s t r i n g | O u t p u t o f s t r i n g l e t a c t _ c o m p a c t 1 a c t 2 = i f a c t 1 = a c t 2 t h e n 0 e l s e match ( a c t 1 , a c t 2 ) w i t h | ( Dass ( s1 , e1 ) , Dass ( s2 , e2 ) ) -> i f v a r _ i n _ s e x p s 1 e2 t h e n -1 e l s e i f v a r _ i n _ s e x p s 2 e1 t h e n 1 e l s e compare a c t 1 a c t 2 | ( Dass ( s1 , e1 ) , C a s s ( C l a s s i d c l 2 , c l e 2 ) ) -> i f v a r _ i n _ c l a s s e x p r s 1 c l e 2 t h e n -1 e l s e i f s e x p _ i n _ c l a s s i d c l 2 e1 t h e n 1 e l s e compare a c t 1 a c t 2 | ( C a s s ( c l 1 , c l e 1 ) , C a s s ( c l 2 , c l e 2 ) ) -> i f c l a s s i d _ i n _ c l a s s e x p r c l 1 c l e 2 t h e n -1 e l s e i f c l a s s i d _ i n _ c l a s s e x p r c l 2 c l e 1 t h e n 1 e l s e compare a c t 1 a c t 2 | ( C a s s ( C l a s s i d c l 1 , c l e 1 ) , Dass ( s2 , e2 ) ) -> i f s e x p _ i n _ c l a s s i d c l 1 e2 t h e n -1 e l s e i f v a r _ i n _ c l a s s e x p r s 2 c l e 1 t h e n 1 ( I n p u t s1 , I n p u t s 2 ) -> compare s 1 s 2 | ( I n p u t s1 , _ ) -> -1 | ( _ , I n p u t s 2 ) -> 1 | ( O u t p u t s1 , O u t p u t s 2 ) -> compare s 1 s 2 | ( O u t p u t s1 , _ ) -> 1 | ( _ , O u t p u t s 2 ) -> -1

Figure 2

 2 Figure 2 Optimization of the clock hierarchy

Figure 3

 3 Figure 3 Sequential code generation from SIGNAL programs

of

  Toulouse III since 1989 and is now Professor of computer science since 2003. His main research inter-ests concern formal specifications, automated and assisted verification of protocols as well as of proof en-vironments. He has participated in European and national projects related to these domains. His current activities are linked to real time modeling and verification either via model checking techniques or at the semantics level. Dr. Mamoun FILALI is a full time researcher at CNRS (Centre National de la Recherche Scientifique). His main research interests concern the certified development of embedded systems. He is concerned by formal methods, model checking and theorem proving. During the last years, he has been mainly involved in the french nationwide TOPCASED project where he was concerned by the verification topic. He has also participated to the proposal of the AADL behavioral annex which has been been adopted as part of the AADL SAE standard.

Table 1

 1 Synchronizations of each primitive construct

Table 2

 2 The OCaml code size of MinSIGNAL

	Module name	OCaml code
	Normalization of the user program	750 lines
	Intermediate representation S-CGA	350 lines
	Solving the clock equation system	750 lines
	Hierarchical representation of clock equations	550 lines
	Code generation and optimization	500 lines

Table 3

 3 Extended synchronizations of each primitive construct

	P	synchronizations o f P in extended clock abstraction
	x

| ( | CLK := when ( a >0) | CLK_13 := when ( n o t ( a > 0 ) ) | ) | ( | CLK_14 := CLK ^ * CLK_z1 | ) | ( | CLK_z1 := CLK_a ^ * CLK | CLK_z1 ^= z1 | ( | z1 := x when CLK_z1 | ) | ) | ( | CLK_17 := when ( a <=0) | CLK_18 := when ( n o t ( a <=0)) | ) | ( | CLK_19 := CLK_17 ^ * CLK_z2 | ) | ( | CLK_z2 := CLK_a ^ * CLK_17 | CLK_z2 ^= z2 | ( | z2 := x when CLK_z2 | ) | ) | ( | CLK_22 := when ( b >0) | CLK_23 := when ( n o t ( b > 0 ) ) | ) | ( | CLK_24 := CLK_22 ^ * CLK_z3 | ) | ( | CLK_z3 := CLK_a ^ * CLK_22 | CLK_z3 ^= z3 | ( | z3 := y when CLK_z3 | ) | )

Acknowledgements This work is supported in part by the National Natural Science Foundation of China under Grant 61502231, the National Defense Basic Scientific Research Project under Grant JCKY2016203B011, the Natural Science Foundation of Jiangsu Province under Grant BK20150753, the Project of the State Key Laboratory of Software Development Environment of China under Grants SKLSDE-2015KF-04, the Avionics Science Foundation of China under Grant 2015ZC52027, China Postdoctoral Science Foundation, and the Open Project of Shanghai Key Laboratory of Trustworthy Computing under Grant 07dz22304201502, and the RTRA STAE Foundation in France (http://www.fondation-stae.net/).