Thierry Gautier
email: hierry.gautier@inria.fr

Clément Guy

Alexandre Honorat

Paul Le Guernic

Jean-Pierre Talpin

Loïc Besnard

Polychronous Automata and their Use for Formal Validation of AADL Models

This paper investigates how state diagrams can be best represented in the polychronous model of computation (MoC) and proposes to use this model for code validation of behavior specifications in AADL. In this relational MoC, the basic objects are signals, which are related through dataflow equations. Signals are associated with logical clocks, which provide the capability to describe systems in which components obey to multiple clock rates. We propose a model of finite-state automata, called polychronous automata, which is based on clock relations. A specificity of this model is that an automaton is submitted to clock constraints. This allows one to specify a wide range of control-related configurations, either reactive, or restrictive with respect to their control environment. A semantic model is defined for these polychronous automata, that relies on a Boolean algebra of clocks. Based on a previously defined modeling of AADL software architectures using the polychronous MoC, this model of polychronous automata is used as a formal model for the AADL Behavior Annex. This is illustrated with a case study which specifies an adaptive cruise control system.

Introduction

The design of embedded systems, and more specifically critical systems, requires the satisfaction of strong, various and heterogeneous constraints such as safety, determinism of embedded programs, threaded or distributed implementation, scheduling in a specific or non specific OS, etc. One way to help designers is to provide them with friendly usable tools supported by strong mathematical semantics. These formal models and methods allow to ensure correctness of components used or defined at each level of the design.

The polychronous model of computation [START_REF] Le Guernic | Polychrony for system design[END_REF] is such a formal model. Historically related to the synchronous programming paradigm [START_REF] Benveniste | The synchronous languages twelve years later[END_REF] (Esterel [3], Lustre [START_REF] Halbwachs | The synchronous dataflow programming language LUSTRE[END_REF]), the polychronous model of computation, implemented in the dataflow language Signal [START_REF] Le Guernic | Programming real-time applications with Signal[END_REF][START_REF] Gamatié | Designing Embedded Systems with the SIG-NAL Programming Language[END_REF] and its environment Polychrony 1) , stands apart by the capability to model multi-clocked systems. The synchronous paradigm consists of abstracting the non-functional implementation details of a system and lets one benefit from a focused reasoning on the logics behind the instants at which the system functionalities should be secured. The fundamental notion of polychrony consists in the capability to describe systems in which components obey to multiple clock rates. In particular, the Signal language gives the opportunity to seamlessly model embedded systems at multiple levels of abstraction while reasoning within a simple and formally defined mathematical model. A design approach that may be advocated is to allow for a seamless inter-operation of heterogeneous programming viewpoints within the same host model of computation which is the polychronous model. A typical case study from Airbus, for instance, was based on a co-modeling of the doors management system of the A350 [START_REF] Yu | System-level co-simulation of integrated avionics using Polychrony[END_REF]. In this case study, functionalities were 1) http://polychrony.inria.fr modeled with synchronous Simulink 2) and a system-level model of the hardware equipment was specified in AADL (Architecture Analysis & Design Language) [START_REF]Aerospace Standard AS5506A: Architecture Analysis and Design Language[END_REF]. The Polychrony toolbox was then used to interpret computations and communications specified in both models in order to synthesize schedulers for sequential and distributed simulation. The experiment was successful, since it has demonstrated that the polychronous model, through its supportive language Signal, may be used as an effective common semantic model for representing or interfacing heterogeneous models. However, Signal is based on a dataflow oriented notation, thus there is sometimes some distance between an actual specification, which may use, for instance, state oriented description, and its semantic encoding as systems of equations. This may cause some practical difficulties, in particular when traceability is a requirement, as is the case in most systems.

In this paper, first, we investigate the way state diagrams can be best represented in the polychronous model of computation, maintaining the multi-clock characteristic property of the representation. We propose a model of automata, called polychronous automata, which is based on clock (or event) relations, and allows one to specify a wide range of control-related configurations, more or less permissive (or, dually, more or less restrictive). A semantic model is defined for these polychronous automata, that relies on the Boolean algebra of clocks, and permits to manipulate these automata, without having necessarily to translate them into dataflow equations. In previous works [START_REF] Yu | Exploring system architectures in AADL via Polychrony and SynDEx[END_REF][START_REF] Yu | Polychronous modeling, analysis, verification and simulation for timed software architectures[END_REF], in the aim of virtual prototyping embedded architectures, we defined a compositional semantic translation of AADL specifications into the polychronous model. We now refine this modeling by considering our semantic model of polychronous automata as a formal model for the AADL Behavior Annex.

Our work is motivated by practical reasons such as effective combination of heterogeneous programming notations (including dataflow and automata), and formal validation and virtual prototyping of timed software architectures. Our purpose is not to propose just another extension of an existing programming language. Instead, we focus on the definition of a specific model of automata, specially adapted to the polychronous model of computation, adopted as common semantic model. Such automata have to relate events by expressing and specifying clock relations (or clock constraints) between these events. For the definition of polychronous automata, the Signal 2) http://www.mathworks.com/products/simulink language is used as syntactic support to express clock equations. Simple examples such as alternating events are used in the first sections of this paper as they are sufficient to illustrate the basics of the model.

In the next section, we first consider some related works, both concerning the introduction of models of automata in synchronous languages, and the use of some formal models to represent and validate AADL models. In Section 3, we recall the main operators of the Signal language and their semantics. Then we define in Section 4 the Boolean control algebra which is used to manipulate clock formulas. In Section 5, we describe the refinement of polychronous programs as automata. In Section 6, we highlight different forms of polychronous automata described as equations on signals.

Relying on these requirements in terms of expressivity, we define our model of automata in Section 7. Then, the principles of the semantic translation of AADL in the polychronous model are presented in Section 8. A concrete AADL case study, including behavior specifications as automata, is detailed in Section 9 to illustrate formal validation in this modeling framework. Conclusion and future work are drawn in Section 10.

Related work

Usual automata have been introduced several years ago in dataflow synchronous languages and are used every day in production tools like SCADE [START_REF] Berry | Scade: Synchronous design and validation of embedded control software[END_REF]. More generally, there have been many attempts to combine heterogeneous programming models. A major problem addressed in Ptolemy is the use of heterogeneous mixtures of models of computation [START_REF] Tripakis | A modular formal semantics for Ptolemy[END_REF]. So-called Modal Models in particular are hierarchical models where the top level model consists of a finite-state machine, the states of which are refined into other models, possibly from different domains [START_REF] Lee | Modal models in Ptolemy[END_REF]. In our approach, heterogeneous designs are expressed in terms of a common semantics, which is that of the polychronous model of computation. In the software system Matlab/Simulink, which is largely accepted in the industry, the Stateflow notation [START_REF] Hamon | An operational semantics for Stateflow[END_REF] is used to describe modes in event-driven and continuous systems.

Mode-automata [START_REF] Maraninchi | Mode-automata: a new domain-specific construct for the development of safe critical systems[END_REF] were originally proposed to gather advantages of declarative and imperative approaches to synchronous programming and extend the functional dataflow paradigm of Lustre with the capability to model transition systems. Mode-automata have been combined with stream functions in Lucid Synchrone [START_REF] Colaço | A conservative extension of synchronous data-flow with state machines[END_REF]. Related forms of hierarchical state machines include Statecharts [START_REF] Harel | Statecharts: A visual formalism for complex systems[END_REF] and their variants, including UML state machines [START_REF] Wang | A semantics of UML state-machines using synchronous pre-order transition systems[END_REF], and SyncCharts [START_REF] André | Semantics of SyncCharts[END_REF], associated in particular with Esterel and, more recently, SC-Charts [START_REF] Hanxleden | SCCharts: Sequentially constructive statecharts for safety-critical applications[END_REF], based on an improved definition of (sequential) constructivity [START_REF] Hanxleden | Sequentially constructive concurrency-A conservative extension of the synchronous model of computation[END_REF]. DDFCharts [START_REF] Radojevic | Design of distributed heterogeneous embedded systems in DDFCharts[END_REF], which compose finite-state machines and synchronous dataflow graphs, have multiple clocks; transitions can be driven by different clocks and the instants at which clocks synchronize are seen as a rendez-vous communication.

Our approach may be distinguished from the others by its capability to model multi-clocked systems and to express clock relations through the automata. A first attempt was made a few years ago to define polychronous mode automata [START_REF] Talpin | Polychronous mode automata[END_REF], but compared to our current proposal, it did not allow to manipulate automata as specific objects that can be used, for instance, to specify dynamic properties of events. In its spirit, our approach, which is based on constraint specification relating occurrence of events, is relatively close to that taken for Lutin [START_REF] Raymond | Lutin: a language for specifying and executing reactive scenarios[END_REF], but with a different purpose. In Lutin, statements describe sequences of non deterministic atomic reactions expressing constraints on input/output values. It is used mainly for test sequence specification and generation. In our proposal, constraints relate values and clocks of signals.

