Zhibin Yang
email: zhibin.yang@irit.fr

Jean-Paul Bodeveix
email: bodeveix@irit.fr

Mamoun Filali
email: filali@irit.fr

A comparative study of two formal semantics of the SIGNAL language

Keywords: synchronous language, SIGNAL, trace semantics, tagged model semantics, semantics equivalence, Coq { b, b 1, b 2, . .

SIGNAL is a part of the synchronous languages family, which are broadly used in the design of safety-critical real-time systems such as avionics, space systems, and nuclear power plants. There exist several semantics for SIG-NAL, such as denotational semantics based on traces (called trace semantics), denotational semantics based on tags (called tagged model semantics), operational semantics presented by structural style through an inductive definition of the set of possible transitions, operational semantics defined by synchronous transition systems(STS), etc. However, there is little research about the equivalence between these semantics.

In this work, we would like to prove the equivalence between the trace semantics and the tagged model semantics, to get a determined and precise semantics of the SIGNAL language. These two semantics have several different definitions respectively, we select appropriate ones and mechanize them in the Coq platform, the Coq expressions of the abstract syntax of SIGNAL and the two semantics domains, i.e., the trace model and the tagged model, are also given. The distance between these two semantics discourages a direct proof of equivalence. Instead, we transform them to an intermediate model, which mixes the features of both the trace semantics and the tagged model semantics. Finally, we get a determined and precise semantics of SIGNAL.

Introduction

Safety-critical real-time systems such as avionics, space systems, and nuclear power plants, are also considered as reactive systems [START_REF] Harel | On the development of reactive systems[END_REF], because they always interact with their environments continuously. 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. The arrival time of events may be different, and the computation needs time. Synchronous method 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 input-computationoutput, which takes zero time. Secondly, the different arrival time of events are abstracted as the relative order between events. Even of the physical time is abstracted, the inherent functional properties are not changed, so we can say this method focuses on functional behaviors at a platformindependent level.

There are several synchronous languages, such as ESTER-EL [START_REF] Boussinot | The esterel language[END_REF], LUSTRE [START_REF] Halbwachs | The synchronous data-flow 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]. Synchronous languages can be considered as different implementations of the synchronous hypothesis. As a main difference from other synchronous languages, SIGNAL naturally considers a mathematical time model, in term of a partial order relation, to describe multi-clocked systems without the neces-sity of a global clock. This feature permits the description of globally asynchronous locally synchronous systems (GAL-S) [START_REF] Teehan | A survey and taxonomy of gals design styles[END_REF][START_REF] Benveniste | From synchrony to asynchrony[END_REF] conveniently.

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[END_REF][START_REF] Guernic | Data-flow to von neumann: the signal approach[END_REF], denotational semantics based on tags which are elements of a partially ordered dense set (called tagged model semantics) [START_REF] Gamatié | Designing embedded systems with the SIGNAL programming language[END_REF][START_REF] Guernic | Polychrony for system design[END_REF], operational semantics presented by structural style through an inductive definition of the set of possible transitions [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[END_REF], operational semantics defined by synchronous transition systems (STS) [START_REF] Pnueli | Tanslation validation[END_REF]. The differences between the trace semantics and the tagged model semantics are: logical time is represented by a totally ordered set (the set of natural integers N) or a partially ordered set; absence of events is explicitly specified (by the ⊥ symbol) or not. Additionally, Nowak proposes a co-inductive semantics for modeling SIGNAL in the Coq proof assistant [START_REF] Nowak | Co-inductive axiomatization of a synchronous language[END_REF][START_REF] Kerboeuf | Specification and verification of a stream-boiler with signal-coq[END_REF]. However, there is little research about the equivalence between these semantics. The trace semantics and the tagged model semantics are more commonly used, so we would like to prove the equivalence between them, to get a determined and precise semantics of the SIGNAL language.

The rest of the paper is organized as follows. Section 2 introduces the basic concepts of the SIGNAL language. The abstract syntax of SIGNAL and its Coq expression is given in Section 3. Section 4 presents the definitions of the two semantics domains, i.e., the trace model and the tagged model. Section 5 gives the two formal semantics and their Coq specifications. The proof of the semantics equivalence is presented in Section 6. Section 7 discusses the related work, and Section 8 gives some concluding remarks.

An Introduction to SIGNAL

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 or 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 set of logical instants.

Moreover, SIGNAL can specify the relations between the abstract clocks of signals in two ways: implicitly or explicitly.

Primitive Constructs SIGNAL uses several primitive constructs to express the relations between signals, including relations between values and relations between abstract clocks. Moreover, 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 a 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 check the output of 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.

Example 2 Let us consider a simple process Count [START_REF] Guernic | Polychrony for system design[END_REF]. It accepts an input signal reset and delivers the integer output signal val. The local variable counter is initialized to 0 and stores the previous value of the signal val. When an input reset occurs, the signal val is reset to 0. Otherwise, the signal val takes an increment of the variable counter. The process Par-allelCount is the composition of two Count processes. Here, the program is not deterministic. 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.

process ParallelCount = (! integer x1, x2; ) (| x1 := Count(r) | x2 := Count(r) |)
• Clock synchronization, the equation

x 1 ˆ= x 2 ˆ= • • • ˆ=x n specifies that signals x 1 , x 2 , • • • , x n

Abstract Syntax of SIGNAL and its Coq Expression

In this section, we first give a brief introduction of the theorem prover Coq, then, we give the abstract syntax of SIGNAL and its Coq expression.

A Brief Introduction of Coq

Coq [START_REF] Bertot | Interactive Theorem Proving and Program Development: Coq Art: The Calculus of Inductive Constructions[END_REF] is a theorem prover based on the Calculus of Inductive Constructions which is a variant of type theory, following the "Curry-Howard Isomorphism" paradigm, enriched with support for inductive and co-inductive definitions of data types and predicates. From the specification perspective, Coq offers a rich specification language to define problems and state theorems. From the proof perspective, proofs are developed interactively using tactics, which can reduce the workload of the users. Moreover, the type-checking performed by Coq is the key point of proof verification.

Here, we try to give an intuitive introduction to the Coq terminologies which are used in this paper. In the spirit of "Curry-Howard Isomorphism" paradigm, types may represent programming data-types or logical propositions. So, the Coq objects used in this paper can be sorted into two categories: the Type sort and the Prop sort:

• Type is the sort for data types and mathematical structures, i.e. well-formed types or structures are of type Type. Data types can be basic types such as nat, bool, nat → nat, etc., and can be inductive structures, record and co-inductive structures (for infinite objects, as for example infinite sequences). We use Fixpoint and CoFixpoint definitions to define functions over inductive and to co-inductive data types. • Prop is the sort for propositions, i.e. well-formed propositions are of type Prop. We can define new predicates using inductive, record (for conjunctions of properties) or co-inductive definitions.

The Abstract Syntax of SIGNAL

The semantics of each of the extended constructs is defined in term of the primitive constructs, so we just consider the primitive constructs, that is core-SIGNAL. Its abstract syntax is presented as follows.

P ::= x := f (x 1 , • • • , x n ) instantaneous f unction |x := x 1 $ init c delay |x := x 1 when x 2 undersampling |x := x 1 de f ault x 2 deterministic merging |P|P ′ composition |P/x local declaration
To express more complex SIGNAL programs, all the rightside signal variables of the equations can be replaced by an expression on signal variables.

Here we give the Coq expression of the abstract syntax of SIGNAL. It is parameterized by the set XVar of signal variables, and the set Value of values that can be taken by the variables. isTrue checks that a value is considered to be true. mkBool is used to coerce Bool(s) to Value(s). The type Process is defined using five constructors corresponding to the constructs of the core-SIGNAL. We give a very abstract expression of an instantaneous function. The function Pass takes three parameters: a function f of type ((Index → Value) → Value) having an indexed set of input parameters, a variable name of type XVar which contains the left-side variable and an indexed set of variable names of type (Index → XVar) which denotes the actual parameters of f . Index, for example 1, • • • , n, represents a set used to index the parameters. Similarly, Pdelay, Pwhen, Pdefault, and Ppar build the corresponding SIGNAL constructs. However, the local declaration is ignored, to get a simplest criterion for the proof of semantics equivalence (see Section 5 and Section 6).

The SIGNAL language specifies a system behavior as a platform-independent model at first. However, it is finally needed to guarantee a correct physical implementation from it (i.e., need to deal with physical time). A formal support for allowing time scalability in design is given in the modeling environment Polychrony [START_REF]The polychrony toolset[END_REF] by the so-called stretch-closure property. This property can be defined both on the trace model and on the tagged model.

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:

V ⊥ = V ∪ {⊥}
The corresponding Coq expression is given as follows: Definition 1 (VSignal) [START_REF] Gamatié | Designing embedded systems with the SIGNAL programming language[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.

A signal can be finite. However, we can extend the finite signal with infinite absences, to get an infinite one. So, in the Coq expression, a signal is defined as an infinite object.

C o I n d u c t i v e V S i g n a l : Type := Vs : EValue → V S i g n a l → V S i g n a l .

In the following paragraphs, the definition of traces is given. 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.

The absent trace on X (N → {⊥ e (X)}), i.e., the infinite sequence formed by the infinite repetition of ⊥ e (X), is denoted

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

Example 3 Let us consider the following equation: x 3 := x 1 * x 2 . The set of signal variables is X = {x 1 , x 2 , x 3 }. A possible trace is given as follow:

x 1 ⊥ 3 3 ⊥ ⊥ 0 • • • x 2 ⊥ 5 7 ⊥ ⊥ 9 • • • x 3 ⊥ 15 21 ⊥ ⊥ 0 • • •
The trace can be seen as a sequence of events:

{e 0 :           x 1 → ⊥ x 2 → ⊥ x 3 → ⊥           , e 1 :           x 1 → 3 x 2 → 5 x 3 → 15           , • • • }
The Coq expression of the definition of traces is given as follows. As mentioned before, the set of instants where a signal takes a value is the abstract clock of the signal. Its Coq expression is given as follows.

C o F i x p o i n t AClock ( x : XVar ) ( t r : T r a c e ) : V S i g n a l := match t r w i t h Tr s t t r ' ⇒ match s t x w i t h Absence ⇒ Vs Absence ( AClock x t r ' ) | _ ⇒ Vs ( Val ( mkBool t r u e ) ) ( AClock x t r ' ) end end .

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.

The Coq expression is given as follows:

Record S p r o c e s s : Type : = { sdom : XVar → Prop ; s t r a c e s : T r a c e → Prop } .

Additionally, we give the definition of the stretch-closure property on the trace model as the definition of compression of a trace given in [START_REF] Benveniste | A denotational theory of synchronous reactive systems[END_REF]. The intuition is to consider a trace as an elastic with ordered marks on it. If it is stretched, the marks remain in the same order but have more space (time) between each other by adding columns of ⊥ (see Fig. 1). The same holds for a set of traces (a behavior), so stretching gives rise to an equivalence between behaviors (stretch equivalence).

Definition 5 (Stretching) For a given subset X of X, a trace tr 1 is less stretched than another trace tr 2 , noted tr 1 ≤ τ X tr 2 , iff there exists a mapping f : N → N such as:

• ∀x ∈ X ∀i ∈ N, tr 2 ( f (i))(x) = tr 1 (i)(x) • ∀x ∈ X ∀ j ∈ N, tr 2 ( j)(x) = ⊥, i f j range( f ) • ∀i j ∈ N, i < j ⇒ f (i) < f ( j)
The Coq expression is given as follows. trGetEV is used to get the value (including ⊥) of each signal at each instant of a trace. F i x p o i n t t r G e t E V t r i x : EValue := match i , t r w i t h O, ( Tr s t t r ' ) ⇒ s t x | ( S j ) , ( Tr s t t r ' ) ⇒ t r G e t E V t r ' j x end .

Record S t r e t c h i n g ( t r 1 : T r a c e ) ( t r 2 : T r a c e )

: Prop : = { S t r e t c h _ f : n a t → n a t ; S t r e t c h _ v a l : ∀ x i , t r G e t E V t r 1 i x = t r G e t E V t r 2 ( S t r e t c h _ f i ) x ; S t r e t c h _ b o t : ∀ x j , ( ∀ i , S t r e t c h _ f j i ) → t r G e t E V t r 2 j x = Absence ; S t r e t c h _ m o n o : ∀ i j , i < j → S t r e t c h _ f i < S t r e t c h _ f j } .

Definition 6 (Stretch Equivalence) For a given subset X of X, two traces tr 1 and tr 2 are stretch-equivalent, noted tr 1 ≷ tr 2 , iff there exists another behavior tr 3 less stretched than both tr 1 and tr 2 , i.e., tr 1 ≷ tr 2 iff ∃tr 3 tr 3 ≤ τ X tr 1 and

tr 3 ≤ τ X tr 2 .
The Coq expression is given as follows:

I n d u c t i v e S t r e t c h _ E q u i v a l e n c e ( t r 1 : T r a c e ) ( t r 2 : T r a c e ) : Prop := S t r _ E q P r f : ∀ t r 3 : T r a c e , S t r e t c h i n g t r 3 t r 1 → S t r e t c h i n g t r 3 t r 2 → S t r e t c h _ E q u i v a l e n c e t r 1 t r 2 .

Definition 7 (Stretch Closure) For a given trace tr, the set of all traces that are stretch-equivalent to tr, defines its stretch closure, noted tr*.

The stretch closure of a set of traces τ X , includes all the traces resulting from the stretch closure of each trace tr ∈ τ X , i.e., tr∈τ X tr * .

The Coq expression is given as follows:

I n d u c t i v e S t r e t c h _ C l o s u r e ( t r s : T r a c e → Prop ) : T r a c e → Prop := S t r e t c h _ c l : ∀ t r 1 t r 2 : T r a c e , t r s t r 1 → S t r e t c h _ E q u i v a l e n c e t r 1 t r 2 → S t r e t c h _ C l o s u r e t r s t r 2 .

Definition 8 (Stretch-Closed) A SIGNAL process is stretch-closed, iff, for all tr ′ ∈ S process.straces and for all tr ∈ τ X , tr ≷ tr ′ ⇒ tr ∈ S process.straces

Tagged Model

Lee and Sangiovanni-Vincentelli proposed the tagged-signal model [START_REF] Lee | A framework for comparing models of computation[END_REF] to compare various models of computation. It is a denotational approach where a system is modeled as a set of behaviors. Behaviors are sets of events. Each event is a valuetag pair. Complex systems are derived through the parallel composition of sub-systems, by taking the intersection of the sets of behaviors. After that, the tagged-signal model is also used to express the semantics of the SIGNAL language [START_REF] Gamatié | Designing embedded systems with the SIGNAL programming language[END_REF][START_REF] Guernic | Polychrony for system design[END_REF], because this model can represent the feature of multiclock naturally.

We reuse the sets X and V defined in Section 4.1. Definition 9 (Tag Structure) A tag structure is a tuple (T, ≤), where:

• T is the set of tags.

• ≤ is a partial order on T.

The Coq expression is given as follows. Tag represents a set of tags, tle is a partial order, and tlt is defined as a strict partial order.

Record TAG: Type : = { Tag : Type ; t l e : Tag → Tag → Prop ; t p o : o r d e r Tag t l e ; t l t t 1 t 2 := t l e t 1 t 2 ∧ t 1 t 2 ; } .

Definition 10 (Tagged Event) [START_REF] Gamatié | Designing embedded systems with the SIGNAL programming language[END_REF] A tagged event e on a given tag structure (T, ≤) is a pair (t, v) ∈ T × V.

Example 4 A tag structure associated with events is given in Fig. 2. Sharing the same tag among different events represents the events are synchronous at that logical instant.

A totally ordered set of tags C ∈ T is called a chain, and min{C} denotes the minimum element of C. In addition, we denote by C T the set of all chains on (T, ≤).

Definition 11 (TSignal) A signal on a tag structure (T, ≤) is a partial function s ∈ C ⇀ V which associates values with the tags that belong to a chain C.

Let the set of signals on (T, ≤) be noted S T . Here, we give two signals as an example (see Fig. 3). The Coq expression is given as follows. The type Tsig-nal_from is used to construct a chain from a tag t. Tsignal represents the set of signals. "@<" is the notation for the strict partial order tlt.

C o I n d u c t i v e T s i g n a l _ f r o m {G :TAG} ( t : Tag G ) : Type := Tend : T s i g n a l _ f r o m t | T n e x t : ∀ t n , t @< t n → V a l u e → T s i g n a l _ f r o m t n → T s i g n a l _ f r o m t .
I n d u c t i v e T s i g n a l G : Type := Tempty : T s i g n a l G | Tfrom : ∀ ( t : Tag G) , V a l u e → T s i g n a l _ f r o m t → T s i g n a l G .

Definition 12 (Behavior) Given a tag structure (T, ≤), a behavior b on X ⊆ X is a function b ∈ X → S T that associates each variable x ∈ X with a signal s on (T, ≤).

Notice that, here signal variables and signals are treated separately, and the behaviors on tag structures give the mapping between them.

The Coq expression is given as follows. In the type Tbehavior, each variable is associated with a signal.

D e f i n i t i o n T b e h a v i o r (G :TAG

) : = XVar → T s i g n a l G .
We denote by B |X the set of behaviors of domain X ⊆ X on (T, ≤). Given a behavior b ∈ B |X , we write vars(b) and tags(b(x)) (x ∈ vars(b)) to denote the signal variables considered in b and the set of tags associated with the signal variable x. 0 |X expresses the association of X with empty signal.

Definition 13 (Tprocess) Given a SIGNAL process, its tagged model semantics, denoted as Tprocess, includes a set of signal variables and a set of behaviors on tag structures.

The Coq expression is given as follows:

Record T p r o c e s s (G :TAG) :

= { tdom : XVar → Prop ; t b e h a v i o r s : T b e h a v i o r G → Prop } .
Remark 1 The logical time used in the trace model is a totally ordered set, and the absence of events is explicitly specified, while the logical time used in the tagged model is a partially ordered set, and the absence of events is not specified. Moreover, a tag structure may correspond to a set of traces.

Additionally, we give the definition of the stretch-closure property on the tagged model [START_REF] Gamatié | Designing embedded systems with the SIGNAL programming language[END_REF][START_REF] Guernic | Polychrony for system design[END_REF]. The intuition is to consider a signal as an elastic with tags on it. If it is stretched, tags remain in the same order but have more space (time) between each other (see Fig. 4). The same holds for a set of elastics: a behavior. If elastics are equally stretched, the partial order between tags is unchanged.

• ∀x ∈ vars(b 1 ), f (tags(b 1 (x))) = tags(b 2 (x)) • ∀x ∈ vars(b 1 ) ∀t ∈ tags(b 1 (x)), b 1 (x)(t) = b 2 (x)( f (t)) • ∀t 1 , t 2 ∈ tags(b 1 ), t 1 < t 2 ⇒ f (t 1 ) < f (t 2 ) • ∀C ∈ C T , ∀t ∈ C, t ≤ f (t)
The Coq expression is given as follows. tags_ f rom and tags are used to get the tags of a given signal, btags represents the tags of all the signals in a given behavior, while tval_ f rom and tval are used to get the value at each tag of a signal. "@<=" is the notation of tle.

I n d u c t i v e t a g s _ f r o m {G} ( t t 0 : Tag G) : T s i g n a l _ f r o m t 0 → Prop := i n _ c u r r : ∀ t i h v i s ' , t = t i → t a g s _ f r o m t t 0 ( T n e x t t 0 t i h v i s ' ) | i n _ n e x t : ∀ t i h v i s ' , t a g s _ f r o m t t i s '
→ t a g s _ f r o m t t 0 ( T n e x t t 0 t i h v i s ' ) .

I n d u c t i v e t a g s {G} t : T s i g n a l G → Prop := i n _ f i r s t : ∀ t 0 v0 s ' , t 0 = t → t a g s t ( Tfrom G t 0 v0 s ' ) | i n _ f r o m : ∀ t 0 v0 s ' , t a g s _ f r o m t t 0 s ' → t a g s t ( Tfrom G t 0 v0 s ' ) . Record t S t r e t c h i n g {G1 G2 :TAG} ( b1 : T b e h a v i o r G1 ) ( b2 : T b e h a v i o r G2 ) ( dom : XVar → Prop ) : Prop : = { t S t r e t c h _ f : Tag G1 → Tag G2 ; t S t r e t c h _ t a g s :

∀ t 2 x , dom x → t a g s t 2 ( b2 x ) → ∃ t 1 , t a g s t 1 ( b1 x ) ∧ t 2 = t S t r e t c h _ f t 1 ; t S t r e t c h _ v a l : ∀ t x v , dom x → t v a l ( b1 x ) t v → t v a l ( b2 x ) ( t S t r e t c h _ f t ) v ; t S t r e t c h _ m o n o : ∀ t 1 t 2 : Tag G1 ,
b t a g s b1 dom t 1 → b t a g s b1 dom t 2 → t 1 @< t 2 → t S t r e t c h _ f t 1 @< t S t r e t c h _ f t 2 ; t S t r e t c h _ i n c r : ∀ t , t @<= t S t r e t c h _ f t } . The Coq expression is given as follows. The Coq expression is given as follows.

Two Formal Semantics

Primitive constructs of the SIGNAL language specify the relations between signals at the syntax level. The trace semantics and the tagged model semantics are both denotational style. They interpret and define precisely the relations between values and the relations between clocks of signals in their semantics domains. In this paper, the semantics ignores the local declaration of signal variables to get a simplest criterion for the proof of semantics equivalence.

Trace Semantics

There are several definitions of the trace semantics of SIG-NAL [START_REF] Besnard | SIGNAL V4 Reference Manual[END_REF][START_REF] Gamatié | Designing embedded systems with the SIGNAL programming language[END_REF][START_REF] Guernic | Data-flow to von neumann: the signal approach[END_REF], we select [START_REF] Gamatié | Designing embedded systems with the SIGNAL programming language[END_REF] as the reference paper semantics and mechanize it in Coq. Most of the Coq expressions are close to the paper semantics, but some expressions are not, so we need to justify the equivalence between them. We also refer to the Coq expressions of Nowak [START_REF] Nowak | Co-inductive axiomatization of a synchronous language[END_REF][START_REF] Kerboeuf | Specification and verification of a stream-boiler with signal-coq[END_REF].

Here, each single signal is observed in the reference paper semantics, while the corresponding trace with signal variables x, x 1 , . . . , x n is directly used in the Coq expressions. The difference between them has been given in Section 4.1. The mapping between them is done at the end (i.e., the definition Process2Sprocess).

Trace Semantics 1 (Instantaneous function) The trace semantics of the instantaneous function is defined as follows: Trace Semantics 2 (Delay) The trace semantics of the delay construct is defined as follows:

∀τ ∈ N s τ = ⊥ i f s 1τ = . . . = s nτ = ⊥ f (s 1τ , . . . , s nτ ) i f s 1τ ⊥ ∧ . . . ∧ s nτ ⊥ At each instant τ,
-(∀τ ∈ N) s 1τ = ⊥ ⇔ s τ = ⊥ -{k | s 1k ⊥} ∅ ⇒ s min{k|s 1k ⊥} = c -(∀τ ∈ N) s 1τ ⊥ ∧ {k > τ | s 1k ⊥} ∅ ⇒ s min{k>τ|s 1k ⊥} = s 1τ
Here, we make the definition of the trace semantics of Delay in [START_REF] Gamatié | Designing embedded systems with the SIGNAL programming language[END_REF] more precise. min(S) denotes the minimum of a non-empty set of naturals. Similarly to the instantaneous function, the delay construct also requires signals s and s 1 have the same clock, denoted as s ˆ= s 1 . Given a logical instant τ, s takes the most recent value of s 1 except the one at τ. Initially, s takes the value c.

The Coq expression is given as follows. Trace Semantics 3 (Undersampling) The trace semantics of the undersampling construct is defined as follows:

∀τ ∈ N s τ = s 1τ i f s 2τ = true ⊥ otherwise
Here, s and s 1 have the same type and s 2 is a boolean signal. The clock of s is the intersection of the clock of s 1 and the clock of s 2 , denoted as s=s 1 ˆ* [s 2 ], while [s 2 ] represents the true occurrences of s 2 . Given a logical instant τ, s τ gets the value of s 1τ when s 2τ is true, else gets the value ⊥.

The Coq expression is given as follows. Trace Semantics 4 (Deterministic merging) The trace semantics of the deterministic merging construct is defined as follows: ∀τ ∈ N

s τ = s 1τ i f s 1τ ⊥ s 2τ otherwise
Here, signals s, s 1 and s 2 have the same type. The clock of s is the union of the clocks of s 1 and s 2 , denoted as s = s 1 ˆ+ s 2 . Given a logical instant τ, s τ gets the merge of the values of s 1τ and s 2τ , and the value of s 1τ has a higher priority.

The Coq expression is given as follows. Finally, we apply these semantics rules to a SIGNAL process, to get a complete semantics of the process, that is Sprocess (defined in Section 4.1). SPassignment, SPdelay, SPwhen and SPdefault, used to construct the corresponding Sprocess on the semantics rule Sassignment, Sdelay, Swhen and Sdefault respectively, while the function Pro-cess2Sprocess is used to combine them as one Sprocess. We also give the semantics of processes composition, that is SPprod.

Program D e f i n i t i o n S P a s s i g n m e n t

tr1 : x1 1 ⊥ 2 ⊥ 0 1 ⊥ 2 ⊥ 3 ⊥ 0 ⊥ . . . x2 ⊥ 1 ⊥ 2 0 ⊥ 1 ⊥ 2 ⊥ 3 0 ⊥ . . . tr2 : x1 0 1 2 ⊥ 0 1 2 ⊥ 3 0 ⊥ . . . x2 0 ⊥ ⊥ 1 0 ⊥ ⊥ 1 ⊥ 0 ⊥ . . .
Property 1 For all SIGNAL processes, the trace semantics is stretch-closed.

Tagged Model Semantics

Similarly, there are several definitions of the tagged model semantics of SIGNAL [START_REF] Gamatié | Designing embedded systems with the SIGNAL programming language[END_REF][START_REF] Guernic | Polychrony for system design[END_REF], we select [START_REF] Gamatié | Designing embedded systems with the SIGNAL programming language[END_REF] as the reference paper semantics and mechanize it in Coq.

Here, signal variables x, x 1 , . . . , x n are used in the reference paper semantics, while the tag structure with signals s, s 1 , . . . , s n is used in the Coq expressions. The relation between them has been shown in Section 4.2. The mapping between them is done at the end (i.e., the definition Pro-cess2Tprocess).

Tagged Model Semantics 1 (Instantaneous function) The tagged model semantics of the instantaneous function is defined as follows:

x := f (x 1 , • • • , x n ) = {b ∈ B |x,x 1 ,••• ,x n |tags(b(x)) = tags(b(x 1 )) = • • • = tags(b(x n )) = C ∈ C T and ∀t ∈ C, b(x)(t) = f (b(x 1 )(t), • • • , b(x n )(t)
I n d u c t i v e t v a l _ f r o m {G} ( t 0 : Tag G ) : T s i g n a l _ f r o m t 0 → Tag G → V a l u e → Prop := t v _ c u r r : ∀ t h v s t t vv , t = t t → v=vv → t v a l _ f
s i g n a l G → Tag G → V a l u e → Prop := t v _ f i r s t : ∀ t v s t t vv , t = t t → v=vv → t v a l ( Tfrom G t v s ) t t vv | t v _ f r o m : ∀ t 0 v s t t vv ,
t v a l _ f r o m t 0 s t t vv → t v a l ( Tfrom G t 0 v s ) t t vv . D e f i n i t i o n t s y n c {G} ( s 1 s 2 : T s i g n a l G ) : Prop := ∀ t , t a g s t s 1 ↔ t a g s t s 2 .

Record T S a s s i g n m e n t {G} s I n d e x ( f : ( I n d e x → V a l u e ) → V a l u e ) ( s i : I n d e x → T s i g n a l G) :

Prop : = { TSA_T : ∀ t d v , ( ∀ i , t v a l ( s i i ) t ( d i ) ) → t v a l s t v → v = f d ; TSA_S : ∀ i , t s y n c ( s i i ) s } .
Tagged Model Semantics 2 (Delay) The tagged model semantics of the delay construct is defined as follows:

x := x 1 $ init c = {0 |x,x 1 }∪ {b ∈ B x,x 1 | tags(b(x)) = tags(b(x 1 )) = C ∈ C T \{∅}; b(x)(min(C)) = c; ∀t ∈ C\min(C), b(x)(t) = b(x 1 )(pred C (t))}
Similarly to the instantaneous function, the tags of each signal represent the same chain C. When the signals are both present, x gets the value c at the initial tag of C, and for all the other tags t ∈ C, x gets the value carried by x 1 at the predecessor of t.

The Coq expression is given as follows. TSY0 and TSYN are used to express the relation between values, while TSYL represents the signals are synchronous. tfirst s t represents that t is the first tag of a given signal s, and tnext s 1 t 1 t 2 means t 2 is the next tag of t 1 of a given signal s 1 (it has the same meaning as t 1 = pred C (t 2 )).

I n d u c t i v e t f i r s t {G} : T s i g n a l G → Tag G → Prop := t f _ p r f : ∀ t v

Tagged Model Semantics 3 (Undersampling)

The tagged model semantics of the undersampling construct is defined as follows:

x := x 1 when x 2 = {b ∈ B |x,x 1 ,x 2 |tags(b(x)) = {t ∈ tags(b(x 1 )) ∩tags(b(x 2 ))|b(x 2 )(t) = true} = C ∈ C T and ∀t ∈ C, b(x)(t) = b(x 1 )(t)}
The set of tags of x is the intersection of the set of tags associated with x 1 and the set of tags at which x 2 carries the value true. Moreover, at each tag of x, the value held by x is the value of x 1 .

The Coq expression is given as follows. Here, we give all the cases. tnval s t means it is absent at the tag t of a given signal s.

D e f i n i t i o n t n v a l {G} s ( t : Tag G ) : Prop

:= ¬∃ v , t v a l s t v .
Record TSwhen {G} ( s s 1 s 2 : T s i g n a l G ) : Prop : = { TSW_T : ∀ t v b , t v a l s 1 t v → t v a l s 2 t b → i s T r u e b → t v a l s t v ; TSW_F : ∀ t b , t v a l s 2 t b → ¬ i s T r u e b → t n v a l s t ; TSW_U1 : ∀ t , t n v a l s 1 t → t n v a l s t ; TSW_U2 : ∀ t , t n v a l s 2 t → t n v a l s t } .

Tagged Model Semantics 4 (Deterministic merging)

The tagged model semantics of the deterministic merging construct is defined as follows:

x := x 1 de f ault x 2 = {b ∈ B |x,x 1 ,x 2 |tags(b(x)) = tags(b(x 1 )) ∪ tags(b(x 2 )) = C ∈ C T and ∀t ∈ C, b(x)(t) = b(x 1 )(t) i f t ∈ tags(b(x 1 )) else b(x 2 )(t)}
The set of tags of x is the union of the tags of x 1 and x 2 . The value taken by x is that of x 1 at any tag when x 1 is present. Otherwise, it takes the value of x 2 at its tags, which do not belong to the tags of x 1 .

The Coq expression is given as follows.

Record T S d e f a u l t {G} ( s s 1 s 2 : T s i g n a l G ) : Prop : = { TSD0 : ∀ t v , t v a l s t v → ( t v a l s 1 t v ∨ t n v a l s 1 t ∧ t v a l s 2 t v ) ; TSD1 : ∀ t v , t v a l s 1 t v → t v a l s t v ; TSD2 : ∀ t v , t n v a l s 1 t → t v a l s 2 t v → t v a l s t v } .

Finally, we apply these semantics rules to a SIGNAL process, to get a complete semantics of the process, that is Tprocess (defined in Section 4.2). Tassignment, Tdelay, Twhen and Tdefault, used to construct the corresponding Tprocess on the semantics rule TSassignment, TSdelay, TSwhen and TSdefault respectively, while the function Process2Tprocess is used to combine them as one Tprocess. The semantics of processes composition is defined in Tpar. Property 2 [START_REF] Guernic | Polychrony for system design[END_REF] For all SIGNAL processes, the tagged model semantics is stretch-closed.

Property 1 and Property 2 represent that a SIGNAL process can be used at different time scales because its semantics is closed for the stretch-equivalence relation.

The Proof of the Semantics Equivalence

The trace semantics and the tagged model semantics are very different models, so the equivalence between them (Theorems S2Teq and T2Seq) is established through an intermediate model. The global idea is sketched in Fig. 6.

The intermediate model M is generic and parameterized by: 1) mdom, the domain of M, such as a set of traces, a set of behaviors on a tag structure; 2) mget m x i v, is true in domain m if variable x gets the i th non-absent value v; 3) msync m x 1 x 2 i 1 i 2 , represents whether the variables x 1 and x 2 are synchronized or not at the i th 1 non-absent value and the i th 2 non-absent value respectively.