Concerning the second contribution of this article, i.e., the use of a formal model (in our case, polychronous automata) to represent and validate AADL behavior specifications, there has been many related works that have contributed to the formal specification, analysis and verification of AADL models and its annexes. We limit ourselves to mentioning here the works which seem to be closest to our approach. In particular, RAMSES [START_REF] Cadoret | Design patterns for rule-based refinement of safety critical embedded systems models[END_REF] presents the implementation of the AADL Behavior Annex. The Behavior Annex supports the specification of automata and sequences of actions to model the behavior of AADL programs and threads. Its implementation OSATE proceeds by model refinement and can be plugged in with Eclipse-compliant backend tools for analysis or verification. For instance, the RAMSES tool uses OSATE to generate C code for OSs complying the ARINC-653 standard.

Synchronous modeling is central in [START_REF] Ölveczky | Formal semantics and analysis of behavioral aadl models in real-time maude[END_REF], which presents a formal real-time rewriting logic semantics for a behavioral subset of the AADL. This semantics can be directly executed in Real-Time Maude and provides a synchronous AADL simulator (as well as LTL model-checking). It is implemented by the tool AADL2MAUDE using OSATE.

Similarly, Yang et al. [START_REF] Yang | Two formal semantics of a subset of the AADL[END_REF] define a formal semantics for an implicitly synchronous subset of the AADL, which includes periodic threads and data port communications. Its operational semantics is formalized as a timed transition system.

This framework is used to prove semantics preservation through model transformations from AADL models to the target verification formalism of timed abstract state machine (TASM).

With respect to related works, we also annex the core AADL and its Behavior Annex with formal semantic frameworks to express executable behaviors and temporal properties, but we endeavour in an effort of structuring and using them together within the framework of a more expressive multi-clocked synchronous model. Polychrony would allow us to gain abstraction from the direct specification of executable, synchronous, specification in the AADL, yet offer services to automate the synthesis of such, locally synchronous, executable specification, together with global asynchrony, when or where ever needed.

The Signal language

We first introduce the Signal language and its semantics, before to formalize its Boolean control algebra, that is the basis for clock calculus. Signal is a declarative language expressed within the polychronous model of computation. The reader is referred to the bibliography of the Signal language for a detailed description (for instance [START_REF] Besnard | Compilation of polychronous data flow equations[END_REF] for an overview, [START_REF] Le Guernic | Programming real-time applications with Signal[END_REF][START_REF] Besnard | SIGNAL V4-INRIA version: Reference Manual[END_REF] for detailed syntax and semantics).

A Signal process defines a set of (partially) synchronized signals as the composition of equations. A signal x is a finite ((∃n ∈ N)(x = (x t ) t∈N,t n ) or infinite (x = (x t ) t∈N ) sequence of typed values in the data domain D x ; the indices in the sequence represent logical discrete time instants. At each instant t, a signal is either present and holds a value v in D x , absent and virtually holds an extra value denoted ⊥, or completed and never holds any actual or virtual value for all instants s such that t s. The set of instants at which a signal x is present is represented by its clock x. Two signals are synchronous iff they have the same clock. Clock constraints result from implicit constraints over signals and explicit constraints over clocks.

The semantics of the full language is deduced from the semantics of a core language, and from the Signal definition of the extended features. A Signal process is either an equation x := f (x 1 , . . . , x n ), where f is a function, or the composition P|Q of two processes P and Q, or the binding P/x of the signal variable x to the process P. In this section, we give a sketch of its functional part using dataflow models.

Semantic domains. For a set of values of some type D, we define its extension D ⊥ = D ∪ {⊥}, where ⊥ D denotes the absence of a signal value. The semantics of Signal is defined as least domain fixed point. For a data domain D, we consider a poset (D ⊥ ∪ {•, #}, ) such that (D ⊥ , ) is flat, i.e., x y ⇒ x = y, for all x, y ∈ D ⊥ (• and # denote respectively the presence of a signal and the absence of information). We denote by D ∞ the set of finite and infinite sequences of "values" in D ⊥ . The empty sequence is denoted by . All n-ary functions f : (D ∞ ) n → D ∞ are defined using the convention of noting s a (possibly empty) signal in D ∞ , v a value in D, x a value in D ⊥ . As usual, |s| is the length of s, s 1 .s 2 is the concatenation of s 1 and s 2 . are stretch-equivalent iff they only differ on non-final empty events (see [START_REF] Le Guernic | Polychrony for system design[END_REF] for more details).

Signal functions. A Signal function is a n-ary (with n > 0) function f that is total, strict and continuous over domains [START_REF] Abramsky | Domain theory[END_REF] (w.r.t. prefix order) and that satisfies:

-stretching: f (⊥.s 1 , . . . , ⊥.s n ) = ⊥. f (s 1 , . . . , s n ) -termination: ((∃i ∈ 1, n)(s i = )) ⇒ f (s 1 , . . . , s n ) =
Stepwise extension. Given n > 0 and a n-ary total function f : D 1 × . . . × D n → D n+1 , the stepwise extension of f (e.g., =, and, +, etc.) denoted F is the synchronous function that satisfies:

-F(v 1 .s 1 , ..., v n .s n ) = f (v 1 , ..., v n ).F(s 1 , ..., s n ) Delay. Function delay: D × D ∞ → D ∞ satisfies: -delay(v 1 , v 2 .s) = v 1 .delay(v 2 , s)
The infix syntax of delay(v 1 , s) is: s $ init v 1 .

Merge. Function default:

D ∞ × D ∞ → D ∞ satisfies: -default(v.s 1 , x.s 2 ) = v.default(s 1 , s 2 ) -default(⊥.s 1 , x.s 2 ) = x.default(s 1 , s 2 )
The infix syntax of default(s 1 , s 2 ) is:

s 1 default s 2 .
Sampling. Let B = {ff , tt} denote the set of Boolean values. Function when:

D ∞ × B ∞ → D ∞ satisfies:
-for b ∈ {⊥, ff }, when(x.s 1 , b.s 2 ) = ⊥.when(s 1 , s 2 )

when(x.s 1 , tt.s 2 ) = x.when(s 1 , s 2 )

The infix syntax of when(s 1 , s 2 ) is: s 1 when s 2 .

Process. An equation is a pair (x, E) denoted x := E. An equation x := E associates with the variable x the sequence resulting from the evaluation of the Signal function f denoted by E (defined as a composition of functions). If A = {x 1 , ..., x n } (x A) is the set of the free variables in E, the equation x := E denotes a process on A, i.e., a set of behaviors on A ∪ {x}; a process is closed by stretch-equivalence (thanks to the stretching rule).

The parallel composition of equations defines a process by a network of strict continuous functions connected by signal names. Composition of processes is associative, commutative and idempotent. When it satisfies the Kahn conditions (no cycle, single assignment. . . ), it then is a strict continuous function or Kahn Process Network (KPN) [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF], defined as least upper bound satisfying the equations. It further satisfies the termination and stretching properties (it is closed for the stretching relation). It may or may not be synchronous. In the semantics of Signal [START_REF] Le Guernic | Polychrony for system design[END_REF], a process is the set of infinite behaviors accepted by the above "KPN semantics".

A process with feedback or local variables may be not time-deterministic. The semantics of a non deterministic process can be defined using Plotkin's power-domain construction [START_REF] Plotkin | A powerdomain construction[END_REF]. The input-free equation x := x $ init 0 is a typical example of not timely deterministic process: x holds a sequence of constant value 0 separated by an undetermined number of silent transitions, characterized by an occurrence of ⊥.

An example of non deterministic process is the equation x ::= E, that defines x to be equal to E when E is present and undefined when E is ⊥ (partial definition). This equation is a shortcut for x := E default x. A signal x can be constructively defined by several equations x ::= E1, . . . , x ::= En in a process, provided that for every pair of equations x ::= Ei, x ::= Ej, when Ei and Ej are both present, they hold the same value. If E1, . . . , En do not recursively refer to x and if they denote functions, then (x ::= E1|...|x ::= En) is a deterministic process.

Partial definitions are very useful in automata where the function that computes the value of a signal often depends on current state. The states being exclusive, the consistency property is satisfied. Partial definitions are used also to define state variables the elements of which are present as frequently as necessary. When such a state variable is not explicitly defined, it keeps its previous value.

Derived operators.

The following notations (which are derived operators) are used to manipulate clocks, represented as signals of type event, always true if and only if present.

• null clock ˆ0 (never present)

• signal clock ˆx, defined by x = x (present, and true, when x is present) Note that, in the syntax, the hat notation appears just before the symbol or variable it applies to: for instance, "ˆ*" is a syntactic representation of " * " (see below).

• selection ~b (a.
A synchronized memory y := x cell c init x0 is defined by the composition of y := x default (y $ init x0) and y ˆ= x ˆ+ [c]. It defines y with the most recent value of x when x is present or c is present and true. Finally, the Signal term ll :: P associates the label ll with the process P; a label ll is a signal of type event. Its clock is the tick of the labeled process, P (i.e., the upper bound of all the clocks in P).

Boolean control algebra

We define the syntax and set the axioms of the Boolean control algebra, taking into account state variables used to represent states of the automata.

Definition 1 Considering V a (possibly empty) countable set of signal variables, S a non empty finite set of state variables with S ∩V = ∅, a Boolean control algebra Φ(V, S ) is a tuple (F V,S , * , +, -, ¬, 0, 1 V ), where:

• * , + designate meet (infimum) and join (supremum); • 0, 1 V are the minimum and maximum.

The set of control Boolean formulas F V,S is the smallest set that satisfies:

• constants 0, 1 V ∈ F V,S ; • atoms ∀x ∈ V ∪ S , x, x ∈ F V,S ; • unary expressions ∀ f ∈ F V,S , ¬ f ∈ F V,S ; • binary expressions ∀ f, g ∈ F V,S , + f g, * f g, -f g ∈ F V,S .
Parentheses and infix notations can be used in the formulas.

The formula x designates the clock of a variable x. The formulas satisfy Boolean axioms: (F V,S , * , +, ¬, 0, 1 V ) is a Boolean algebra. The following supplementary axioms are also considered.

• difference f -g = f * ¬g; • partition ∀x ∈ V ∪ S , x = x + ¬ x and x * ¬ x = 0; • exclusion ∀s1, s2 ∈ S , s1 * s2 = 0 or s1 = s2; • 1 ∅ = 0.
The clock of an automaton with a non-empty V is defined by x∈V ( x + ¬ x) = 1 V , and ∀s ∈ S , s = 1 V . Formulas in the Boolean control algebra have normal forms: Shannon disjunctive forms (given an arbitrary total order on variables).

Note that, independently of state variables which are distinguished here, this Boolean control algebra is that of the standard polychronous model of computation. The formal tools which are based on this control algebra, such as the clock calculus (which builds a clock hierarchy), still apply exactly in the same way when automata are considered. In both contexts, timing analysis mainly refers to analyzing clock relations based on clock hierarchy.

Clock hierarchy. The clock hierarchy of a process is a component of its Data Control Graph (DCG). The DCG is made of a multigraph G and a clock system Σ. We refer to [START_REF] Besnard | Compilation of polychronous data flow equations[END_REF] for a more complete description. A clock equation is a class of equivalent clock formulas. The clock system Σ is a forest (set of trees) of clock equations: this is why it is called clock hierarchy. The equational nature of the Signal language is a fundamental characteristic that makes it possible to consider the compilation of programs as an endomorphism over Signal programs. We have mentioned a few properties allowing to rewrite programs with rules such as commutativity and associativity of parallel composition.

More generally, until the very final steps of code generation (when code generation is an objective), the compilation process may be seen as a sequence of morphisms allowing to rewrite programs as transformed Signal programs. The final steps (C code generation for instance) are simple morphisms over the transformed Signal programs. These transformation steps, to sequential, clustered, or distributed code generation, are described in [START_REF] Besnard | Compilation of polychronous data flow equations[END_REF].

Refinement of processes as automata

So far, contrary to what is done for other synchronous languages, including dataflow ones like Lustre (see for instance [START_REF] Halbwachs | Generating efficient code from data-flow programs[END_REF]), no explicit representation of automata was directly produced in the compilation of Signal programs, either for code generation purpose, or as input to formal verification tools. In this section, we propose a method for deriving an automaton from a polychronous program, which relies heavily on the concept of clock.

A given Signal program may be seen as an automaton which contains one single state and one single transition, labeled by a clock. This clock is the upper bound of all the clocks of the program (the tick of the program).

The construction of a refined automaton from a Signal program will be based on delayed signals, viewed as state variables (in particular Boolean ones). A state of the automaton is a Signal program with some valuation of its state variables. Transitions are labeled by clocks, which represent the events that fire these transitions. The principle of the construction consists in dividing a given state according to the possible values of a state variable (i.e., true and false for Boolean state variables, which are considered here) in order to get two states, and thus two new Signal programs. Each one of these two states is obtained using a rewriting of the starting program. Moreover, the absence of value for the state variable (which can be considered as another possible value) is taken into account in the clocks labeling the transitions. The construction of the automaton is a hierarchic process.

Figure 1 illustrates the first step of the construction. Initially, the automaton A has one single state, which is the Signal program P, with one transition, labeled by the tick k of P. The construction is started with the valuation of a first state variable, s, in the program P, respectively with true and false, which gives two new programs, P 1 and P 2 . The new programs are obtained by rewriting the previous one, taking into account the considered valuation. This rewriting results

P P

1 P 2 k ¬ s k -¬ s s k -s Figure 1 Refinement of state s in P by the automaton A 1 = (P 1 , P 2 )
generally in simplifications of the programs. The resulting automaton, A 1 , now contains two states, P 1 and P 2 . The calculus of the transitions consists in computing the clocks of the events that cause a change of state. The transition from P 1 to P 2 occurs when the state variable s, which was true, becomes false; thus the corresponding clock is ¬ s. Conversely, the transition from P 2 to P 1 occurs at the clock s. The transition from P 1 to itself is labeled by the clock k, minus the instants at which there is a transition from P 1 to P 2 (and the same reasoning for P 2 ). Note that the transitions are not instantaneous. When a clock raising a change of state is present at a given instant, the effective change of state of the automaton takes place at the following instant (with respect to the tick).

The construction of the automaton is an iterative process, by successive valuation of its state variables, s 1 , s 2 , etc. For instance, the second step would introduce new states, P 11 and P 12 from P 1 , by discriminating it according to the value of a second variable s 2 . One could, equivalently, introduce two other states from P 2 . Now, at any refinement step n > 1, one could then potentially define 2 n states by iterating the refinement of all sub-processes P n-1 i , of clocks k n-1 i and indices 0 < i 2 n-1 obtained from step n -1, by partitioning them according to an nth state variable s n and by using the same mechanism, Figure 2. This would seem to be an expensive construction, at least in the worst case, in the size of the explicit automaton being an exponential of its number of state variables. Fortunately, however, all Signal programs have a clock hierarchy, defined from the dominance relation introduced in Section 4, which is used to represent the control flow of the program in a much more efficient way (and actually optimal, as hierarchies can be normalised and admit a canonical representation). Concretely, most of the 2 n are in practice inaccessible, because of dominance (of a state value by a clock).

P n i1 P n i2 ¬ s n k n-1 i -¬ s n s n k n-1 i -s n
Example. Let's for instance consider a Signal program with two state variables s 1 and s 2 such that s 2 is not defined when s 1 is false, i.e., s 2 ˆ= when s 1 . In other words, s 1 has a higher frequency than s 2 , and in the built clock hierarchy, the clock of s 1 dominates s 2 . If we construct its automaton as in figure 2, evaluating s 1 first, s 2 second, we would obtain four sub-processes P 2 11,12,21,22 from P 1 1 and P 1 2 . However, partitioning P 1 2 into P 2 21,22 is useless, since s 2 is not present when s 1 is false.

It may further be observed that, when constructing the automaton, the order in which state variables are valuated has an influence on the number of states of the automaton. Our choice is to therefore base this order on the clock hierarchy of the Signal program, using a pre-order depth-first traversal. In this way, more frequent state variables are evaluated before less frequent ones. Note also that when some state variable is valuated, the corresponding program is rewritten, using in particular constant propagation. This results generally in many simplifications, since a number of clocks may become null, thus eliminating corresponding variables.

Automaton description in Signal equations

Of particular interest from the previous example is that, in the polychronous framework, the behavior of an automaton may be either reactive, with respect to its environment or context, or restrictive: constrained by clock relations. In the case of a reactive automaton, events from the environment are free to occur at their own rate. The automaton registers the occurrences of these events and makes its state evolve according to these occurrences. In the case of a restrictive automaton, the automaton enforces constraints on the events that can occur. Events that are not explicitly allowed in some state are forbidden: this has an effect on the environment which is, in some way controlled by the automaton. This can be illustrated on an automaton alternating two events, a and b. In Signal, the observer will be implemented using a couple of equations that monitor alternation using a state variable change and stuttering using another wait. A resettable Esterel program like the famous ABRO is an object which falls in between constrained and reactive behaviors: it emits an output o immediately after receiving both inputs a and b. It is reset when r occurs. So, signal o is controlled, while others aren't. In the ABRO program, the inputs a, b, r are never controlled, and the output o is obviously controlled. However, in Signal, it is worth noting that controlled variables are not limited to output signals.

Explicit structure of polychronous automata

Although it is always possible to represent automata by systems of equations, equations are clearly not always the most natural way to represent them. Moreover, in a model-driven engineering context, it is better suited to explicitly represent user-specified and automatically generated automata to maintain high-level semantic properties as well as the traceability of model transformations.

We have hence chosen light-weight syntactic extensions to the Signal language in order to introduce explicit representations of automata.

We add a new syntactic category of process, called automaton. In such an automaton process, labeled processes represent states, and generic processes such as Transition are used to represent the automaton features. Usual equations can be used in these automaton processes to specify constraints or to define computations. Then comes the question of whether these automata should be only a syntactic structure (in such a way that they would be systematically translated as ordinary equations on signals when compiled), or whether they should be reflected in the polychronous formal model itself. This latter choice has the advantage of allowing a formal manipulation of automata (which may be, or not, translated as equations). For instance, it may be the case that a given behavior is best abstracted as an interface automaton than as a system of clock equations which would require to make explicit some hidden Boolean variables. It is therefore desirable to define a model of "polychronous automata" allowing a possible smooth integration within the polychronous model.

A basic statement for the definition of our automata is that state change takes time. It is also assumed in [START_REF] Maraninchi | Mode-automata: a new domain-specific construct for the development of safe critical systems[END_REF], [START_REF] Colaço | A conservative extension of synchronous data-flow with state machines[END_REF], or in SCADE 6. In this way, there is a single state at each logical instant and there is no immediate transition. Such automata should be used to schedule steps, not actions in a step. This drives towards simplicity and is also suitable for high-level mode modeling in an application.

In the polychronous framework, transitions will be labeled by clock (or event) expressions named triggers and a state is implicitly exited on the upper bound of its triggers. An automaton is clocked: it is controllable by an external clock, its control clock. There are several possible interpretations of a given automaton: in a permissive view, all non forbidden events are allowed in states; while in a restrictive one, all non allowed events are forbidden in states. By default, we adopt the permissive hypothesis.

Notations for polychronous automata

To make things concrete, let us write a syntactic representation of the automaton in Fig. 6. This simple automaton has two external events, a and b, and its control clock is, implicitly, the upper bound, a ˆ+ b of the clocks of its inputs. The two states, S1 and S2, are designated by labels, associated here with empty processes. The statement Never (a ˆ* b) represents the constraint of the automaton. This constraint, which must always be respected, can be expressed by a clock formula that is constrained to be null: here, a ˆ* b ˆ= ˆ0, expressed as Never (a ˆ* b). Such constraints can always be expressed as a conjunction of Never formulas (which can also be specified as one single Never statement with several parameters) or of explicit synchronizations like Synchro (x, y) (with Synchro (x, y) defined as Never (x ˆy, y ˆx)). In this small automaton with two states and two explicit transitions, the initial state is S1. We will see below that there are also implicit transitions.

Let us state some vocabulary and notations. For a transition T = Transition (S1, S2, h), S1 is the source of T, S2 is the target of T, h is the trigger of T, denoted trig-ger(T), and a trigger in S1; h is a clock expression, that may represent, for instance, a conjunction of events (e.g., a ˆ* b represents the conjunction of events a and b). The transition A step is defined as being an implicit not exiting reflexive (e.g. stuttering) transition. A step S1--h->>S1 is enabled at k iff (k ˆ* h) is not null, current state is S1 and there is no enabled transition. All steps that are not explicitly forbidden are allowed. In the example of Fig. 6, S1 --bˆ-a ->> S1 and S2 --aˆ-b ->> S2 are steps (they appear as dotted transitions). Steps allow for "stuttering" when there is no enabled transition. For a state S, exiting on (one of the) enabled transitions is mandatory. A formal model of constrained automata, consistent with the polychronous framework, is proposed in the next section.

T is enabled at k iff (k ˆ* h) is not null

Formal definition

For an automaton A of signal variables V A and states S A , we denote by F A,S the set of normal form formulas in the Boolean control algebra Φ(V A , S A ) (cf. Section 4).

Definition 2 A polychronous automaton A is an epsilon-free automaton defined up to isomorphism (over states) as a tuple A = (S A , s 0 , R A ,V A , T A , C A ) where:

• S A is the non empty finite set of states;

• s 0 is the initial state;

• R A ⊂ S A × S A is the transition relation;

• V A is the, possibly empty, finite set of signal variables;

• T A : (R A ) → F A,S is the function that assigns a formula to a transition;

• C A is the constraint of A: it is a formula in F A,S that is (constrained to be) null (thus a formula f in F A,S is null in A iff f * C A = f ).
Remarks. A transition in T A carries a formula in the Boolean control algebra that represents its trigger. Polychronous automata are subject to clock constraints C A which are expressed by a formula in the Boolean control algebra. If C A is 0, then the automaton is constraint-free; if C A is 1 V A (i.e., the supremum of the algebra is constrained to be null), all formulas are null. The notation 1 A is used to denote the supremum

1 V A .
An automaton with an empty set of transitions is O V = ({s}, s, ∅, V, ∅, 1 V ), which blocks all occurrences of all variables of V. The automaton with an empty set of variables is

I = I ∅ = ({s}, s, ∅, ∅, ∅, 0); it is equal to O ∅ = ({s}, s, ∅, ∅, ∅, 1 ∅ ).
Example. The automaton in Fig. 6

is defined by

A = (S A , s 0 , R A , V A , T A , C A ) with • S A : {S 1 , S 2 } • s 0 : S 1 • R A : {(S 1 , S 2 ), (S 2 , S 1 )} • V A : {a, b} • T A : (S 1 , S 2 ) → a, (S 2 , S 1 ) → b • C A : a * b + ¬ a + ¬ b
(a, b are events thus ¬ a, ¬ b should be null).

A labeled transition is denoted by "h : s 1 R A s 2 " meaning that ((s 1 , s 2 ) ∈ R A and T A ((s 1 , s 2 )) = h).

Properties

Now notions introduced previously can be formalized:

• The control clock of an automaton A is 1 A (= x∈V A ( x)), the supremum of the clocks of its variables. • In h : s 1 R A s 2 , h is the trigger of (s 1 , s 2 ) and a trigger in s 1 .

• The trigger of a state s, trigger A (s), is the upper bound of the triggers of (s, * ), where (s, * ) stands for all the transitions outgoing from s.

Then it is possible to define the stuttering clock of a state as the clock difference between the control clock of the automaton and the trigger of the state (plus the null clock of the state, C A (s) = s * C A ): the stuttering clock of a state s is τ(s) = 1 A -(C A (s) + trigger A (s)). Hence the definition of implicit transitions: when the stuttering clock τ(s) of a state s is not null, there is a silent implicit transition τ(s) : sR A s named step. Usual properties of automata can be easily extended to polychronous automata:

• A state t is n-reachable in A iff s 0 and t are not null and either n = 0 and t = s 0 , n > 0 and t is (n -1)-reachable in A, n > 0 and (∃s (n -1)-reachable in A) (∃h)(h * s not null)(h : sR A t).

• A state t is reachable in A iff it is |S A |-reachable in A.
• A state s is deterministic if the triggers of its transitions are mutually exclusive: formally, s is determin-istic iff (∀((s, s 1 ), (s, s 2 )) ∈ R A × R A )((s 1 = s 2 ) ∨ (T A ((s, s 1 )) * T A ((s, s 2 )) = 0)). • An automaton is deterministic iff all its reachable states are deterministic.

• A state s is total (or reactive) iff τ(s) + (Σ (s,t) ∈ R A (trigger A ((s, t)))) = 1 A .
• An automaton is total (or reactive) iff all its states are total (we observe that if C A is not 0 then A is not reactive).

Polychronous automata algebra

Just like the synchronous composition, the composition (or synchronous product) of polychronous automata corresponds to the conjunction of the behaviors specified by each of them.

Definition 3 Let A = (S A , s 0 , R A , V A , T A , C A ) and B = (S B , t 0 , R B ,V B , T B , C B )
two polychronous automata, their composition is defined by AB = A|B = (S AB , (s 0 , t 0 ), R AB ,V AB , T AB , C AB ), where:

• S AB = S A × S B , • R AB = {((s 1 , t 1 ), (s 2 , t 2 )) | ((s 1 , s 2 ), (t 1 , t 2 )) ∈ R A × R B }, • V AB = V A ∪ V B , • (∀ st = ((s 1 , t 1 ), (s 2 , t 2 )) ∈ R AB ) (T AB (st) = T AB ((s 1 , t 1 )) * T AB ((s 2 , t 2 ))), • C AB = C A + C B .
Note that the constraint of the composed automaton (its null formula C AB ) is defined by the clock union of the constraints of the operand automata.

Theorem 1 The composition of polychronous constrained automata has the following properties:

• if A is deterministic, A|A = A, it is idempotent; • it is commutative;
• it has a neutral element I = ({s}, s, ∅, ∅, ∅, 0); • it is associative.

Idempotence for deterministic automata can be proved using induction on n-reachability of states. Associativity can be proved by induction on n-prefix automata (the states of a nprefix automaton of an automaton A are the n-reachable states of A). Associativity corresponds to context independence and commutativity to order independence.

Discussion

The added value provided by the formal model of the polychronous automata is to allow for a smooth integration of automata into the polychronous model of computation of the Signal dataflow language. They have not necessarily to be translated by systems of equations on signals, although such a translation is, of course, possible. Note that using such a translation, semantics of polychronous automata reduce to semantics of standard polychronous programs. Comparable translations have been studied in previous works, such as [START_REF] Colaço | A conservative extension of synchronous data-flow with state machines[END_REF] for example (it is not our purpose here to describe another translation that would not be so different). We have defined a parallel composition (synchronous composition) of polychronous automata. A classical extension of finite automata is also that of hierarchical automata, in which states may be non atomic. Here, this can be handled quite simply in the context of the Signal language. It is not detailed in this article since it does not present new challenges with respect to previous works.

Just like labels are syntactically associated with states, labels can also be associated with transitions, and these labels can be used as clocks. The label of a transition is an event signal (a clock), which is true (present) when this transition is fired. Actions associated with an automaton can be expressed as polychronous equations (in our case, in Signal), that are composed with the constraints of the automaton. They may use specific events associated with the automaton, such as labels of transitions, but also other typical events such as entering or exiting a given state, etc. For example, let t1 and t2 be labels associated with two transitions in a given automaton, then the equation o := t1 ˆ+ t2 expresses the action of emitting an event o as soon as one of these transitions is fired.

A further remark can be made on permissive versus restrictive interpretation (recall permissive is the default one). The transformation of a given automaton from a permissive interpretation to a restrictive one is obtained as follows by disabling its steps. Given a (permissive) automaton A, the high level operation "strong A" consists in adding the following constraint for every state s in A: In previous sections, we have introduced a model of polychronous automata in the polychronous model of computation. This polychronous MoC has been used previously as semantic model for systems described in the core AADL standard. The core AADL is extended with annexes, such as the Behavior Annex, which allows to specify more precisely architectural behaviors. The translation from AADL specifications into the polychronous model should take into account these behavior specifications, which are based on description of automata. In this section, we first describe the principles of a compositional semantic translation of AADL specifications into the polychronous model.

(1 A -trigger A (s)) * s = 0.

A short introduction to AADL

AADL is a SAE (Society of Automotive Engineers) standard, dedicated to modeling embedded real-time system architectures. It describes the structure of systems as an assembly of software components allocated on execution platform components together with timing constraints.

Architecture. Three families of components are provided in AADL:

• software application components, which include process, thread, thread group, subprogram, and data components; • execution platform components, which include processor, virtual processor, memory, device, bus, and virtual bus components; • composite components, which describe systems containing execution platform, application software, or other composite components.

Each component has a type, which represents the functional interface of the component and externally observable attributes. Each type may be associated with zero, one or more implementation(s) that describe the contents of the component, as well as the connections between components. The components communicate via data ports, event ports, and event data ports.

Properties. AADL properties provide information about model elements of an AADL specification. For example, a property Dispatch_Protocol is used to describe the dispatch type of a thread. Property associations in component declarations assign a particular property value (e.g., Periodic) to a particular property (e.g., Dispatch_Protocol) for a particular component. Timing properties associated with threads, such as Input_Time or Output_Time of ports, assure an input-compute-output model of thread execution.

Binding properties assign hardware platform to the execution of application components.

AADL timing execution model. Threads are dispatched either periodically, or by the arrival of data or events on ports, or by the arrival of subprogram calls from other threads, depending on the thread type. Three event ports are predeclared: dispatch, complete and error (Figure 8). A thread is activated to perform the computation at start time, and has to be finished before deadline. A complete event is sent at the end of the execution. The received inputs are frozen at a specified point (Input_Time), by default the dispatch time, which means that the content of the port does not change during the execution of a dispatch, even though the sender may send new values. For example, the values 2 and 3 (Figure 8) arriving after the first Input_Time will not be processed until the next Input_Time. As a result, the performed computation is not affected by a new input arrival until an explicit request for input. Similarly, the output is made available to other components at a specified point of Output_Time, by default at complete (resp., deadline) time if the associated port connection is immediate (resp., delayed) communication.

Behavior. The Behavior Annex provides an extension to AADL core standard so that complementary behavior specifications can be attached to AADL components. The behavior is described with a state transition system equipped with guards and actions.

AADL modeling

AADL time model in Polychrony

The key idea for modeling the computing latency and communication delay in Signal is to keep the ideal view of instantaneous computations and communications, while delegating computing latency and communication delays to specific "memory" processes, that introduce delay and well-suited synchronizations to timed signals.

A "memory" process o = f m (i, b) is used to repeat the input signal i on the instants of a Boolean signal b. The result o contains values of i when i is present and b is true, and the last value of i when i is absent and b is true:

o = f m (i, b) ≡ ∀t > 0 : o t =                i t if i t ⊥, and b t = true i pred(t) if i t =⊥, and b t = true, pred(t) = max{k < t | o k ⊥} ⊥ otherwise
freezing. Let f (x) represent the result of the behavior f of a given in port on its input signal x (e.g., f can be a FIFO to represent queued event or event data port). A port y = f (x) gives the available output y from the currently received input x:

y = f (x) ≡ ∀t > 0 : (x t ⊥⇔ f (x t ) ⊥) ∧ (y t = f (x t )))
The freezing of x at t, denoted here x t, is a function that takes an input x, a frozen time event t, and produces a new signal z at time t:

z = x t ≡ z = f m ( f (x), t)
Thread activation. We use th(z 1 , z 2 , . . . ) to represent the original computation of a thread th with frozen inputs z 1 , z 2 , . . . An activation condition start is introduced so that the thread th is activated to perform computation at start. This is denoted as th (z 1 , z 2 , . . . , start), where the inputs z 1 , z 2 , . . . are memorized at start: th (z 1 , z 2 , . . . , start) ≡ th(z 1 , z 2 , . . . ) where ∀i, z i = f m (z i , start) Output sending. Like for in ports, let g(y) represent the behavior of an out port. The sending function, denoted here y t, is such that the generated output of g(y) is hold and sent out at time t:

w = y t ≡ w = f m (g(y), t)

Compositional transformation

The translation from AADL to Signal is recursive. A package, which represents the root of an AADL specification, is transformed into a Signal module, the root of a Signal program, allowing to describe an application in a modular way. The rest of the transformation proceeds modularly by an inductive translation of the AADL concepts of a given model or source text. Each AADL component implementation is translated into a Signal process composed of the following elements:

• an interface consisting of input/output signals translated from the features (ports) provided by the component type, • additional control signals, that may also be added depending on the component category (Dispatch and Deadline for a thread), • a body, itself composed of subcomponents, subprogram call sequences, connections, component properties and a transition system specifying the functional behavior.

Threads. Let us sketch the principles of the translation of threads, which are the main executable and schedulable components. The six types of threads (periodic, aperiodic, sporadic, timed, hybrid, background) are discriminated by the dispatch: a dispatch request is periodic, or is triggered by an event (or event data) arriving, etc. The different threads are implemented in the same way, but the "dispatch" signal is generated differently.

An AADL thread component is implemented as a Signal process (Figure 9): it is composed of processes that represent its behavior, property, ports and subcomponents. The translation (as polychronous automata) of the transition system that provides the functional behavior of the thread will be illustrated on the case study described in Section 9.

Complete toolchain

A global view of the toolchain for modeling, timing analysis and verification of the AADL models in the polychronous MoC is given in Figure 10. The AADL model, which conforms to the AADL meta-model, is captured as AADL textual code in the OSATE toolkit [START_REF] Osate | OSATE V2 Project[END_REF]. The timing properties provide detailed timing specifications related to the AADL model. A model transformation toolchain, ASME2SSME, performs analyses on the ASME models (AADL Syntax Model under Eclipse) and generate Signal models in SSME (Signal Syntax Model under Eclipse). The SSME models can be transformed to Signal textual code within Polychrony.

An AADL2SIGNAL library provides common Signal processes reducing significantly the transformation cost. The timing properties represented as Signal clocks are calculated and analyzed in the compilation of Signal programs. Then, executable code can be generated for simulation. Associated tools, such as Sigali [START_REF] Marchand | Synthesis of discrete-event controllers based on the Signal environment[END_REF] and SynDEx [START_REF] Sorel | SynDEx: System-Level CAD Software for Optimizing Distributed Real-Time Embedded Systems[END_REF], can be used for further verification and validation. The global architecture, in the context of Polychrony, is represented in Figure 11. In this section, we present the ADDL modeling of an Adaptive Cruise Control (ACC) system, a highly safety-critical system embedded in recent cars, and we show how polychronous automata allow to verify properties over such an heterogeneous system.

Adaptive Cruise Control systems

Adaptive Cruise Control systems are embedded systems in cars. They get information from different sensors and can act on the speed of the vehicle, notably in the case of a risk of collision. As such, ACC systems are safety-critical systems, needing for careful design and verification.

An Adaptive Cruise Control System is an optional cruise control system for road vehicles that automatically adjusts the vehicle speed to maintain a safe distance from vehicles ahead. [. . . ] Control is imposed based on sensor information from onboard sensors [START_REF] Wikipedia | Autonomous cruise control system -wikipedia, the free encyclopedia[END_REF].

ACC systems pursue two main goals: automatically follow a preset speed (as a classical Cruise Control system), improving comfort of the driver, reducing fatigue and preventing subconsciously violating speed limits; and adapt the vehicle speed to maintain safe distance from vehicle ahead and prevent collisions.

For this, an ACC system gets information from different sensors: speedometer, lidar/radar to detect vehicles or obstacles ahead, and wheel sensor to adjust the position of the lidar/radar. It also gets information from the driver through buttons allowing to set the preferred speed and to activate/deactivate the system. Depending on the situation (presence of an obstacle or not, activation of the cruise control or not), it computes the acceleration/deceleration for the vehicle to reach the needed speed: the preferred speed of the driver if there is no obstacle and the cruise control is on, or the speed of the vehicle ahead if one is detected. Finally, it acts on the vehicle speed through its brakes and throttle.

ACC systems are thus highly safety-critical systems which have to satisfy multiple requirements linked to multiple perspectives:

• from the timing and scheduling perspective, all threads must meet their deadlines and the overall task of reacting to the presence or absence of an obstacle must meet a maximum reaction time; • from the logical perspective, the system must be free of deadlock and race condition; • from the security perspective, critical software components (processes or systems) must be protected from less critical components, thus executed on dedicated processors; • from the consumption perspective, the system must draw minimal power from the car battery, thus processors must run on the minimal possible frequency; • from the cost perspective, the overall cost of the system should be minimal, which means minimizing hardware component size and complexity.

All these requirements interact in many ways, and thus cannot only be checked on a subset of the system. Minimizing hardware components size and processors frequency to reduce construction costs and consumption of the vehicle will affect execution time and scheduling of the different tasks (e.g., less powerful processor will take more time to execute a task and smaller or slower buses will slow data communication). In the same way, changing a processor by another to reduce costs, may lead to impossible bindings between processes and processors (e.g., some embedded processors may be unable to execute complex operations).

To analyze collectively all these requirements, and ensure that choices made in order to satisfy one requirement does not break another (i.e., that the set of requirements is consistent), the full system must be analyzed at once. AADL model of the ACC system can be transformed into a Signal program, where behavior is described through polychronous automata and properties are used as constraints over the system. It is then possible to use the Polychrony framework to analyze and schedule the system. The Polychrony framework targets the two first perspectives presented above: time and scheduling, and logical perspectives. Requirements depending on other perspectives should be addressed using complementary analyzes.

AADL modeling of the Adaptive Cruise Control system

In the following, we present the modeling of a simplified ACC system using AADL. AADL provides a combination of visual and textual modeling: we use the visual representation for the overview of the system and details about connections, communications, and behavior automata, and we use the textual representation for details about requirements and properties such as types, numbered or enumerated properties and about behavior actions. 9.2.1 Architecture of the Adaptive Cruise Control system Figure 12 presents an overview of the system, consisting in:

• devices, such as sensors (speedometer, radar, wheel sensor), console with buttons and display, throttle and brakes; • buses allowing subsystems to communicate with each other and with devices; • controller and console subsystems.

Each of the two subsystems consists itself of hardware components, such as processors, memories and buses; and software components: processes containing threads. Figure 13 presents the controller subsystem and its components: one processor, one memory, one bus connecting the processor and the memory and one controller process. The controller process itself contains four threads, one for each sensor, and the ComputeActionThread, which is responsible for sending speed up, slow down or complete stop signals to the throttle and brakes of the vehicle.

Behavior of the Adaptive Cruise Control system

In AADL, system behavior is specified through the so-called behavior annexes attached to components. Behavior annexes specify the behavior of AADL components (threads and subprograms) through state transition systems with guards and actions, which can be expressed as polychronous automata.

Figure 14 shows the state transition system describing the behavior of the ComputeActionThread thread, which is responsible for processing the correct behavior the system should adopt (slow down, speed up or keep the speed constant) depending on the situation.

For readability sake, guards and actions have been omitted. In the case of this state transition system, guards are tests on input signals (are they present or not, and value comparison if they are present), and actions are of two kinds: either the sending of a signal through one of the output ports of the thread; or the computation of an intermediate value, such as the vehicle speed relative to the obstacle one, or the acceleration/deceleration needed to reach a given speed. For an example of such guards and actions, see Listing 1 which presents the complete transition from the Started state to the Detected one.

The state transition system starts in the Waiting state, waiting for its thread to be dispatched, and to pass in Started state. The Waiting state is a complete one, that is, a state in which a thread pauses its execution when entering in, waiting for a new dispatch.

After entering the Started state, depending on the inputs, the state transition system can pass in Detected (the system detected an obstacle) or Console state (the system did not detect an obstacle and the cruise control is on), or go back to the Waiting state (the system did not detect an obstacle and the cruise control is off).

In the Detected state, the system must decide the emergency of the situation: if the obstacle is in an unsafe range, the system goes into the Emergency state and its next transition will send a signal to brakes in order to stop the vehicle; if the obstacle is outside this range, the system enters the NoEmergency state and then determines whether it should slow down to adapt its speed to the obstacle speed, speed up or keep the speed constant (each transition sending the corresponding signal to the throttle after the computation of the needed acceleration/deceleration). The same happens in the Console state depending on the current speed of the vehicle and the speed preset by the driver. After saving useful values (e.g., current speed, current obstacle speed and distance in the SaveValues state, the state transition system returns in the Waiting state, waiting for the next dispatch of its thread.

Properties of the Adaptive Cruise Control system

Requirements, such as threads deadline, sensors period, memories and buses size, processors frequency and scheduling policies, are modeled using AADL properties.

Timing and scheduling requirements on a thread can be expressed through AADL properties such as: dispatch protocol (Dispatch_Protocol), period in case of a periodic dispatch (Period), execution deadline (Deadline) and worst-case execution time (Compute_Execution_Time). For example, Listing 2 presents these properties attached to the ComputeAction-Thread thread. Logical requirements, such as the absence of deadlocks and race condition, are not explicitly expressed through properties, but automatically checked by the Polychrony framework.

Refinement and verification of system requirements using the polychronous model of computation

The AADL model of the ACC system can be transformed into a Signal program, where behavior is described through polychronous automata and properties are used as constraints over the system. It is then possible to use the Polychrony framework to analyze and schedule the system.

Transformation of the Behavior Annex to Signal

An overview of the compositional transformation from AADL to Signal is presented in Section 8. We will now focus on the translation of a state transition system described through an AADL behavior annex to a polychronous automaton described in Signal. The rules describing formally the semantics of the Behavior Annex and its translation in transition systems represented as polychronous automata are de-tailed in [START_REF] Besnard | Formal semantics of behavior specifications in the architecture analysis and design language standard[END_REF]. Here, we rather provide the intuition of this translation as Signal automata through our case study.

Such an automaton is described using the Signal syntactic extensions presented in Section 7. Listing 3 shows the declaration and interface (input and output signals) of the Signal automaton process corresponding to the state transition system of the ComputeActionThread thread presented above.

States are simply declared as Signal labels. Listing 4 presents declaration of a few states from the Signal automaton obtained from the transition system of the ComputeAc-tionThread thread of the Adaptive Cruise Control system.

Transitions are declared as a label attached to special Signal process Automaton_Transition which takes as parameters the labels of the source and destination states, and the condition expression corresponding to the AADL guard of the transition. Moreover, transition processes declare Signal equations to compute when firing the transition. Listing 5 presents the Signal declaration corresponding to the AADL transition presented in Listing 1. Listing 3 Signal declaration and interface of the automaton corresponding to the transition system of the ComputeActionThread thread. Once the AADL model of a system transformed into a Signal program, one can analyze the program using the Polychrony framework in order to check if timing, scheduling and logical requirements over the whole system are met.

Verification of timing and scheduling requirements

Polychrony provides a schedulability analysis for periodic programs obtained from AADL models. In particular, it can detect non-schedulable systems thanks to the timing properties (mainly the period and the WCET-Worst Case Execution Time). Moreover, with some extra information (port rates), periods can be left undefined: they will be computed by calling a standalone plugin named ADFG (this plugin is based on the work of Bouakaz [START_REF] Besnard | Timed behavioural modelling and affine scheduling of embedded software architectures in the AADL using Polychrony[END_REF][START_REF] Bouakaz | Real-time scheduling of dataflow graphs[END_REF]).

The schedulability test is triggered during the translation of an AADL processor device into Signal, provided that all threads of the unique process bound to this processor are periodic and have at least a defined Compute_Execution_Time. The test is composed of the two following steps:

1. Polychrony checks that all threads have a defined period and tries to compute it if it is not the case (in our case study, all periods are defined so this step is skipped). The periods can be computed if all threads define connections between them (such that they form a connected graph) and have Input_Rate and Output_Rate properties on their connections' ports. The computation is done by ADFG which ensures that the deduced periods imply a schedulable system. 2. A simple utilization factor test is done on the system (which is useful especially if the periods are userprovided). If the utilization factor is less than one, each thread period is converted into an affine clock relation between the fastest clock and each thread control signal (Dispatch, Resume, Deadline, Initialize) with corresponding phases. Otherwise, the AADL to Signal transformation continues on the other AADL elements.

Note that this way of defining the periodic thread control signals implies that the generated Signal code does not take into account possible thread preemptions: this is oriented towards functional simulation.

The current implementation has some limitations: e. g., all temporal properties (periods, etc.) must be expressed in the same time unit, and the scheduled threads must be in the same unique process of a processor. Future work is dedicated to release these limitations and to use an exact scheduling test in the step 2, instead of the utilization factor (which is only a necessary condition), for EDF (Earliest Deadline First) and DM (Deadline Monotonic) scheduling algorithms. Besides, the step 1 is based on ADFG which can compute the best periods, deadlines, and communication buffer sizes given a cyclo-static dataflow graph, in order to maximize the throughput. This is more than what is currently used, so a possible improvement would be to reuse all the ADFG results to refine more AADL properties related to the scheduling. In this graph, cycles represent possible deadlocks: cyclical data dependencies between signals and/or clock variables. However, since dependencies are conditioned, Polychrony only needs to consider instants where all the dependencies are valid. To do so, it computes the product of the labels of each edge in the cycle. If this product is null, there is no instant where all the dependencies are valid at the same time, and thus there is no possible deadlock.

If the product clock of every cycle in the Graph of Conditional Dependencies of the Signal program is null, then the program (and the AADL model from which it has been obtained) is deadlock-free.

On the case study, a race condition due to an error in the state transition system of the ComputeActionThread was detected thanks to the clock calculus of Polychrony.

In addition, model checking based formal verification can be performed in the Polychrony framework using the associated Sigali tool [START_REF] Marchand | Synthesis of discrete-event controllers based on the Signal environment[END_REF]. Properties such as invariance, reachability and attractivity can be checked by Sigali. Algorithms for computing state predicates are also available in the tool.

Conclusion

We have presented a model of finite-state automata, called polychronous automata, that integrates smoothly with dataflow equations in the polychronous model of computation. They define transition systems to express explicit reactions together with properties, in the form of Boolean formulas over logical time, to constrain their behavior.

The implementation of such automata amounts to composing explicit transition systems with a controller synthesized from the specified constraints.

Polychronous automata have been integrated in the opensource version of the Polychrony framework through lightweight syntactic extensions of the Signal language. They may be used to specify behaviors (and constraints) and to abstract behaviors, as the result of a formal calculus.

This formal model of automata supports the recommendations adopted by the SAE committee on the AADL to implement a timed and synchronous behavioural annex for the standard [START_REF] Besnard | Logically timed specifications in the AADL: a synchronous model of computation and communication[END_REF]. The model of polychronous automata has been provided as semantic model for our proposal of an extension of the AADL Behavior Annex.

An experimental implementation of the semantic features of this "timing annex" enriches the already existing transformation from AADL models to Signal programs to consider behavior of AADL models. This transformation will be integrated in the POP environment for Eclipse 3) . The implementation has been tested with the Adaptive Cruise Control case study, developed with Toyota ITC. Adaptive Cruise Control systems are highly safety-critical car embedded systems which need to satisfy multiple interdependent requirements. Polychronous automata allow us to define a complete semantic model for AADL specifications of such systems. We provide tools over this semantic model for verifying and analyzing properties (such as deadlock freeness and schedulability) over a whole system.

  Given a non empty finite set of signal variables A, a function b : A → D ∞ that associates a sequence b(a) with each variable of a ∈ A is named a behavior on A. The length |b| of a behavior b on A is the length of the smallest sequence b(a). An event on A is a behavior b : A → D ⊥ . For a behavior b on a set of signal variables A, and an integer i |b|, b(i) denotes the event e on A such that e(a) = (b(a))(i) for all a ∈ A. An event e on A is said to be empty iff e(a) = ⊥ for all a ∈ A. The concatenation of signals is extended to tuples of signals. Two behaviors b 1 , b 2

  k.a. [b] or [:b]), defined by ˆb when b (present, and true, when b is present and is true) • intersection x1 ˆ* x2, defined by ˆx1 when ˆx2 • union x1 ˆ+ x2, defined by ˆx1 default ˆx2 • difference x1 ˆ-x2, defined by [(not ˆx2) default ˆx1] • synchronization x1 ˆ= x2, defined as (c := (ˆx1 = ˆx2))/c

  The clock hierarchy is defined by a relation ˆ (dominates) on the quotient set of signals by ˆ= (x and y are in the same class iff they are synchronous). Informally, a class C dominates a class D if the clock of D is computed as a function of Boolean signals belonging to C and/or to classes recursively dominated by C. A node n of a tree, which is a clock equation, contains also the list of signals signal(n) the clock of which is equal to this class. A tree represents an endochronous process: it has a fastest rated clock and the status (presence/absence) of all signals is a pure flow function (this status depends neither on communication delays, nor on computing latencies).

Figure 2

 2 Figure 2 Refinement of state s n in P n-1 i by the automaton (P n i1 , P n i2 )

Figure 3 ,Figure 3

 33 Figure 3 A restrictive behavior

Figure 4

 4 Figure 4 A reactive behavior

  wait := change cell (a^+b) init false | waiting := wait $ init false | change := (true when a when not waiting) default (false when b when waiting)

Figure 5

 5 Figure 5 Automaton for ABRO

Figure 6

 6 Figure 6 Polychronous automaton (with implicit stuttering loops)

Figure 7

 7 Figure 7 "alternate" automaton

Figure 8

 8 Figure 8 time model for an AADL thread

Figure 9

 9 Figure 9 Thread modeling

Figure 10 A

 10 Figure 10 A global view of the AADL to Signal toolchain

Figure 11

 11 Figure 11 Global architecture

Figure 12

 12 Figure 12 Overview of the Adaptive Cruise Control system modeled with AADL. Double-lined rectangles represent devices, double-arrows buses and rectangles with rounded corners systems and subsystems.

Figure 13

 13 Figure 13 Controller subsystem of the Adaptive Cruise Control system modeled with AADL. Rectangles represent processors, double-arrows buses, cylinders memories and rhombuses processes and threads.

Figure 14 Listing 1

 141 Figure 14 State transition system for the ComputeActionThread thread.

Listing 2

 2 Timing and scheduling properties of the ComputeActionThread thread implementation (double right arrows associate values to properties).

labelListing 4

 4 S_Waiting, S_Started, S_Detected [...] Extract of the Signal declaration of the states of the automaton corresponding to the transition system of the ComputeActionThread thread.

(Listing 5

 5 | t1 :: Automaton_Transition(S_Started, S_Detected, [:inObstacleDetected]) | on t1 :: (| obstacle_distance ::= inObstacleDistance |) |) Signal translation of the AADL transition presented in Listing 1.

9. 3 . 3

 33 Verification of logical requirements Polychrony also allows to detect deadlocks in an AADL model of a given system. After the transformation of the AADL model to a Signal program (following the compositional transformation presented in Section 8), the Polychrony framework calculates the Graph of Conditional Dependencies of the Signal program and computes the product clock of each cycle in this graph (a cycle representing a potential deadlock) [41]. The Graph of Conditional Dependencies is a labeled directed graph where: • vertices are the signals and clock variables; • edges indicate data dependencies among signals and clock variables; • labels represent the conditions at which the dependencies are valid.


Adeline Crépieux

Marine Guigou

P. DEVILLARD Alexandre Popoff

Pierre Devillard

Thierry Martin

A Cr Épieux

Photo-assisted shot noise in Coulomb interacting systems

come

Introduction

In mesoscopic systems, the measurement of shot noise makes it possible to probe the effective charges which flow in conductors. This has been illustrated experimentally and theoretically when the interaction between electrons is less important 1 or when it is more relevant 2,3 . Additional informations can be obtained through the photo-assisted noise when an AC bias is superposed to the DC bias. Experimentally, photo-assisted noise has been measured in diffusive wires, diffusive junctions and quantum point contacts 4 . For normal metals, the noise derivative displays steps 5 at integer values of the ratio ω 0 /ω, where ω is the AC frequency and ω 0 is related to the DC voltage. We naturally expect that this behavior is modified in Coulomb interacting systems. The present work deals with two specific one-dimensional correlated systems: a Hall bar in the fractional quantum Hall regime, for which charge transport occurs via two counterpropagating chiral edges states, and a carbon nanotube to which electrons are injected from a Scanning Tunneling Microscope (STM) tip.

2 Photo-assisted noise in the fractional quantum Hall regime

The first system we consider is a two-dimensional electrons gas in the fractional quantum Hall regime which is described by the Hamiltonian H = H 0 + H B . The kinetic term H 0 = (hv F /4π) r=R,L ds∂ s φ r (t)) 2 describes the right and left moving chiral excitations along the edge states (φ R and φ L are the bosonic fields), and

H B = A(t)Ψ † R (t)Ψ L (t) + h.c
. describes the transfer of quasiparticles from one edge to the other.

Ψ R(L) = F R(L) e i √ νφ R(L) (t) /
√ 2πa where F R(L) is a Klein factor, a, the short-distance cutoff and ν, the filling factor which characterizes the charge e * = νe of the backscattered quasiparticles. The backscattering amplitude between the edge states has a time dependence due to the applied voltage V (t) = V 0 + V 1 cos(ωt):

A(t) = Γ 0 e i νe h dtV (t) = Γ 0 e iω 0 t+i ω 1 ω sin(ωt) = Γ 0 +∞ p=-∞ J p ω 1 ω e i(ω 0 +pω)t , (1)
where ω 0 ≡ νeV 0 /h and ω 1 ≡ νeV 1 /h. We have made an expansion in term of an infinite sum of Bessel functions J p of order p, which is a signature of photo-assisted processes 6 .

The backscattering current noise correlator is expressed with the help of the Keldysh contour:

S(t, t ′ ) = η=±1 T K {I B (t η )I B (t ′-η ) exp(-i K dt 1 H B (t 1 ))} /2 where I B (t) = iνeA(t)Ψ † R (t)Ψ L (t)- h.c
. is the current operator. We are interested in the Poissonian limit only, so in the weak backscattering case, one collects the second order contribution in the tunnel amplitude A(t).

The main purpose of this work is to analyze the double Fourier transform of the noise S(Ω 1 , Ω 2 ) ∝ dt dt ′ S(t, t ′ ) exp(iΩ 1 t + iΩ 2 t ′ ) when both frequencies Ω 1 and Ω 2 are set to zero. At zero temperature, the shot noise exhibits divergences 7 at each integer value of the ratio ω 0 /ω which are not physical since they appear in a range of frequencies where the perturbative calculation turns out to be no more valid. At finite temperature, the photo-assisted noise reads:

S(0, 0) = (e * ) 2 Γ 2 0 2π 2 a 2 Γ(2ν) a v F 2ν 2π β 2ν-1 × +∞ p=-∞ J 2 p ω 1 ω cosh (ω 0 + pω)β 2 Γ ν + i (ω 0 + pω)β 2π 2 , ( 2
)
where Γ is the Gamma function and We have tested the validity of our result by setting ν = 1 which corresponds to a noninteracting system. The derivative of the noise according to the bias voltage exhibits staircase behavior as shown on Fig. 1 (left). Steps occur every time ω 0 is an integer multiple of the AC frequency. This is in complete agreement with the results obtained be Lesovik and Levitov for a Fermi liquid 5 . For a non-integer value of the filling factor (ν = 1/3), the shot noise derivative exhibits evenly spaced singularities as seen on Fig. 1 (right), which are reminiscent of the tunneling density of states singularities for Laughlin quasiparticles. The spacing is determined by the quasiparticle charge νe and the ratio of the bias voltage with respect to the AC frequency. Photo-assisted transport can thus be considered as a probe for effective charges at such filling factors, and could be used in the study of more complicated fractions of the quantum Hall effect.

β = 1/k B T . -3 -2 -1 0 1 2 3 -2.5 -2 -1.5 -1 -0.5 0 0.5 1 1.5 2 2.5 ω 0 /ω dS(0,0)/dω 0 -4 -3 -2 -1 0 1 2 3

Photo-assisted noise in carbon nanotube

We consider the following setup: an STM tip close to a carbon nanotube connected to leads at both extremities. A voltage applied between the STM and the nanotube allows electrons to tunnel in the center region of the nanotube. As a result, charge excitations propagate along the nanotube towards the right and left leads. This system is described by the Hamiltonian H = H N + H STM + H T . The nanotube is a non-chiral Luttinger liquid 8 :

H N = 1 2 jδ +∞ -∞ dx v jδ (x) K jδ (x)(∂ x φ jδ ) 2 + K -1 jδ (x)(∂ x θ jδ ) 2 , ( 3
)
where x is the position along the nanotube, φ jδ and θ jδ are non-chiral bosonic fields and K jδ is the Coulomb interactions parameter for each charge/spin, total/relative sectors jδ ∈ {c+, c-, s+, s-}. We take K c-= K s+ = K s-= 1, and we assume that K c+ depends on position 9 as depicted on Fig. 2a. The velocities satisfy v jδ (x) = v F /K jδ (x).

The electrons in the metallic STM tip are assumed to be non-interacting. For convenience, the electron field c σ in the STM tip can be described in terms of a semi-infinite Luttinger liquid with Coulomb interactions parameters all equal to one. The tunnel Hamiltonian between the STM tip and the nanotube at position x = 0 is H T (t) = rασ Γ(t)Ψ † rασ (0, t)c σ (t) + h.c. where r corresponds to the branch index, α to the mode index and σ to the spin. The fermionic fields for electrons in the nanotube and in the STM tip are respectively defined by: Ψ rασ (x, t) = F rασ e ik F rx+iq F αx+iϕrασ(x,t) / √ 2πa and c σ (t) = f σ e i φσ(t) / √ 2πa where a is the ultraviolet cutoff of the Luttinger liquid model, F rασ and f σ are Klein factors, k F is the Fermi momentum and q F is the momentum mismatch associated with the two modes α.

In the presence of a voltage modulation superimposed on the constant DC voltage, V (t) = V 0 +V 1 cos(ωt), the tunnel amplitude becomes Γ(t) = Γ +∞ p=-∞ J p (ω 1 /ω) exp(i(ω 0 +pω)t), where J p the Bessel function on order p, ω 0 ≡ eV 0 /h and ω 1 ≡ eV 1 /h. The calculation of noise is thus analogous to the one which applies to the fractional quantum Hall effect, except that here only electrons tunnel in the nanotube. We thus obtain 10 :

S(0, 0) = 4Γ 2 e 2 π 2 a 2 +∞ p=-∞ J 2 p ω 1 ω +∞ 0 dτ cos((ω 0 + pω)τ ) 1 + v F τ a 2 1+ν 2 × cos (1 + ν) arctan v F τ a + 1 8 ∞ n=1 b n c+ K c+ + (-b c+ ) n K c+ arctan 2av F τ a 2 +(nLK c+ ) 2 -(v F τ ) 2 ∞ n=1 a 2 +(nLK c+ ) 2 -(v F τ ) 2 a 2 +(nLK c+ ) 2 2 + 2av F τ a 2 +(nLK c+ ) 2 2 1 16 b n c+ K c+ +(-b c+ ) n K c+ , (4)
where b c+ = (K c+ -1)/(K c+ + 1) is the reflexion coefficient at the nanotube contacts x = ±L/2 and ν = jδ (1/K jδ + K jδ )/8.

The "standard" way 5 to display the results for photo-assisted transport is to consider the noise derivative as a function of voltage: in particular, this allows to compare the results with the non-interacting case where the noise derivative exhibits a staircase variation. In Fig. 2b, we plot the numerically computed noise derivative as a function of the ratio ω 0 /ω in the presence of Coulomb interactions (K c+ = 0.2).

For ω L /ω = 0.1 (full line), we are in the limit where the wave packet spatial extension is smaller that the nanotube length. In this regime (except for a small region close to the origin) the vast majority of the voltage scale lies in the regime where ω 0 > ω L . The noise derivative differs from the single electron behavior, in the sense that the sharp steps and plateaus expected in this case are absent. Instead, because of Coulomb interactions effects, the noise derivative is smoothed out, but there is a clear reminiscence of the step positions: the slope of dS(x, x; Ω = 0)/dω 0 increases abruptly at the location of the steps. We attribute the smoothing to the tunneling density of states on the nanotube which is modified by the Coulomb interactions in the nanotube. For ω L /ω = 1.2 (dashed line), we are in an intermediate regime for which electron wave packets are comparable to the nanotube length. For ω L /ω = 6 (dashed-dotted line), we are in the limit where electron wave packets are larger than the nanotube length, and as a consequence, the finite size effects dominate over the Coulomb interactions effects and a stepwise behavior in dS(x, x; Ω = 0)/dω 0 , which is typical of non-interacting metals, can be identified.

✁ ✁ ✁ ✁ ✁ ✁ ✁ ✁ ✁ ✁ ✁ ✁ ✁ ✁ ✁ ✁ ✁ ✁ ✁ ✁ ✁ ✁ ✁ ✁ ✁ ✁ ✁ ✁ ✁ ✁ ✁ ✁ ✁ ✂ ✁✂ ✁✂ ✁✂ ✁✂ ✁✂ ✁✂ ✁✂ ✁✂ ✁✂ ✁✂ ✁✂ ✂ ✁✂ ✁✂ ✁✂ ✁✂ ✁✂ ✁✂ ✁✂ ✁✂ ✁✂ ✁✂ ✁✂ ✂ ✁✂ ✁✂ ✁✂ ✁✂ ✁✂ ✁✂ ✁✂ ✁✂ ✁✂ ✁✂ ✁✂ ✄ ☎✄ ☎✄ ✆ ☎✆ ☎✆ ✝ ✝ ✞ ✞ ✟ ☎✟ ☎✟ ✠ ☎✠ ☎✠ V Nanotube STM Γ 0 K (x) c+ x L / 2 -L / 2 1 0 a) 0 1 2 3 4 0 0.5 1 1.5 2 ω 0 / ω dS(x,x;0) / dω 0 b ) ω L /ω = 0.1 ω L / ω = 1.2 ω L / ω = 6

Conclusion

Photo-assisted noise is affected by Coulomb interactions in one-dimensional systems. In the fractional quantum Hall effect, the photo-assisted noise shows evenly spaced singularities with a spacing related to the filling factor. As a consequence, photo-assisted noise measurement in such a system could be used to extract fractional charge. In carbon nanotube, Coulomb interactions affect the height and shape of the steps in the differential noise when ω L /ω is small. On the contrary, when ω L /ω ≥ 1, finite size effects play an important role and attenuate the Coulomb interactions effects.

Figure 1 :

 1 Figure 1: Noise derivative in the fractional quantum Hall regime as a function of ω 0 /ω = νV 0 /hω for (left) ν = 1 at temperatures: kBT /hω = 0.01 (solid line) and kBT /hω = 0.1 (dashed line) and for (right) ν = 1/3 at temperatures: k B T /hω = 0.05 (solid line) and k B T /hω = 0.15 (dashed line). We take ω 1 /ω = eV 1 /hω = 3/2.

Figure 2 :

 2 Figure 2: a) Picture of the system and spatial variation of the Coulomb interactions parameter Kc+; b) Shot noise derivative in the nanotube for Kc+ = 0.2, ω1/ω = 2, ωc/ω = 100 and several values of ωL/ω.