With these three functions, it is possible to give a semantics of SIGNAL, that is Uprocess(M). The difference between the trace semantics and the intermediate model is that the latter just considers non-absent values, while the difference between the tagged model semantics and the intermediate model is that the latter uses a totally ordered set to express logical time. In other words, the intermediate model mixes the features of both the trace semantics and the tagged model semantics. Here, Uprocess(M) is just a general expression, because the domain is unknown. However, we give a general mapping between two intermediate models (M1toM2), and give a basic theorem to prove the equivalence between them (Theorem TFR12).

The trace semantics and the tagged model semantics are considered as instances of the intermediate model, so we transform them to their instance and prove the equivalence (Theorems Ssem_def1, Ssem_def2, Tsem_def1 and T-sem_def2).

Finally, we consider the relation between the two instances. The mapping M1toM2 is refined as m_str2tag and m_tag2str, and the Theorem TFR12 is reused. Secondly, we define a semantics of SIGNAL using this model, which is a predicate over m ∈ mdom. Here, signal variables x, x 1 , . . . , x n are used both in the mathematical model and the Coq expressions.

Intermediate Model 1 (Instantaneous function) The intermediate model of the instantaneous function is defined as follows:

x := f (x 1 , • • • , x n ) (m) = -∀i ∈ N, ∀v 1 • • • v n v ∈ V, mget m x 1 i v 1 ∧ mget m x 2 i v 2 ∧ • • • ∧ mget m x n i v n ∧ mget m x i v ⇒ v = f (v 1 , . . . , v n ) -∀i ∈ N, msync m x 1 x i i ∧ msync m x 2 x i i ∧ . . .
Prop : = { Uass_T : ∀ d v i , ( ∀ p , mget m ( vp p ) i ( d p ) ) → mget m x i v → v = f d ; Uass_S : ∀ p i , msync m ( vp p ) x i i } .
Intermediate Model 2 (Delay) The intermediate model of the delay construct is defined as follows:

x := x 1 $ init c (m) = -mget m x 0 c -∀i ∈ N, ∀v 1 v 2 ∈ V, mget m x 1 i v 1 ∧ mget m x 1 (i + 1) v 2 ⇒ mget m x (i + 1) v 1 -∀i ∈ N, msync m x x 1 i i
The two signals x and x 1 are synchronous. mget m x 0 c represents the first non-absent value of x is the initial value c, and the (i + 1) th non-absent value of x is the i th non-absent value of x 1 , provided it has an (i + 1) th value.

The Coq expression is given as follows.

Intermediate Model 3 (Undersampling)

The intermediate model of the undersampling construct is defined as follows:

x := x 1 when x 2 (m) = -∀i ∈ N, ∀v ∈ V, mget m x i v ⇒ (∃i 1 i 2 ∈ N, msync m x x 1 i i 1 ∧ msync m x x 2 i i 2 ∧ mget m x 1 i 1 v ∧ mget m x 2 i 2 true) -∀i 1 i 2 ∈ N, ∀v ∈ V, msync m x 1 x 2 i 1 i 2 ∧ mget m x 1 i 1 v ∧ mget m x 2 i 2 true ⇒ (∃i ∈ N, msync m x x 1 i i 1 ∧ mget m x i v)
Here, x is defined in the position i if and only if there are two synchronized positions i 1 and i 2 at which x 1 and x 2 are defined, and such as the value of x 2 is true. In such a case, the i th non-absent value of x is the i th 1 non-absent value of x 1 . The Coq expression is given as follows.

Record Uwhen {M} (m: mdom M) x x1 x2 :

Prop : = { Uwhen_v : ∀ i v , mget m x i v → ∃ i 1 i 2 , msync m x x1 i i 1 ∧ msync m x x2 i i 2 ∧ mget m x1 i 1 v ∧ ∃ b , mget m x2 i 2 b ∧ i s T r u e b ; Uwhen_v12 : ∀ i 1 i 2 b v , msync m x1 x2 i 1 i 2 → mget m x1 i 1 v → mget m x2 i 2 b → i s T r u e b → ∃ i , msync m x x1 i i 1 ∧ mget m x i v } .

Intermediate Model 4 (Deterministic merging)

The intermediate model of the deterministic merging construct is defined as follows:

x := x 1 de f ault x 2 (m) = -∀i ∈ N, ∀v ∈ V, mget m x i v ⇒ ((∃i 1 ∈ N, msync m x x 1 i i 1 ∧ mget m x 1 i 1 v)∨ (¬(∃i 1 ∈ N, msync m x x 1 i i 1 )∧ (∃i 2 ∈ N, msync m x x 2 i i 2 ∧ mget m x 2 i 2 v))) -∀i i 1 ∈ N, ∀v ∈ V, msync m x x 1 i i 1 ∧ mget m x 1 i 1 v ⇒ mget m x i v -∀i i 2 ∈ N, ∀v ∈ V, (¬(∃i 1 ∈ N, msync m x x 1 i i 1 ) ∧ msync m x x 2 i i 2 ∧ mget m x 2 i 2 v ⇒ mget m x i v
Here, either the i th position of x is synchronized with some position of x 1 , or else it is synchronized with some position of x 2 . In both cases, the value of x at the i th position is the value of the synchronized one.

The Coq expression is given as follows.

Record U d e f a u l t {M} (m: mdom M) x x1 x2 :

Prop : = { U d e f a u l t _ v : ∀ i v , mget m x i v → ( ( ∃ i 1 , msync m x x1 i i 1 ∧ mget m x1 i 1 v ) ∨ ( ¬ ( ∃ i 1 , msync m x x1 i i 1 ) ∧ ∃ i 2 , msync m x x2 i i 2 ∧ mget m x2 i 2 v ) ) ; U d e f a u l t _ v 1 : ∀ i i 1 v , msync m x x1 i i 1 → mget m x1 i 1 v → mget m x i v ; U d e f a u l t _ v 2 : ∀ i i 2 v , ( ¬ ( ∃ i 1 , msync m x x1 i i 1 ) → msync m x x2 i i 2 → mget m x2 i 2 v → mget m x i v } .
In addition, we apply these semantics rules to a process to get a complete semantics, that is Uprocess. We also give the semantics of processes composition. Thirdly, we give a general mapping between two intermediate models (M1toM2). We use a function s1tos2 to express the mapping from a set of elements of the domain of M 1 (denoted as S 1 ) to a set of elements of the domain of M 2 . It relies on a function m2tom1 mapping one element of the domain of M 2 to one element of the domain of M 1 , such as from one trace to one behavior on a tag structure.

s1tos2(S 1 ) = {e 2 ∈ mdom(M 2 )|m2tom1(e 2 ) ∈ S 1 }
get12 and sync12 define the properties of m2tom1, i.e., the same variable of two models has the same value at the same value index (same mget), and has the same synchronous relations (same msync).

Record M1toM2 M1 M2: Type : = { m2tom1 : mdom M2 → mdom M1; g e t 1 2 : ∀ m2 x i v , mget m2 x i v ↔ mget ( m2tom1 m2 ) x i v ; s y n c 1 2 : ∀ m2 x1 x2 i 1 i 2 , msync m2 x1 x2 i 1 i 2 ↔ msync ( m2tom1 m2 ) x1 x2 i 1 i 2 ; s 1 t o s 2 : ( mdom M1 → Prop ) → ( mdom M2 → Prop ) := f u n s 1 ⇒ f u n e2 ⇒ s 1 ( m2tom1 e2 ) } .
Moreover, a basic theorem in which two intermediate models are equivalent is proven. This theorem states that the transformation of the M 2 semantics of a SIGNAL process p is the M 1 semantics of p. The predicate trGet tr i x v is satisfied if the i th non-absent value of x is v.

I n d u c t i v e t r G e t : T r a c e → n a t → XVar → V a l u e → Prop := t r g 0 : ∀ x s t t r v , s t x = Val v → t r G e t ( Tr s t t r ) 0 x v | t r g U : ∀ i x s t t r v , s t x = Absence → t r G e t t r i x v → t r G e t ( Tr s t t r ) i x v | t r g N : ∀ i x s t t r v , s t x Absence → t r G e t t r i x v → t r G e t ( Tr s t t r ) ( S i ) x v .

In order to define trSync, we introduce the auxiliary predicate trGetp. trGetp tr i x j is satisfied if the i th non-absent value of x is at the instant j of the trace tr.

I n d u c t i v e t r G e t p : T r a c e → n a t → XVar → n a t → Prop := t r g p 0 : ∀ x s t t r , s t x Absence → t r G e t p ( Tr s t t r ) 0 x 0 | t r g p U : ∀ i x s t t r j , s t x = Absence → t r G e t p t r i x j → t r G e t p ( Tr s t t r ) i x ( S j ) | t r g p N : ∀ i x s t t r j , s t x Absence → t r G e t p t r i x j → t r G e t p ( Tr s t t r ) ( S i ) x ( S j ) .

Then, we say that x 1 and x 2 synchronize at value index i 1 and i 2 if the i th 1 non-absent value of x 1 and the i th 2 non-absent value of x 2 occur at the same instant.

D e f i n i t i o n t r S y n c x1 x2 ( t r : T r a c e ) ( i 1 i 2 : n a t )

: Prop := ∀ j , t r G e t p t r i 1 x1 j ↔ t r G e t p t r i 2 x2 j .

We construct the corresponding intermediate model instance using the observers trGet and trSync. D e f i n i t i o n s t r I n s t a n c e : Model := { | mdom:= T r a c e ; mget t r x i v := t r G e t t r i x v ; msync t r x1 x2 i 1 i 2 := t r S y n c x1 x2 t r i 1 i 2 | } .

Finally, we prove the equivalence between the trace semantics and its corresponding intermediate model instance. Here, we set the domain as a behavior on a tag structure. The observers mget and msync are refined as tGet and tSync.

In order to define tGet and tSync, we introduce the auxiliary predicates tGett_from and tGett. tGett s i t is satisfied if the i th tag of the signal s is t. Then, we say that x 1 and x 2 synchronize at tag index i 1 and i 2 if they share the same tag. We construct the corresponding intermediate model instance using the observers tGet and tSync.

I n d u c t i v e t G

Example 8

We construct the intermediate model instance of the tag structure G1 shown in the example 6 (see Fig. 8). We refine the definition of mapping (M1toM2) as m_str2tag and m_tag2str. In other words, m_str2tag and m_tag2str are defined as instances of M1toM2.

In m_str2tag, the function m2tom1, i.e., from a behavior on a tag structure to a trace, is constructed by a mathematical transformation (transformation 1) which is close to the topological sort algorithm [START_REF] Cormen | Introduction to algorithms[END_REF], and it is used in the definition of the function s1tos2, i.e., from the set of traces to a set of behaviors. Transformation 1 Let us consider the mapping from a behavior on a tag structure to a trace. It must visit the tags of each signal following their chain order and must be fair(all the tags of all the signals must be eventually visited). For that, we use a variant of topological sort algorithm and the finiteness of the set signal variables.

• Step0: consider the first tag of each signal, i.e., the tag index on each signal is 0, denoted as the vector of tag indexes:

                 0 0 . . . 0                  .
• Step1: select any signal such as:

-no other signal will synchronize in the strict future with its current position.

-it has a minimal index compared to indexes of such signals.

• Step2: get the current tag of the chosen signal.

• Step3: add to the target trace the values of the signal variables for that tag, while the values of other signals variables are noted ⊥. • Step4: increment the index of all the signals of which current tag is the chosen tag, namely their tag index will be added 1, for example

                 1 0 . . . 0                  .
• Step5: repeat step1, step2, step3 and step4.

The transformation stops if there does not exist any variables with an associated tag at its current tag index. In this case, the resulting trace is finite. Otherwise, the transformation builds an infinite trace.

Example 9 According to transformation 1, the tag structure G1 in the example 6 can be mapped to a set of traces (different arrangement of values), and the trace tr1 shown in the example 5 belongs to this set (see Fig. 9). The tag index on each signal is noted on the tag structure explicitly. The transitions of the vector of tag indexes of tr1 and tr2 are given respectively as follows.

0 0 → 1 0 → 1 1 → 2 1 → 2 2 → 3 3 → 4 3 → 4 4 → 5 4 → 5 5 → 6 5 → 6 6 → ∅ 0 0 → 1 0 → 2 0 → 2 1 → 2 2 → 3 3 → 4 3 → 4 4 → 5 4 → 5 5 → 6 5 → 6 6 → ∅
In m_tag2str, the function m2tom1, i.e., from a trace to a behavior on a tag structure, is constructed by another mathematical transformation (transformation 2), and it is used in the definition of the function s1tos2, i.e., from a set of behaviors to a set of traces. In order to map the infinite traces on the tag structure, we must suppose that infinite chains exist, one of these chains will be chosen to map all the traces. So, we have the following hypothesis.

Hypothesis 1 A tag structure always has at least an infinite chain.

The Coq definition is given as follows. Finally, each signal variable will get a sub-chain. Example 10 According to transformation 2, the trace tr1 shown in the example 5 is mapped to an infinite chain with non-absent values, which has the same observers tGet and tSync with the tag structure G1 in the example 6 (see Fig. 10). In the direction from the trace semantics to the tagged model semantics, we can get a corresponding tag structure using the mapping Sprocess2Tprocess, that is Spro-cess2Tprocess G (Process2Sprocess p), then we prove it is equivalent with the tagged model semantics Pro-cess2Tprocess, namely, they have the same observers tGet and tSync. In the direction from the tagged model semantics to the trace semantics, we can get a corresponding trace using the mapping Tprocess2Sprocess, that is Tprocess2Sprocess G (Process2Tprocess G p), then we prove it is equivalent with the trace semantics Process2Sprocess, namely, they have the same observers trGet and trSync.

Discussion

As mentioned before, the observers mget and msync are used in the equivalence between two different semantic models. Moreover, local signal variables are ignored in the formal development to get a simplest criterion for comparing models. Here, we discuss the possible properties of mget and msync on the same semantics model, either on the trace semantics or on the tagged model semantics.

Remark 2

The SIGNAL semantics is not closed for mget/msync equivalence when the SIGNAL programs have local declarations, as explained in the following example. The trace model is considered here. Similarly, we just consider the external visible signals. We give two traces having the same observers mget and msync. However, tr1 belongs to the trace semantics of Sampler, while tr2 does not. The initial value of the local variable y is true, so x1 should always get values at first.

x1 1 ⊥ 1 ⊥ 1 ⊥ • • • tr1 : x2 ⊥ 2 ⊥ 2 ⊥ 2 • • • x1 ⊥ 1 ⊥ 1 ⊥ 1 • • • tr2 : x2 2 ⊥ 2 ⊥ 2 ⊥ • • • Remark 3
The SIGNAL semantics is closed for mget/msync equivalence when the SIGNAL programs don't have local declarations, because the semantic constraints are expressed only through mget and msync.

So, we should not confuse the property of the observers mget and msync with the property of stretch closure.

Related Work

The formal semantics of the SIGNAL language has a longtime research, and the contributors describe the semantics using different models. The reference manual of SIGNAL V4 [START_REF] Besnard | SIGNAL V4 Reference Manual[END_REF] gives the definitions of event and trace, and defines the trace semantics. The trace model is a convenient one to be comprehended, so it is always used to interpret the basic concepts of SIGNAL [START_REF] Gamatié | Designing embedded systems with the SIGNAL programming language[END_REF][START_REF] Guernic | Data-flow to von neumann: the signal approach[END_REF][START_REF] Houssais | The synchronous programming language signal-a tutorial[END_REF]. Lee and Sangiovanni-Vincentelli proposes the tagged-signal model [START_REF] Lee | A framework for comparing models of computation[END_REF] to compare various models of computation, such as Kahn process networks, sequential processes, data flow, event structures, etc. It is a denotational approach where a system is modeled as a set of behaviors. Behaviors are set of events and each event is a value-tag pair. [START_REF] Gamatié | Designing embedded systems with the SIGNAL programming language[END_REF] and [START_REF] Guernic | Polychrony for system design[END_REF] refine the definitions of event, chain, behavior on tags, and give the tagged model semantics of SIGNAL. [START_REF] Benveniste | Composing heterogeneous reactive systems[END_REF] introduces an algebra of tag structures, which is a variation of the tagged-signal model, to define parallel composition of heterogeneous reactive systems formally. Morphisms between tag structures can be used to represent design transformations from tightly-synchronized specifications to loosely-synchronized implementation architectures such as loosely time triggered architecture (LTTA) and globally asynchronous locally synchronous (GALS). In [START_REF] Gamatié | Designing embedded systems with the SIGNAL programming language[END_REF], they also give a structured operational semantics of SIGNAL through an inductive definition of the set of possible transitions. [START_REF] Pnueli | Tanslation validation[END_REF] proposes a synchronous transition systems (STS) model to present the operational semantics of SIGNAL, and presents the translation validation method to verify the compiler from SIGNAL to sequential C-code. [START_REF] Benveniste | Compositionality in dataflow synchronous languages: specification distributed code generation[END_REF] defines the properties of endochrony and isochrony on the STS semantics model, to guarantee correct-by-construction deployment from the synchronous programs to GALS.

Meanwhile, there are some work about mechanization of the semantics of the synchronous languages. Nowak proposes a co-inductive semantics for modeling SIGNAL in the Coq proof assistant [START_REF] Nowak | Co-inductive axiomatization of a synchronous language[END_REF][START_REF] Kerboeuf | Specification and verification of a stream-boiler with signal-coq[END_REF]. In [START_REF] Boulmé | Certifying synchrony for free[END_REF], a semantics of Lucid-Synchrone, an extension of LUSTRE with higherorder stream functions, is given in Coq. [START_REF] Schneider | Proving the equivalence of microstep and macrostep semantics[END_REF] specifies the semantics of QUARTZ in HOL, and proves the equivalence between different semantics.

However, there has been little research about the equivalence between different semantics of SIGNAL. [START_REF] Nowak | Co-inductive axiomatization of a synchronous language[END_REF] defines a translation scheme of the trace semantics of SIGNAL to the logical framework of Coq, but they don't consider the semantics equivalence, the stretch-closure property is also excluded. They conduct some case studies to apply the approach SIGNAL-Coq, such as the steam-boiler problem [START_REF] Kerboeuf | Specification and verification of a stream-boiler with signal-coq[END_REF], and the correctness of an implementation of SIGNAL protocol for LTTA [START_REF] Kerboeuf | Formal proof of a polychronous protocol for loosely time-triggerd architectures[END_REF].

Conclusion and Future Work

In this paper, we have studied the equivalence between two denotational semantics of SIGNAL, the trace semantics and the tagged model semantics. The former is easier to be comprehended, so it is often used to explain the basic concepts of SIGNAL. However, the latter can represent the multi-clock and distributed features more naturally. These two semantics have several different definitions respectively. We select appropriate ones as the reference paper semantics and mechanize them in the Coq platform. The distance between these two semantics discourages a direct proof of equivalence. Instead, we have transformed them to an intermediate model, which mixes the features of both the trace semantics and the tagged model semantics. Thus we have established the existence of a bijection between the trace and the tagged semantics domain such that the trace semantics of SIGNAL can be obtained from its tagged model semantics and vice versa. We prove the equivalence between the SIGNAL semantics by in-troducing two observers mget and msync, which introduces an equivalence relation weaker than the stretching relation. A feedback from our formal development, besides stretchequivalence, the SIGNAL semantics satisfies the mget/msync equivalence if the SIGNAL programs don't have local declarations.

In the future, we plan to consider the local declarations in the intermediate model. Furthermore, we can use this framework to compare the definitions of SIGNAL properties such as endochrony, isochrony defined on variants of semantics models or on the syntax.

The synchronous hypothesis simplifies system specification and verification, however, the problem of deriving a correct physical implementation from it does remain. In particular, the target architecture has a distributed feature, such as multi-core systems. In order to exploit the emerging multicore processors, thanks to the theory of weakly endochronous systems [START_REF] Potop-Butucaru | Concurrency in synchronous systems[END_REF], there are several research to synthesize multithreaded code from the synchronous specifications [START_REF] Jose | Formal model driven software synthesis for embedded systems[END_REF][START_REF] Papailiopoulou | From design-time concurrency to effective implementation parallelism: the multi-clock reactive case[END_REF]. However, one needs to prove the semantics preservation from the SIGNAL specifications to the multi-threaded code. The results of this paper will be useful for this challenging problem.

  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 inclusion relation between the clocks of signals x 1 and x 2 , the statement x 1 ˆ> x 2 specifies a set containment relation between the clocks of signals x 1 and x 2 .

I

  n d u c t i v e EValue : Type := Val : V a l u e → EValue | Absence : EValue .

  C o I n d u c t i v e T r a c e : Type := Tr : ( XVar → EValue ) → T r a c e → T r a c e .

Fig. 1

 1 Fig. 1 Stretching of a trace following f

Fig. 2 A

 2 Fig. 2 A tag structure with events

Fig. 4

 4 Fig. 4 Stretching of a behavior composed of two signals following f

  I n d u c t i v e b t a g s {G} ( b : T b e h a v i o r G) ( dom : XVar → Prop ) t : Prop := b t a g s P r f : ∀ x , dom x → t a g s t ( b x ) → b t a g s b dom t .

Definition 15 (

 15 Stretch Equivalence) For a given domain X ⊆ X, two behaviors b 1 and b 2 are stretch-equivalent, noted b 1 ≷ b 2 , iff there exists another behavior b 3 less stretched than both b 1 and b 2 , i.e., b 1 ≷ b 2 iff ∃b 3 b 3 ≤ B |X b 1 and b 3 ≤ B |X b 2 .

  I n d u c t i v e t S t r e t c h _ E q u i v a l e n c e {G1 G2 :TAG} ( b1 : T b e h a v i o r G1 ) ( b2 : T b e h a v i o r G2 ) ( dom : XVar → Prop ) : Prop := t S t r E q : ∀ G3 ( b3 : T b e h a v i o r G3 ) , t S t r e t c h i n g b3 b1 dom → t S t r e t c h i n g b3 b2 dom → t S t r e t c h _ E q u i v a l e n c e b1 b2 dom . Definition 16 (Stretch Closure) For a given behavior b, the set of all behaviors that are stretch-equivalent to b, defines its stretch closure, noted b*. The stretch closure of a set of behaviors B |X includes all the behaviors resulting from the stretch closure of each behavior b ∈ B |X , i.e., b∈B |X b * .

  I n d u c t i v e t S t r e t c h _ C l o s u r e {G :TAG} ( t b : T b e h a v i o r G → Prop ) ( dom : XVar → Prop ) : T b e h a v i o r G → Prop := t S t r e t c h _ c l : ∀ b1 b2 , t b b1 → t S t r e t c h _ E q u i v a l e n c e b1 b2 dom → t S t r e t c h _ C l o s u r e t b dom b2 . Definition 17 (Stretch-Closed) A SIGNAL process is stretch-closed, iff, for all b ′ ∈ T process.tbehaviors and for all b ∈ B |X , b ≷ b ′ ⇒ b ∈ T process.tbehaviors

  C o I n d u c t i v e S d e l a y x x1 c : T r a c e → Prop := SdelayU : ∀ s t t r , s t x1 = Absence → s t x = Absence → S d e l a y x x1 c t r → S d e l a y x x1 c ( Tr s t t r ) | S d e l a y P : ∀ s t v t r , s t x1 = Val v → s t x = Val c → S d e l a y x x1 v t r → S d e l a y x x1 c ( Tr s t t r ) .

C o I n d u c t i v e

  Swhen ( x x1 x2 : XVar ) : T r a c e→Prop := SwhenT : ∀ s t v b t r , i s T r u e b → s t x = Val v → s t x1 = Val v → s t x2 = Val b → Swhen x x1 x2 t r → Swhen x x1 x2 ( Tr s t t r ) | SwhenF : ∀ s t b t r , ¬ i s T r u e b → s t x = Absence → s t x2 = Val b → Swhen x x1 x2 t r → Swhen x x1 x2 ( Tr s t t r ) | SwhenU : ∀ s t t r , s t x = Absence → s t x2 = Absence → Swhen x x1 x2 t r → Swhen x x1 x2 ( Tr s t t r ) .

  C o I n d u c t i v e S d e f a u l t ( x x1 x2 : Var ) : T r a c e→Prop := S d e f a u l t U : ∀ s t t r , s t x = Absence → s t x1 = Absence → s t x2 = Absence → S d e f a u l t x x1 x2 t r → S d e f a u l t x x1 x2 ( Tr s t t r ) | S d e f a u l t 1 : ∀ s t v t r , s t x = Val v → s t x1 = Val v → S d e f a u l t x x1 x2 t r → S d e f a u l t x x1 x2 ( Tr s t t r ) | S d e f a u l t 2 : ∀ s t v t r , s t x = Val v → s t x1 = Absence → s t x2 = Val v → S d e f a u l t x x1 x2 t r → S d e f a u l t x x1 x2 ( Tr s t t r ) .

Example 5

 5 x I n d f x i := { | sdom y := y=x ∨ ∃ i , y= x i i ; s t r a c e s t r := S a s s i g n m e n t x I n d f x i t r | } . Program D e f i n i t i o n S P d e l a y x x1 c := { | sdom y := y=x ∨ y=x1 ; s t r a c e s t r := S d e l a y x x1 c t r | } . Program D e f i n i t i o n SPwhen x x1 x2 := { | sdom y := y=x ∨ y=x1 ∨ y=x2 ; s t r a c e s t r := Swhen x x1 x2 t r | } . Program D e f i n i t i o n S P d e f a u l t x x1 x2 := { | sdom y := y=x ∨ y=x1 ∨ y=x2 ; s t r a c e s t r := S d e f a u l t x x1 x2 t r | } . Program D e f i n i t i o n SPprod p1 p2 := { | sdom y := sdom p1 y ∨ sdom p2 y ; s t r a c e s t r := s t r a c e s p1 t r ∧ s t r a c e s p2 t r | } .F i x p o i n t P r o c e s s 2 S p r o c e s s ( p : P r o c e s s ) : S p r o c e s s := match p w i t h P a s s I n d f x x i ⇒ S P a s s i g n m e n t x I n d f x i | Pwhen x x1 x2 ⇒ SPwhen x x1 x2 | P d e l a y x x1 c ⇒ S P d e l a y x x1 c | P d e f a u l t x x1 x2 ⇒ S P d e f a u l t x x1 x2 | P p a r p1 p2 ⇒ SPprod ( P r o c e s s 2 S p r o c e s s p1 ) ( P r o c e s s 2 S p r o c e s s p2 ) end . The trace semantics of the process Parallel-Count (example 2) is a set of traces, and two possible traces are given as follows. Here, we just consider the external visible signals (the local declarations are hidden).

  )} The semantics of the instantaneous function is the set of behaviors b. The tags of each signal involved in b represent the same chain C, i.e., all the signals are synchronous. When the signals are all present, at each tag of C, the output signal gets the corresponding value. The corresponding Coq expression is given as follows. T-SA_T is used to express the relation between values, while TSA_S represents all the signals are synchronous. tval_from and tval represent that, given a signal of a tag structure G and a tag of the signal, we can get the corresponding value. tsync means two signals are synchronous.

D

  e f i n i t i o n T a s s i g n m e n t {G} x I n d e x ( f : ( I n d e x → V a l u e ) → V a l u e ) ( x i : I n d e x → XVar ) : T p r o c e s s G:= { | tdom y := y=x ∨ ∃ i , y= x i i ; t b e h a v i o r s b := T S a s s i g n m e n t ( b x ) I n d e x f ( f u n i ⇒ ( b ( x i i ) ) ) | } . D e f i n i t i o n T d e l a y {G} ( x x1 : XVar ) c : T p r o c e s s G:= { | tdom y := y=x ∨ y=x1 ; t b e h a v i o r s b := T S d e l a y ( b x ) ( b x1 ) c | } . D e f i n i t i o n Twhen {G} x x1 x2 : T p r o c e s s G:= { | tdom y := y=x ∨ y=x1 ∨ y=x2 ; t b e h a v i o r s b := TSwhen ( b x ) ( b x1 ) ( b x2 ) | } . D e f i n i t i o n T d e f a u l t {G} x x1 x2 : T p r o c e s s G:= { | tdom y := y=x ∨ y=x1 ∨ y=x2 ; t b e h a v i o r s b := T S d e f a u l t ( b x ) ( b x1 ) ( b x2 ) | } . D e f i n i t i o n T p a r {G} ( p1 p2 : T p r o c e s s G) : = { | tdom y := tdom p1 y ∨ tdom p2 y ; t b e h a v i o r s b := t b e h a v i o r s p1 b ∧ t b e h a v i o r s p2 b | } .

FExample 6

 6 i x p o i n t P r o c e s s 2 T p r o c e s s G ( p : P r o c e s s ) : T p r o c e s s G:= match p w i t h P a s s I n d f x x i ⇒ T a s s i g n m e n t x I n d f x i | P d e l a y x x1 c ⇒ T d e l a y x x1 c | Pwhen x x1 x2 ⇒ Twhen x x1 x2 | P d e f a u l t x x1 x2 ⇒ T d e f a u l t x x1 x2 | P p a r p1 p2 ⇒ T p a r ( P r o c e s s 2 T p r o c e s s G p1 ) ( P r o c e s s 2 T p r o c e s s G p2 ) end . The tagged model semantics of the process ParallelCount (example 2) is a set of behaviors, and two examples are shown in Fig.5. Similarly, we just consider the external visible signals.

Fig. 5

 5 Fig. 5 The tag structures of two possible behaviors of the process Parallel-Count

Fig. 6

 6 Fig. 6 Proof's plan

6. 1

 1 Intermediate Model Firstly, we give the definition of the intermediate model. mdom represents the domain of the model. In this model, we introduce two observers, mget which gives the (finite or infinite) sequence of values taken by each variable, and msync which defines the synchronization points of any couples of variables. Record Model : Type : = { mdom : Type ; mget : mdom → XVar → n a t → V a l u e → Prop ; msync : mdom → XVar → XVar → n a t → n a t → Prop } .

  ∧ msync m x n x i i All signals are synchronous and the i th non-absent values of each signal satisfy the functional constant v = f (v 1 , . . . , v n ). The Coq expression is given as follows, Uass_T represents the relation between values and Uass_S means all signals are synchronous. Record U a s s i g n m e n t {M} (m: mdom M) I n d e x ( f : ( I n d e x → V a l u e ) → V a l u e ) ( x : XVar ) ( vp : I n d e x → XVar ) :

Record U d e

  l a y {M} (m: mdom M) x x1 c : Prop : = { U d e l a y _ 0 : ∀ v , mget m x 0 v → v=c ; Udelay_S : ∀ v1 v2 i , mget m x1 i v1 → mget m x1 ( S i ) v2 → mget m x ( S i ) v1 ; U d e l a y _ s : ∀ i , msync m x x1 i i } .

F

  i x p o i n t U p r o c e s s {M} ( p : P r o c e s s ) (m: mdom M) : Prop := match p w i t h P a s s I n d f x x i ⇒ U a s s i g n m e n t m I n d f x x i | P d e l a y x x1 c ⇒ U d e l a y m x x1 c | Pwhen x x1 x2 ⇒ Uwhen m x x1 x2 | P d e f a u l t x x1 x2 ⇒ U d e f a u l t m x x1 x2 | P p a r p1 p2 ⇒ U p r o c e s s p1 m ∧ U p r o c e s s p2 m end .

  Theorem TFR12 : ∀ M1 M2 ( p : P r o c e s s ) ( t 1 2 : M1toM2 M1 M2) , ∀ ( m2 : mdom M2) , U p r o c e s s (M:=M2) p m2 ↔ s 1 t o s 2 t 1 2 ( U p r o c e s s (M:=M1) p ) m2 . 6.2 The Relation between the Trace Semantics and the Intermediate Model Notice that, the semantics defined by intermediate model (Uprocess) is generic, because mget and msync are abstract observers. Here, we focus on the relation between the trace semantics and the intermediate model, so we set the domain as a trace. The observers mget and msync also need to be refined, that are trGet and trSync.

TheoremExample 7

 7 Ssem_def1 : ∀ p t r , s t r a c e s ( P r o c e s s 2 S p r o c e s s p ) t r → U p r o c e s s (M:= s t r I n s t a n c e ) p t r . Theorem Ssem_def2 : ∀ p t r , U p r o c e s s (M:= s t r I n s t a n c e ) p t r → s t r a c e s ( P r o c e s s 2 S p r o c e s s p ) t r . We construct the intermediate model instance of the trace tr1 shown in the example 5 (see Fig.7).

Fig. 7

 7 Fig. 7 The intermediate model instance of a trace

I

  n d u c t i v e t S y n c {G} x1 x2 ( b : T b e h a v i o r G) i 1 i 2 : Prop := t S y n c P r f : ( ∀ t , t G e t t ( b x1 ) i 1 t ↔ t G e t t ( b x2 ) i 2 t ) → t S y n c x1 x2 b i 1 i 2 .

  D e f i n i t i o n t a g I n s t a n c e G : Model := { | mdom:= T b e h a v i o r G; mget b x i v := t G e t ( b x ) i v ; msync b x1 x2 i 1 i 2 := t S y n c x1 x2 b i 1 i 2 | } . Finally, we prove the equivalence between the tagged model semantics and its corresponding intermediate model instance. Theorem Tsem_def1 : ∀ G p b , t b e h a v i o r s ( P r o c e s s 2 T p r o c e s s G p ) b → U p r o c e s s (M:= t a g I n s t a n c e G) p b . Theorem Tsem_def2 : ∀ G p b , U p r o c e s s (M:= t a g I n s t a n c e G) p b → t b e h a v i o r s ( P r o c e s s 2 T p r o c e s s G p ) b .

Fig. 8

 8 Fig. 8 The intermediate model instance of a tag structure

  Lemma m _ s t r 2 t a g : ∀ G, M1toM2 s t r I n s t a n c e ( t a g I n s t a n c e G ) . D e f i n i t i o n S p r o c e s s 2 T p r o c e s s G ( p : S p r o c e s s ) : = { | tdom := sdom p ; t b e h a v i o r s := s 1 t o s 2 ( m _ s t r 2 t a g G ) ( s t r a c e s p ) | } .

Fig. 9

 9 Fig. 9 Mapping from a tag structure to a trace

  Lemma m _ t a g 2 s t r : ∀ G, M1toM2 ( t a g I n s t a n c e G) s t r I n s t a n c e . D e f i n i t i o n T p r o c e s s 2 S p r o c e s s G ( p : T p r o c e s s G) : = { | sdom := tdom p ; s t r a c e s := s 1 t o s 2 ( m _ t a g 2 s t r G ) ( t b e h a v i o r s p ) | } .

  C o I n d u c t i v e h a s I n f i n i t e C h a i n F r o m {G} ( t : Tag G ) : Type := NextTag : ∀ t 1 , t @< t 1 → h a s I n f i n i t e C h a i n F r o m t 1 → h a s I n f i n i t e C h a i n F r o m t . I n d u c t i v e h a s I n f i n i t e C h a i n G : Type := F i r s t T a g : ∀ ( t : Tag G) , h a s I n f i n i t e C h a i n F r o m t → h a s I n f i n i t e C h a i n G . H y p o t h e s i s i n f c h : ∀ G, h a s I n f i n i t e C h a i n G . Transformation 2 Let us consider the mapping from a trace to a behavior on a tag structure. An infinite chain of the target tag structure is noted by the tags {t i | i = 0, 1, • • • } which correspond to instants ( j = 0, 1, • • • ) of the trace. • Step0: start from the first instant of the trace, find the first position which has non-absent value, if the position cannot be found, then return an empty chain. • Step1: note the variable-value pair on the corresponding tag of the infinite chain. • Step2: from the current position, find the next position which has non-absent value, if the position cannot be found, then return the chain which is ended at the current position. • Step3: repeat Step1 and Step2.

Fig. 10

 10 Fig. 10 Mapping from a trace to a tag structure

Record

  TPeq {G:TAG} ( p1 p2 : T p r o c e s s G ) : Type : = { TPd : ∀ y : XVar , tdom p1 y ↔ tdom p2 y ; TPb : ∀ ( b1 : T b e h a v i o r G ) ( b2 : T b e h a v i o r G) , ( ∀ y , b1 y = b2 y ) → ( t b e h a v i o r s p1 b1 ↔ t b e h a v i o r s p2 b2 ) } . Theorem S2Teq : ∀ G ( p : P r o c e s s ) , TPeq ( S p r o c e s s 2 T p r o c e s s G ( P r o c e s s 2 S p r o c e s s p ) ) ( P r o c e s s 2 T p r o c e s s G p ) .

Record

  SPeq ( p1 p2 : S p r o c e s s ) : Prop := { SPd : ∀ y , sdom p1 y ↔ sdom p2 y ; SPs : ∀ t r , s t r a c e s p1 t r ↔ s t r a c e s p2 t r } . Theorem T2Seq : ∀ G ( p : P r o c e s s ) , SPeq ( T p r o c e s s 2 S p r o c e s s G ( P r o c e s s 2 T p r o c e s s G p ) ) ( P r o c e s s 2 S p r o c e s s p ) .

Example 11

 11 Let us consider another process Sampler: process S ampler = (! integer x1, x2; ) (| y := not y $ init true | x1 := 1 when y | x2 := 2 when not y |) where boolean y; end;

  Dr. Zhibin YANG received his PhD degree in Computer Science from Bei-Hang University, Beijing, China in February 2012 . Since April 2012, he has been a Postdoc in IRIT of University of Toulouse, France. His research interests include safety-critical real-time system, formal verification, AADL, synchronous languages. Dr. Jean-Paul BODEVEIX received a PhD of Computer Science from the University of Paris-Sud 11 in 1989. He has been assistant professor at University of Toulouse III since 1989 and is now Professor of computer science since 2003. His main research interests concern formal specifications, automated and assisted verification of protocols as well as of proof environments. 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.

  the signals are either all present or all absent, i.e., they are synchronous, denoted as s ˆ= s 1 ˆ= • • • = s n . s τ gets the value of f (s 1τ , . . . , s nτ ) when the signals are all present. The function f includes different mathematical operations, such as arithmetic operations, boolean operations, etc.The corresponding Coq expression is given as follows.

	→ s t x=Val ( f v )
	→ S a s s i g n m e n t x I n d e x f x i t r
	→ S a s s i g n m e n t x I n d e x f x i ( Tr s t t r ) .

C o I n d u c t i v e S a s s i g n m e n t x I n d e x ( f : ( I n d e x → V a l u e ) → V a l u e ) ( x i : I n d e x → Var ) : T r a c e → Prop := SassU : ∀ s t t r , ( ∀ i , s t ( x i i ) = Absence ) → s t x = Absence → S a s s i g n m e n t x I n d e x f x i t r → S a s s i g n m e n t x I n d e x f x i ( Tr s t t r ) | S a s s P : ∀ v s t t r , ( ∀ i , s t ( x i i ) = Val ( v i ) )

  The predicate tGet s i v is satisfied if the value on the i th tag of the signal s is v.

	I n d u c t i v e t G e t {G} s i v : Prop :=
	t G e t _ p r f : ∀ t : Tag G, t G e t t s i t
	→ t v a l s t v → t G e t s i v .
	e t t _ f r o m {G} ( t 0 : Tag G ) :
	T s i g n a l _ f r o m t 0 → n a t → Tag G → Prop :=
	t g t n 0 : ∀ t 1 h d s t , t = t 1
	→ t G e t t _ f r o m t 0 ( T n e x t t 0 t 1 h d s ) 0 t
	| t g t n S : ∀ t 1 h d s i t ,
	t G e t t _ f r o m t 1 s i t →
	t G e t t _ f r o m t 0 ( T n e x t t 0 t 1 h d s ) ( S i ) t .
	I n d u c t i v e t G e t t {G} : T s i g n a l G → n a t
	→ Tag G → Prop :=
	t g t 0 : ∀ d t s , t G e t t ( Tfrom G t d s ) 0 t
	| t g t S : ∀ t 0 d s i t , t G e t t _ f r o m t 0 s i t →
	t G e t t ( Tfrom G t 0 d s ) ( S i ) t .

Acknowledgements This work was supported in part by the National Natural Science Foundation of China under Grant 61073013 and Grant 61003017, the Aviation Science Foundation of China under Grant 2012ZC51025, the TOPCASED Project, and the RTRA STAE Foundation in France.


F Pistolesi

R Shekhter

Tunable spin-polaron state in a singly clamped semiconducting carbon nanotube

Keywords: numbers: 85.85.+j, 71.38.-k, 85.75.-d

de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Nanoelectromechanics with suspended carbon nanotubes evolved rapidly in last few years [1][2][3][4][5][6][7]. Recently I. Snyman and Yu.V. Nazarov [8] considered a semiconducting CNT laying on an insulating substrate with one end of it suspended. A metallic gate below both the insulating substrate and the suspended part of the CNT generates an homogeneous electric field (cf. Fig. 1 of Ref. [8]). The mechanical bending of the suspended part of the nanotube induces then a spatial inhomogeneity of the electrostatic potential along the CNT forming a minimum at the deformable end of the wire. The competition between such an electrostatic bending with both the elastic potential of the CNT and the quantum rigidity of the electronic wave function makes the mechanical bending as well as the formation of the localized polaronic state at the movable end of the CNT to occur as a first order phase transition as a function of the electric field. The estimate for the critical field for a realistic experimental set up was predicted in Ref. [8] to be 0.01 V/µm.

An impressive effort of the nanoelectronics community is currently deployed to manipulate and exploit the electronic spin degrees of freedom in transport devices (spintronics) [9]. In this context the possibility of magnetic gating, i.e. the use of ferromagnetic leads inducing magnetic exchange fields E ex /µ B (with µ B the Bohr magneton) on the electronic spin is currently actively investigated [10][11][12][13]. More surprisingly such exchange fields can have remarkable consequences also on the dynamics of a nano-mechanical system for which dynamical (shuttle) instabilities, strong spin-polarized currents, and cooling have been predicted [14][15][16] In this paper we show that the system discussed by Snyman and Nazarov [8] in presence of a magnetic dielectric substrate allows the formation of a localized fully polarized polaronic state. The experimentally observed exchange energy E ex (see Ref. [13,14]) turns out to be as large as tens of Kelvins, thus being of the same order of magnitude of the localization energy for an electron in a CNT on the scale of the micrometer. This allows for a high tunability of the polaronic state by means of two electric gates, below the suspended and non-suspended

M C eE y(x) x E V G1 L V G2 U -(x) eV E exc E exc U + (x) U (x) y(x) 0 U -(x)=U + (x)
FIG. 1. Schematic of the system considered: a CNT laying on a magnetic substrate (C) and protruding out of a length L. Two independently adjustable gates (VG1 and VG2) are shown and a contact (C) on the substrate side. The potential for spin up and down (U+ and U-) is also sketched above.

part of the CNT (see Fig. 1). As a result a continous electrostatic tuning of the localization length and the bound state energy can be achieved, forming a stability diagram of spin-up and spin-down polaronic states. Detection of the state of the system can be envisaged by use of a nearby single-electron transistor, for which the CNT tip acts as a gate [17]. Fully electric manipulation of the mechanical and electronic spin state of the CNT is thus possible in this system.

The system. Following Ref. [8] let us consider a CNT laying on a substrate with a suspended part protruding out of a length L (see Fig. 1). In Ref. [8] it has been shown that the wavefunction ψ(x) of the electrons in the valence band of the CNT can be describled by a standard one-dimensional Schroedinger equation with an effective mass m * = 0.6m e a 0 /r, where m e is the electronic mass, a 0 the Bohr radius, and r the radius of the CNT. The variable x parametrizes the position along the CNT, its value is 0 at the edge of the substrate and L on the tip of the suspended part. The length of the CNT on the substrate is supposed to be L, and is taken infinity for simplicity. Then vanishing boundary conditions apply at x = L and x = -∞. As in Ref. [8] the CNT can bend with a displacement y(x) (for 0 < x < L) in the direction orthogonal to the substrate. The elastic energy cost reads IY dx [y (x)]

2 /2, where I = 6.4πa 0 r 2 is the second moment of area of the tube cross section and Y the CNT Young modulus (of the order of 1.2 TPa). Single clamping implies that y(0) = y (0) = 0 and y (L) = y (L) = 0. In this paper we will restrain to the classical description of the deflection. The tip of the CNT on the substrate is in tunneling contact with a metal whose chemical potential can be tuned close to the valence band of the CNT by adjusting the electric potential. Up to now the description followed closely Ref. [8]. We introduce now the main difference: We will assume that the substrate is a magnetic insulator that induces an exchange interaction term -E ex 0 -∞ dxσ|ψ σ (x)| 2 for the electrons being in the CNT over the substrate (x < 0). The variable σ indicates the spin projection in the z direction. This creates a spin-dependent potential so that the spin-up electrons (σ = +) are attracted in the x < 0 region. In order to tune the potential we assume that two different gates are present, one below the magnetic substrate and an other one under the suspended part. By changing independently the potentials on the two gates it is possible to modify the electrostatic potential V and the electric field E acting on the electrons on the suspended part (taking the non-suspended region as a reference for the potential, cf. Fig. 1). We can then write the full Hamiltonian for the problem as follows (θ x is the Heaviside function):

H = σ L -∞ dx 2 2m * |∂ x ψ σ (x)| 2 + IY 2 ∂ 2 x y(x) 2 -(E ex σθ -x + eV θ x -eEy(x)) |ψ σ (x)| 2 . ( 1
)
The first term in Eq. ( 1) gives the quantum kinetic energy, the second the elastic energy, and the third is a sum of three parts: the exchange energy, the electrostatic potential and its variation induced by the deflection [y(x)] of the CNT. In Ref. [8], for V = 0 and for E ex = 0, it has been shown that it exists a critical value of the electric field E c for which the ground state is an electronic localized state on the CNT suspended part. The formation of the bound state is a first order transition: the CNT starts to bend only for E > E c and a metastable bound state exists for E c1 < E < E c . At E = E c the localization length is thus finite and typically much shorter than L. In order to have a tunable bound state it is necessary to have a smooth transition from the delocalized to the localized state. This is actually the typical case in quantum mechanics, by decreasing the depth of a potential well that allows a bound state one can delocalize progressively the wave function. The bound-state radius then diverges at the threshold for its appearance. We will thus see that the presence of V and E ex allows to create a spin-dependent tunable bound state, that is associated to a displacement of the CNT tip. Electronic problem. Let us begin with the purely electronic problem [y(x) ≡ 0 for all x]. The ground state can be found by solving the Schroedinger equation:

- 2 ∂ 2 x 2m * -E ex σθ -x -eV θ x ψ σ (x) = σ ψ σ (x) (2)
for each spin projection. The presence of a bound state is signaled by the existance of a solution of Eq. ( 2) with σ < -σE ex the bottom of the relative band. Taking σ < -σE ex as a reference in energy the problem for each spin species reduces to that describled by Eq. ( 2) with E ex → 0 and eV → eV -σE ex = U . The solution can then be found by matching the wave function ψ(x) = Ae κx for x < 0 with ψ(x) = Be ikx + Ce -ikx for x > 0 at x = 0 asking the continuity of the wave function and of its derivative. The boundary conditions lead to the eigenvalue equation

e -2ikL = -(ik + κ)/(ik -κ) with κL = [-2m * b / 2 ] 1/2 , kL = [2m * (U + b )/ 2 ]
1/2 and b < 0 the bound state energy. At the threshold b → 0 -, thus there κ vanishes and the eigenvalue equation reduces to e -2ikL = -1. This gives kL = π/2 and the threshold value for the potential

U t = (π/2) 2 E K , with E K = 2 /(2m * L 2 ) the kinetic energy scale. For U - U t E K the localization length κ -1 = 2LE K /(U -U t )
and diverges as anticipated. By changing U it is then possible to adjust the spread of the wave function on the magnetic substrate. Since the two spin species feel a different potential only on the substrate, this allows to change continuously the energy difference of the up and down bound states. The bound state energy for each spin state reads:

σ = -σE ex + b (eV -σE ex ) (3)
with the threshold value for V : eV σ = U t + σE ex . A typical picture of the eV dependence of the two bound states for E = 0 is shown dashed in Fig. 2. For V -< V < V + a unique bound state exists for spin down. Let's define V c the value for which the down-spin energy crosses the up-spin bottom band:

-(V = V c ) = -E ex . For V + < V < V c
two bound states exist, but only the lowest one (spin up) is stable, since the spin-down lays above the bottom of the spin-up band, and any spin-flip perturbation allows its decay into the spin-up continuum. Finally for V > V c two stable bound states exist. Their energy splitting has a maximum at V c and then monotonically decreases as a function of V . This is due to the reduction of the localization length reducing the effect of the exchange interaction that acts only for x < 0. Although both spin-up and spin-down polaronic states are stable at V > V c only one of them can be occupied due to the Coulomb blockade, whose repulsion energy turns out to be much larger than the polaronic bound state energy (∼ E K ) at L 1 nm. This fact allows the formation of a controllable single-electron fully spin polarized state at the protruding part of the CNT. Nanomechanical effects. We now consider how the system behaves when we let the CNT bend. It is not possible any more to find the ground state energy analytically, we will thus follow closely the variational method used in Ref. [8] to which we refer for more details. We introduce the dimensionless variables z = x/L, h = H/E K , f = yY I/eEL 3 , φ σ = ψ σ √ L, and the coupling parameter α = (eE) 2 L 3 /(Y IE K ). The problem can then be completely determined by giving only three independent coupling parameters: α, µ = E ex /E K , and ν = eV /E K . The functional to be minimized reads:

0 1 2 3 4 5 -1.0 -0.5 0.0 0.5 eV/ E K ϵ b / E K V - V + π 2
h = 1 -∞ dz φ σ 2 + α f φ 2 σ + f 2 2 -(µσθ -z + νθ z ) φ 2 σ .
(4) By writing φ(z) = M n=1 a n (1 -z) n for z > 0 and M n=1 a n z n e κz for z < 0, and f (z) = M n=1 b n z n+1 one can enforce the boundary conditions and minimize numerically the functional in order to find the parameters {a n , b n , κ} and thus the ground state energy σ with explicit expressions for the bending and the wavefunction. The charge accumulated on the suspended part of the CNT in presence of an electric field induces a force that bends the tip of the CNT. The effective electronic potential deepens and bending lowers the bound state energy. In particular it favors a stronger localization of the wave function on the tip (measured by κ -1 ). For E ex = eV = 0 in Ref. [8] it is shown that the bound state forms with a first order phase transition for α > α c = 312.03. In order to keep a smooth transition we will consider the case α < α c and investigate the dependence of the bound state energy and wavefunction on eV /E K for given values of

E ex /E K .
Before considering the results of the numerical calculation it is useful to estimate analytically the typical range of the displacement of the CNT tip induced by the localization of the charge. Let us assume that the fraction n < 1 of an electron charge is accumulated on the CNT tip uniformely. A simple ansatz for the displacement is f (z) = az 2 . It satisfies both the boundary conditions and the Euler equation f = 0. Substituing it in Eq. ( 4) one has for the part proportional to α:

eV/ E K ϵ ± / E K V c ϵ -/ E K ϵ + / E K 3.6 3.
h α = α(2a 2 + n a 3 ) (5)
this functional has a minimum at a = -n/12 = f (1). It gives a rough estimate of the dimensionless displacement of the tip by taking into account only the competition between the electric field and the elastic stiffness. The effect of the other two parameters is hidden into the value of n, that cannot be larger than 1.

We present on Fig. 3 the numerical results for α = 175 and µ = 1. One can see that the energy splitting of the two spin states is of the order of E K = E ex (top-left panel). Defining n σ = 1 0 dzφ 2 σ the fraction of charge (and spin) localized on the suspended part of the CNT one finds that for V = V c both bound states present a finite value of n σ and n --n + ≈ 0.17. The difference is slowly reduced for larger values of the gate voltage. The same can be said for the deflection of the tip of the CNT (f σ = f (1) for each spin state, bottom-left panel). Finally the bottom-right panel shows that the ratio f ± /n ± is actually close to the rough estimate 1/12.

The plots of Fig. 3 show that a particularly important quantity is the value of the physical parameters ( σ , n σ and f σ ) at the threshold V c . The dependence on V is always monotonic and the maximum or minimum values are observed at V c . In view of manipulating the spin state, the value at V c gives thus a very good indication of the range in which the state can be accessible. We thus show in Fig. 4 as a function of α and for different values of µ the threshold V c , the energy splitting --+ , the difference in the occupation n --n + , and in the deflection f --f + . As expected the critical voltage V c decreases as a function of α, and in particular, for sufficiently small µ, it vanishes when α approaches the critical value α c . The bound-state energy splitting is monotone in α, since the electric field increases the localization of the bound state, and thus reduces the difference of the two states. Its αdependence is rather weak. Even for µ 1 the energy splitting remains of the order of E K , that thus sets the main energy scale of the problem. Quite surprisingly the difference in the fraction of localized charge (n --n + ) is not monotonic for small µ as a function of the electric field. This is due to the fact that the transition region is approached at different values of α for each spin state. A similar behavior is observed in f --f + . One can conclude that the optimal value of α to observe a well defined bound state is between 100 and 200.

Estimates. In order now to consider the possibility to observe the two bound states we discuss the typical scales of the problem. Expressing the radius in nm and the length in µm E K ≈ 13.9(r/L 2 ) mK. The typical value of L ranges between 0.1 and 1µm, leading to a range for E K between few K to tens of mK, thus always accessible with standard cryogenics. The thermal and quantum fluctuations of the displacement of the tip plays also an important role, since they define the distinguibility of the displacement of the two bound states. From Eq. ( 5) one can write an approximate potential for the tip displacement δf = f (1) -f 0 (with f 0 = n/12 the equilibrium value): h α = 2α(δf ) 2 . The equipartition theorem then gives for the thermal fluctuations δf T = [k B T /(4αE K )] 1/2 . Quantum fluctuations -δf Q -has the same expression with k B T → ω m . Since ω m /E K = 0.0332 independently of L or r [8,[START_REF] Cleland | Foundations of nanomechanics: from solid-state theory to device applications[END_REF] then δf Q = 0.09/ √ α. Expressing as above T in mK, L in µm, and r in nm δf T = 0.13L[T /(rα)] 1/2 . Those values have to be compared with f --f + that are at best 0.04. f Q is thus 5 times smaller of this value already for α = 100, while in order to keep δf T small one needs T .09rα/L 2 . This is realizable for instance choosing L = .5µm, r = 2nm, α = 200 and working at temperatures T ≈ 20 mK (E K is 111 mK in this case).

Conclusions. We have shown that combining electrostatic and magnetic gating the formation of a spinpolaronic state in a singly clamped CNT becomes possible. Electric, magnetic, and mechanical tuning provides an effective manipulation of such spin-polaron states offering a controllable magneto-electro-mechanical transduction with single electronic charge and spin sensitivity involving sub nanometer mechanical displacement.

FIG. 2 .

 2 FIG.2. Dependence on the gate voltage V of the two spinprojection bound-state energy ( σ ) for Eex/EK = 0.5, α = 0 (i.e. E = 0, dashed) and α = 50 (full line). The bottom of the lower electronic band (spin-up) is shown dotted.

fFIG. 3 .

 3 FIG. 3. For Eex = EK and α = 175 gate voltage dependence of the bound state energies (top-left), fraction of localized charge or spin (top-right), deflection of the tip (bottom-left), and ratio of deflection to localized charge (bottom-right).

1 FIG. 4 .

 14 FIG. 4. The four panels show as a function of α for µ = 0.1, 1., 10, 20 the critical gate voltage value Vc (top left), the energy splitting of the two bound states --+ (top right), the difference in the fraction of localized charge n+ -n-(bottom left), and the difference of the CNT tip deflection f--f+ (bottom-right); the last three quantities calculated at V = Vc.

Acknowledgements R.S. acknowledges financial support from Idex of Univ. Bordeaux through visiting professor program. F.P. acknowledges support from ANR QNM.