Dumitru Potop
email: dumitru.potop_butucaru@inria.fr

Semantics foundations of PsyC based on synchronous Logical Execution Time

Keywords: Computer systems organization → Real-time languages; Real-time system specification Multiform Logical Time, Synchronous languages, Logical Execution Time, Real-Time Systems

Task models for Real-Time Scheduling (RTS) and Synchronous Reactive (SR) languages are two prominent classes of formalisms for the design and analysis of time-critical embedded systems. Task models allow providing deadlines, periods, or other such kinds of interval time boundaries that make the system description fit for schedulability analysis. Synchronous reactive languages use logical clocks to be activation condition triggers in languages providing programmability. We consider here synchronous LET (sLET) extensions that intend to re-use notions of logical clocks and logical time, for the purpose of providing schedulability boundaries. As its name indicates, sLET borrows deeply from Logical Execution Time ideas, where timing dimensions are all provided at logical design time, but they extend asynchronous events as in xGiotto with SR-inspired programmability and "first-class citizen" logical clock constructs. Our work results in a two-level semantics of the programming language PsyC. The benefits are to reuse techniques from both RTS and SR. Big-step RTS models provide inputs for task model schedulability analysis and implementation. Meanwhile, SR small-step models provide methodological tools to view any events as a time base (logical clock) and verification technologies (but they do not consider the WCET of tasks to be kept within time boundaries by the scheduling). We show the semantic equivalence of those two semantics at visible time interval boundaries.

INTRODUCTION

Real-Time Systems have to handle time in a predictable manner. Specified temporal requirements from a system specification should still hold in the final system. Thus, time must be considered from the very start of the design. However, exact computation durations are usually not available in early design phases as they depend on the target. In answer, various formalisms based on the Multiform Logical Time concept have been introduced to abstract [START_REF] André | A multiform time approach to real-time system modeling; Application to an automotive system[END_REF] those target-dependent durations (expressed in physical time) with logical time constraints (expressed in logical time). Then, specific analysis, usually called schedulability analysis (or time safety analysis) can be used to fill the gap between logical and physical time, that is, they ensure that physical computations satisfy their logical time constraints. In RTS models this usually translates into the fact that real-time constraints are specified as requirements, while worst-case execution time (WCET) of tasks is provided as guarantees. Schedulability analysis then breaks down in satisfying the contract that WCET guarantees imply real-time constraints. Although the PsyC language defined later includes WCET modeling and scheduling resolution, it is out of the scope of the current paper, which focuses on its specification expressiveness combining influences from RTS, SR and LET.

The synchronous approach introduced a discretized abstraction of time based on logical clocks in which computations and reactions happen in discrete atomic instants, and so, logically instantaneously [START_REF] Benveniste | The Synchronous Languages 12 Years Later[END_REF]. While multiple logical clocks may be used for specification expressiveness of sophisticated event-based timing patterns, the traditional operational semantics of synchronous languages usually imposes to expand the behaviors on a unique parent clock. Consequently, compilation of synchronous languages may suffer from the "Long Task Problem" [START_REF] Girault | Clock-Driven Automatic Distribution of Lustre Programs[END_REF]. When different tasks of different rhythms are compiled, physical execution time variability is usually limited to a common cycle rate. More recently, the Logical Execution Time (LET) paradigm [START_REF] Kirsch | The Logical Execution Time Paradigm[END_REF] has been introduced to give a compromise between the strong expressiveness of the synchronous approach and the efficiency of traditional task scheduling. For that, LET mandates to specify the actual logical duration a task has to fulfill based on a uniform pseudo-physical time. This forms LET intervals in which communications can only happen on its bounds. Inputs can only be consulted at the start of the interval and outputs are displayed to other tasks at the end. Consequently, as communication can only be made at predefined instants, LET ensures the temporal determinism property.

Previous work has introduced early results on the definition of synchronous LET (sLET) as being a variation of LET based on the Multiform Logical Time approach [START_REF] Siron | The synchronous Logical Execution Time paradigm[END_REF]; it allows defining LET intervals with respect to multiple logical clocks. Therefore, the duration of an interval is specified as being up to the next 𝑛 𝑡ℎ tick of a clock. It should be noted that such logical duration is not necessarily constant across all reactions as it is specified relatively to a clock. In the simple case where there is only one global clock used as in the original LET paradigm, all durations become constants. Hence, sLET is a generalization of the original LET paradigm. Moreover, as the sLET allows multiple valid schedules taking into account physical time that are mutually equivalent with respect to logical clocks, the classical synchronous semantics is actually one of those in which computations happen logically instantaneously at the start of sLET intervals and outputs are delayed at the end. This article goes further than our previous work in [START_REF] Siron | The synchronous Logical Execution Time paradigm[END_REF], introducing an equivalence relation theorem between semantics.

To illustrate this approach, this article gives in section 3 the abstract syntax and the formal semantics of PsyC, an industrial language developed by the company Krono-Safe, which implements the sLET paradigm. The approach may benefit from the fact that it is an industrial-scale language, with a user community of embedded engineers. The formal semantics of PsyC is then defined using two approaches, one native semantics in section 3.2 and an other semantics defined by translation into the Esterel language in section 4, thereafter called the synchronous semantics. Both semantics are observationally equivalent with respect to sLET interval boundaries formalized in section 4.3. Indeed, while the synchronous semantics covers a whole PsyC application, our native semantics covers only individual agents (i.e. PsyC sequential tasks). Through a discussion in section 5, this article shows how synchronous techniques such as formal verification could then be re-used for (s)LET based languages.

RELATED WORK

The synchronous approach has been implemented in languages such as Esterel or Lustre [START_REF] Benveniste | The Synchronous Languages 12 Years Later[END_REF]. It is based on the Multiform Logical Time approach and thus, totally abstracts execution time to focus on logical instants, allowing both determinism and concurrency. Nonetheless, compilation can be non-trivial given non-negligible (physical) execution times, as described in the Long Task Problem to which some answers have been proposed [START_REF] Girault | Clock-Driven Automatic Distribution of Lustre Programs[END_REF]. Still, today, the common workaround in the industry is to slice long tasks into sub-tasks that fit in the instant period.

The Logical Execution Time approach has been introduced with the Giotto language [START_REF] Kirsch | The Logical Execution Time Paradigm[END_REF], later extended with the Timing Definition Language (TDL), which allows describing applications with a fixed set of periodic tasks and some global modes mechanism. However, those two languages do not consider logical time as being anything else than a simple abstraction of physical time. Similarly to PsyC, TimedC extends C with timing primitives, although also using an abstraction of physical time [START_REF] Natarajan | Timed C: An Extension to the C Programming Language for Real-Time Systems[END_REF]. xGiotto [START_REF] Ghosal | Event-Driven Programming with Logical Execution Times[END_REF] is closer to our work as it extends Giotto with events handled by a mechanism called event scoping. While our sLET paradigm can express the same kind of patterns, it treats any event or time(s) basis in the same way through logical clocks.

sLET also shares similarities with the Sparse Synchronous Model (SSM) [START_REF] Stephen | The sparse synchronous model[END_REF]; both dedicated to applications with sparse and potentially irregular computations. However, sLET still handles time with logical time units as in the Multiform Logical Time approach while SSM handles temporal expressions based on abstracted physical time units. Nonetheless, as SSM, the sLET semantics is also inspired by discrete event model such as Lingua Franca [START_REF] Lohstroh | Toward a Lingua Franca for deterministic concurrent systems[END_REF].

Although related, sLET also differs from k-periodic networks or N-synchronous systems [START_REF] Cohen | N-synchronous Kahn networks: a relaxed model of synchrony for real-time systems[END_REF]. These formalisms aim at providing a certain flexibility in exact execution instants based on a global timing framework in which synchrony can be relaxed. In sLET the focus is extended to placing in time behaviors with a certain duration in terms of number of instants spent in a single behavior.

THE PSYC LANGUAGE 3.1 Informal Description of PsyC

The industrial language PsyC is a language developed by the French company Krono-Safe [START_REF]Krono-Safe[END_REF], which provides a set of tools for the design and the integration of safety-critical real-time applications. Such applications can then be certified at the highest level of criticality for the avionic domain (DAL-A with the DO-178C standard). PsyC stands for Parallel SYnchronous and has been initially presented as a model based on the timed-triggered approach [START_REF] David | Safety Properties Ensured by the OASIS Model for Safety Critical Real-Time Systems[END_REF]. As stated in the introduction, previous work has introduced an early definition of the synchronous LET paradigm as being a generalization of the LET paradigm. As the modern version of PsyC can now use multiple logical clocks, it naturally implements the synchronous LET paradigm.

Similarly to Multiform Logical Time concept, time is defined through the use of logical clocks, that is, totally-ordered sequences of ticks. The PsyC language allows describing two levels of logical clocks:

• sources are externally-defined logical clocks, they can be mapped to a timer (i.e. pseudo-physical time) or any events (e.g. the rotation of an engine crankshaft); • clocks define a sub-sampling of sources; they are defined through an affine relation 𝑝 × 𝑐 + 𝑜 with 𝑝 and 𝑜 being respectively the period and the offset with respect to another clock or source 𝑐.

1 body start { 2 y1 = f ( x1 ); 3 advance 2 with A ; 4 y2 = g ( x2 ); 5 advance 3 with B ; 6 }

Listing 1: Simple PsyC example

A PsyC application is composed of multiple concurrent components, called agents. Each agent defines an infinite sequential behavior using a syntax based on the C language. A special statement called advance allows synchronizing on a tick of a given PsyC clock. They specify both the deadline of preceding code, and the activation of code following it. Moreover, following the LET semantics, the advance specifies the instants in which communication can happen. As an example, the Listing 1 describes an infinite loop agents can communicate with each other through dedicated deterministic communication channels. The main one, called temporal variable, is an implicit one-to-several real-time data flow. The task owner of the temporal variable updates this flow at a predetermined rhythm. Moreover, its value is sampled with respect to a clock allowing an additional sampling level between different agents, but we will not consider it in this article. Determinism of communication is ensured by the visibility principle, defined as follows:

• a data can only be timestamped with a date greater or equal to its corresponding deadline; • a data can be consulted only if its timestamp is lower or equal to the current activation date;

In the Listing 1, in the first interval, 𝑦1 is made visible at the deadline specified by the next advance at line 3 while in the second interval, 𝑥2 should be visible from the activation specified by the preceding advance, also at line 3. Listing 2: PsyC implementation of a GNC task [START_REF] Carle | From Dataflow Specification to Multiprocessor Partitioned Time-triggered Realtime Implementation[END_REF] This mechanism, along with agent synchronization, is an implementation of the synchronous Logical Execution Time approach. As a simple example, consider the Listing 2. It implements a modified version of the conditional triggering of a Guidance, Navigation and Control System (GNC) as described in [START_REF] Carle | From Dataflow Specification to Multiprocessor Partitioned Time-triggered Realtime Implementation[END_REF]. The example uses three clocks: a source clock, expected to have a period of 1 ms, and two periodic clocks c20ms and c50ms which have a period of respectively 20 and 50 ms. The example shows only one agent called GNC which has two consulting inputs: sensors and mode, and one displaying output: commands. When not in nominal mode, the condition of line 8 is false and the agent waits for the next tick of clock c50ms. When in nominal mode, the condition of line 8 is true and the computation is constrained with a deadline of 2 ticks of clock c20ms. Then, afterward, the agent waits for the next tick of clock c50ms as shown in Figure 2.

In this article, we consider a subset of PsyC which grammar is described in Figure 1. The left column specifies the PsyC constructions defined at the application level while the right column describes the PsyC syntax at the agent level. The syntax is quite abstract with respect to the concrete one which is based on the C language. However, the objective here is to highlight the reactive part of PsyC.

Native Operational Semantics of PsyC

This section gives a native formal semantics of PsyC agents based on the Structural Operational Semantics (S.O.S.) approach introduced by Plotkin [START_REF] Plotkin | A structural approach to operational semantics[END_REF] and adapted later by Berry [START_REF] Potop-Butucaru | Constructive Operational Semantics[END_REF] to reactive languages. A more detailed version of the semantics will be made available in a research report [START_REF] Siron | Formal Semantics of the PsyC language[END_REF]. The global approach is to successively rewrite the program such that each rewriting represents a logical instant. Transition rules (or relations) describe valid rewritings of the program. The following section describes the notations used by these rules.

Configuration and Transitions syntax.

In this paper, a configuration (i.e. a program state) of an agent is defined by the following tuple:

⟨𝐸, 𝑏,𝑇 𝑜𝑢𝑡𝑝𝑢𝑡 ⟩ where 𝐸 is the private environment of the agent, 𝑏 is the identifier of the next body to be executed and 𝑇 𝑜𝑢𝑝𝑢𝑡 is the public environment of the agent. This allows to distinguish values that can be accessed by other tasks (through the temporal variable mechanism) and values that shouldn't be accessed.

Two different transitions are considered in the semantics: transitions that explicitly consume logical time and ones that are executed in the instant. We shall call the former temporal transitions and the latter non-temporal transitions.

Non-temporal transitions are expressed using the following syntax:

𝐶 ⊢ 𝑡 -→ 𝐶 ′ ⊢ 𝑡 ′
where 𝐶 (resp. 𝐶 ′ ) denotes the agent configuration before (resp. after) the transition and 𝑡 (resp. 𝑡 ′ ) denotes the agent program before (resp. after) the transition. Temporal transitions are defined similarly:

𝐶 ⊢ 𝑡 =⇒ 𝑛×𝑠 𝐶 ′ ⊢ 𝑡 ′
where 𝑛 ∈ N * and 𝑠 is a source denoting a temporal transition that has a duration of 𝑛 ticks of the source 𝑠.

Moreover, to form sLET intervals, we can combine non-temporal transitions followed by a temporal one:

𝐶 ⊢ 𝑡 -→ 𝐶 1 ⊢ 𝑡 1 -→ . . . 𝐶 𝑛-1 ⊢ 𝑡 𝑛-1 =⇒ 𝐶 𝑛 ⊢ 𝑡 𝑛 𝐶 ⊢ 𝑡 =⇒ 𝐶 𝑛 ⊢ 𝑡 𝑛 3.
2.2 Sources and Clocks. While sources are considered as inputs in the semantics, PsyC clocks can be defined using three operators:

• Source(𝑐) which gives the source from which clock 𝑐 is derived; • Π(𝑐) which gives the absolute period (in source ticks) of clock 𝑐 with respect to its source; • Φ(𝑐) which gives the absolute offset (in source ticks) of clock 𝑐 with respect to its source. Additionally, to avoid keeping an unbounded date for each source, we assume that 𝑑 𝑐 gives the (current) date of c modulo its period. It is defined as 𝑑 𝑐 = (𝑑 𝑠 -Φ(𝑐)) 𝑚𝑜𝑑 Π(𝑐) with respect to its corresponding source date 𝑑 𝑠 .

Semantics rules of agent.

The three following rules describe the basic statements of PsyC. skip does not make time progress and is rewritten to itself while the assignment and the next are defined in the same way but update their environment accordingly.

𝐶 ⊢ skip -→ 𝐶 ⊢ skip (nothing) 𝐸, 𝑏,𝑇 ⊢ 𝑥 := 𝑓 (𝑒𝑥𝑝+) -→ 𝐸 [𝑥 ← [[ 𝑓 (𝑒𝑥𝑝+) ]] 𝐸 ], 𝑏,𝑇 ⊢ skip (assign) 𝐸, 𝑏 1 ,𝑇 ⊢ next 𝑏 2 -→ 𝐸, 𝑏 2 ,𝑇 ⊢ skip (next)
The advance statement however is more complex. It performs the two following steps:

• it makes time progress with a duration computed using the corresponding clock state 𝑑 𝑐 . • and it updates the available outputs to the ones computed during the interval.

𝑁 = 𝑛 × Π(𝑐) -𝑑 𝑐 𝑇 ′ = UpdateOutputs(𝐸) 𝑠 = Source(𝑐) 𝐸, 𝑏,𝑇 ⊢ advance 𝑛 with 𝑐 =⇒ 𝑁 ×𝑠 𝐸, 𝑏,𝑇 ′ ⊢ skip (advance)
Based on these basic rules, control statements can be described easily. Rules if-1 and if-2 describe the rewriting of the condition statement when respectively the condition expression is true or false. Similarly, rule while-1 and while-2 describe the rewriting of the while statement. Finally, rule seq describes the rewriting of the sequence statement which rewrites its first part until it is terminated. Then, it is rewritten to its second part.

GN C GN C F ast F ast 1 F ast 2 F ast 3 [GN C, F ast] [GN C @ 20, F ast] [GN C @ 10, F ast] [GN C,F ast]
[[ 𝑒𝑥𝑝 ]] 𝐸 ≠ 0 𝐸, 𝑏,𝑇 ⊢ if (𝑒𝑥𝑝) 𝑠 1 else 𝑠 2 -→ 𝐸, 𝑏,𝑇 ⊢ 𝑠 1 (if-1) [[ 𝑒𝑥𝑝 ]] 𝐸 = 0 𝐸, 𝑏,𝑇 ⊢ if (𝑒𝑥𝑝) 𝑠 1 else 𝑠 2 -→ 𝐸, 𝑏,𝑇 ⊢ 𝑠 2 (if-2) [[ 𝑒𝑥𝑝 ]] 𝐸 = 0 𝐸, 𝑏,𝑇 ⊢ while 𝑒𝑥𝑝 do 𝑠 -→ 𝐸, 𝑏,𝑇 ⊢ skip (while-1) [[ 𝑒𝑥𝑝 ]] 𝐸 ≠ 0 𝐸, 𝑏,𝑇 ⊢ while 𝑒𝑥𝑝 do 𝑠 -→ 𝐸, 𝑏,𝑇 ⊢ 𝑠 ; while 𝑒𝑥𝑝 do 𝑠 (while-2) 𝐶 ⊢ 𝑠 1 -→ * 𝐶 ′ ⊢ skip 𝐶 ⊢ 𝑠 1 ; 𝑠 2 -→ 𝐶 ′ ⊢ 𝑠 2 (seq)
The statement rules defined above can then be used to describe the semantics of agents. For that, body can be rewritten to a loop containing a sequence of if statements (one for each body). The research report [START_REF] Siron | Formal Semantics of the PsyC language[END_REF] describes the whole semantics of the PsyC language considering more advanced body constructs like early exit (e.g. equivalent to Esterel trap).

The parallel product is very similar to the synchronous one in the general case considering that the start and the end of sLET interval are synchronous instants. However, when all clocks are based on a unique source, then it can be defined as a sequence of intervals with some duration in which each agent is either in a global state (i.e. the start or the end of one of its interval) or in an intermediate state due to the overlapping with an other agent as illustrated in Figure 3.

SYNCHRONOUS SEMANTICS OF SLET 4.1 Description

The global idea comes from the following observation: for a given task, the sLET paradigm is equivalent to a synchronous model in which the communication model is delayed. By moving up all computations to the start of the sLET interval, the small-step semantics masks the ability to dispatch them all along. The main role of small-step semantics is therefore to allow the reuse of development environments based on SR languages. More generally, part of this work must be understood as an attempt to draw a precise semantic link between existing languages, emphasizing the place of synchronous LET in the making. The synchronous translation is based on the following pattern: 1) on the activation instant, the inputs are read, the computation is done synchronously, and the output is saved in an internal state; 2) we then wait for the specified duration; and 3) finally, the outputs generated during the interval are displayed and made visible to other tasks on the last instant.

Structural Translation of PsyC to Esterel

To illustrate the approach above we propose in this article a structural translation of PsyC to the synchronous language Esterel. We chose Esterel because its syntax is very close to PsyC. It's mainly control-flow and imperative. In particular, the advance statement is very similar to the Esterel await statement. While a data-flow synchronous language such as Lustre has more available and upto-date tools today for analysis, the translation of PsyC to Lustre is far more complicated as the control-flow needs to be flattened. However, the circuit semantics of Esterel describes a data-flow representation of its semantics, which could be represented in Lustre.

The global idea of the translation is to represent PsyC clock and source ticks with Esterel signals and PsyC temporal variables with Esterel valued signals as well as Esterel variables to handle private agent copies. Based on that, agent can be translated, almost as is, with PsyC advance statement translated to the Esterel await statement. The translation rules are as follows: PsyC skip is just translated by: nothing PsyC assignation of temporal 𝑥, 𝑥 := 𝑒𝑥𝑝 is translated by:

private_temporal_x := 𝑇 (𝑒𝑥𝑝 )
PsyC assignation of variable 𝑥, 𝑥 := 𝑒𝑥𝑝 is translated by:

var_x := 𝑇 (𝑒𝑥𝑝 )
PsyC next statement, next 𝑏, is translated by: next_body := 𝑏 PsyC statement's advance, of the form advance 𝑛 with 𝑐 and assuming var1, var2 . . . varN are all the temporal variables in output of the agent, is translated by: await n c ; emit temporal_var1 ( private_temporal_var1 ); emit temporal_var2 ( private_temporal_var2 ); ... emit temporal_varN ( private_temporal_varN );

Control structures are translated into their equivalent form in Esterel without any difficulties, so they are not given here. The global translation scheme of an agent then directly results from the translation patterns defined above. Its module interface is composed of temporal variables (inputs and outputs) which are translated to Esterel valued signals and PsyC clocks which are translated to Esterel pure signals. As an illustration, the Listing 3 shows how the PsyC implementation of the task 𝐺𝑁𝐶 described in Listing 2 is translated using the rules above.

Equivalence relation with the native semantics

Based on the introduced PsyC semantics and its Esterel translation, this section gives an observational equivalence between them for individual agents. First of all, let us define the Esterel operational semantics coming from [START_REF] Potop-Butucaru | Constructive Operational Semantics[END_REF] as following:

Definition 4.1 (Esterel semantics). Given a constructive Esterel program 𝑃 and a set of 𝑑𝑎𝑡𝑎, the semantics of its macro-step is given by the following relation:

𝑃, 𝑑𝑎𝑡𝑎 𝐸 𝑜 --→ 𝐸 𝑖 → 𝑃 ′ , 𝑑𝑎𝑡𝑎 ′
where 𝐸 𝑖 and 𝐸 𝑜 are respectively the input and output signal set active on the current reaction.

The equivalence theorem yields naturally from both semantics (PsyC and Esterel) and some data equivalence relation. Considering a sLET interval, the theorem states that both the PsyC and the Esterel representation have an equivalent behavior on the boundaries of the interval. The PsyC semantics yields only one transition while the Esterel semantics yields a sequence of unitary transitions (i.e. with respect to some source). If both data representations are equivalent at the start of the interval, then, they are also equivalent at the end. An extended proof will be available in the report [START_REF] Siron | Formal Semantics of the PsyC language[END_REF]. Theorem 4.2. For all PsyC agent 𝑝 𝑎𝑔 and the Esterel translation 𝑇 and for any agent transition of the form:

𝐶 ⊢ 𝑝 𝑎𝑔 =⇒ 𝑛×𝑠 𝐶 ′ ⊢ 𝑝 ′ 𝑎𝑔
Assuming, 𝐶 ≈ 𝑑𝑎𝑡𝑎 and 𝑠 ∈ 𝐸, we have an equivalent sequence of Esterel transitions:

𝑇 (𝑝 𝑎𝑔 ), 𝑑𝑎𝑡𝑎 --→ 𝐸 → 𝑃 1 , 𝑑𝑎𝑡𝑎 1 . . . --→ 𝐸 → 𝑃 𝑛 , 𝑑𝑎𝑡𝑎 𝑛
with 𝑇 (𝑝 ′ 𝑎𝑔 ) = 𝑃 𝑛 and 𝐶 ′ ≈ 𝑑𝑎𝑡𝑎 𝑛 Proof. By structural induction on native rules structure □

DISCUSSION

As mentioned earlier, the dual semantic presentation (native and synchronous) was meant to target two distinct further design paths: real-time scheduling models lead to efficient multicore compilation based on schedulability analysis; synchronous reactive extensions yield verification techniques mostly based on model-checking of synchronous models. Note that, currently, each path is somehow weak for covering the other goal: SR expansion do not preserve WCET features and computations become instantaneous; RTS models do not exactly fit with existing verification formalisms and need further encoding. We now comment briefly on experiments in these two directions.

Compilation

Currently, the efficient PsyC compilation chain restricts to monosource programs, corresponding to a single global clock (as in Lustre or LET), but where affine clock down sampling is still allowed in multi-rate specifications. The compiler may then flatten all interval durations on the single source, and then checks real-time schedulability along with WCET inputs. A last issue remains when the actual interval value is data-dependent, as in the following case: The current compiler treats this case by looking for a uniform solution that satisfies the shortest delay (i.e. 10 ms), relaxing this constraint afterward (i.e. 30 ms when going to the "else" branch). However, we view this problem has a general issue for future work, especially in the case of multi-source systems.

Verification

Since PsyC systems cannot deadlock or support clock preemptions, verification efforts consist mainly in establishing the correctness of logical timed properties such as latencies. These are expressed as synchronous observers, in our case using the Clock Constraint Specification Language CCSL [START_REF] André | Verification of clock constraints: CCSL Observers in Esterel[END_REF]. In the "simple efficient compilation case" as described above, verification models such as simple Timed Automata or even Integer Linear Programming solvers could be considered. However, in the general case the mix of boolean logic and integer duration constraints will require mixed-techniques, such as SAT/SMT or BDD. As ongoing work, we focused so far primarily on NuSMV [START_REF] Cimatti | NuSMV: a new symbolic model checker[END_REF] and Prover PSL model-checkers [START_REF]Prover Technology[END_REF]. PSL is an industrial model-checker, developed by Prover, heavily used to demonstrate safety of railway systems. Partial results are listed in Figure 4 conducted on two simple but representative PsyC case studies (both composed of 5 agents) from a benchmark suite coming from [START_REF] Suryadevara | Verifying MARTE/CCSL mode behaviors using UPPAAL[END_REF]: an Anti-Lock Braking System (ABS) and a Temperature Control System (TCS). The results for both tools are satisfying, even in the more complicated setting of ABS1-3 in which a slow mode involves long durations. More advanced results are expected in future work.

Requirement

NuSMV (s) Prover PSL (s) TCS1 (Causality)

CONCLUSION

We showed how semantic background from Synchronous Reactive Languages and Real-Time Scheduling task models could respectively allow providing a small-step and big-step meaning to PsyC, or alternately how the PsyC language could be seen as an exploitation of these notions in a commercial framework. We showed the two semantics to coincide on agent synchronization points (i.e. interval boundaries). These ideas are strongly indebted to the Logical Execution Time design philosophy, emphasizing the potential use of sporadic events as logical clocks syntactically involved in reactive language constructs. We hope this common ground will help better understand efficient multicore compilation as well as efficient timed verification and analysis in the future.

Figure 2 :

 2 Figure 2: Possible timeline of the GNC task in nominal mode.

Figure 3 :

 3 Figure 3: Agent network semantics

Figure 4 :

 4 Figure 4: Verification results in seconds of a subset of requirements of two use-cases coming from[START_REF] Suryadevara | Verifying MARTE/CCSL mode behaviors using UPPAAL[END_REF].

  clock 𝑐 1 = 𝑛 1 × 𝑐 2 + 𝑛 2 Abstract syntax of our PsyC subset of two functions 𝑓 () and 𝑔() in which the former interval takes 2 ticks of clock 𝐴 while the latter takes 3 ticks of clock 𝐵.

	application ::= decl*
	decl source temporal clock	::= source | clock | temporal | agent ::= source 𝑐 ::= temporal 𝑖𝑑 = 𝑣 with 𝑐 ::= * ) | 𝑠𝑡𝑚𝑡 1 ; 𝑠𝑡𝑚𝑡 2 | while 𝑒𝑥𝑝 do 𝑠𝑡𝑚𝑡 | if (𝑒𝑥𝑝) 𝑠𝑡𝑚𝑡 2 else 𝑠𝑡𝑚𝑡 3 | advance 𝑛 with 𝑐 | next 𝑏 | skip
		Figure 1:

agent ::= agent 𝑖𝑑 (starttime 𝑛 with 𝑐) 𝑏𝑜𝑑𝑦+ body ::= body 𝑖𝑑 𝑠𝑡𝑚𝑡 stmt ::= 𝑖𝑑 := 𝑓 (𝑒𝑥𝑝


Martin Lefranc Résumé

LE FASCISME EN EUROPE ET SES ENJEUX MÉMORIELS Mémoire du fascisme dans l'extrême droite française

L'extrême droite française est régulièrement stigmatisée pour sa filiation avec les avatars historiques du fascisme. Face aux accusations, elle cherche d'un côté à minimiser les méfaits des fascismes mussolinien ou hitlérien, voire à les réhabiliter ; de l'autre, elle réfute une assimilation jugée trop rapide, et s'empare du terme stigmatisant pour contre-attaquer, en ciblant notamment la gauche et en rappelant les origines socialistes ou communistes de nombreux fascistes. Cette rhétorique ne masque pas le fait que l'extrême droite demeure le seul courant politique qui, en France, a transmis et continue de transmettre, souvent de façon souterraine et marginale, la mémoire du fascisme historique.

 Ill. 1. La Brigade Frankreich (1973)

qui rassemble les droites radicales françaises

  , premier volet d'une trilogie à succès de Jean Mabire sur les SS français, éditée chez Fayard.Il existe en France une mémoire du fascisme, entendue comme la perpétuation du souvenir de groupes ou de figures s'étant réclamées du fascisme, comme les écrivains Pierre Drieu la Rochelle ou Robert Brasillach, au nom de leur appartenance à cette nébuleuse. Cette mémoire s'attache plus généralement aux collaborationnistes politiques, ainsi qu'aux engagés français sur le front de l'Est et dans la SS entre 1940 et 1945. La mémoire du fascisme est aussi celle des régimes nazis et fascistes étrangers, en particulier le III e Reich et l'Italie mussolinienne. Cette mémoire ne se confond pas, ou peu, avec celle du vichysme, ou avec celle d'organisations politiques de droite nationaliste comme l'Action française.Pour l'extrême droite en reconstruction, ces ouvrages sont des éléments d'une contreculture qui se cherche des mythes et des héros. Les nostalgiques du fascisme défendent un nationalisme européen propre à une extrême droite proche des thèses défendues par la Nouvelle Droite à partir des années 1970. Mais la mémoire du fascisme est également relayée par les « nationaux », héritiers du vichysme et du maurrassisme. Par exemple, la Serp, maison de disques dirigée par Jean-Marie Le Pen, publie à plusieurs reprises, dans les années 1960-1970, des disques compilant des chants militaires nazis, ou des discours de dirigeants du III e Reich. Après leur publication, J.-M. Le Pen et plusieurs de ses collaborateurs sont condamnés en 1968 pour « apologie de crimes de guerre ». Au-delà de leur aspect provocant, ces disques sont d'abord des objets mémoriels destinés à un public de nostalgiques du fascisme qui, à l'époque, gravitent dans les mouvements d'extrême droite et contribuent à leur unification.Dans le premier Front national, créé en 1972, on trouve de nombreux anciens collaborateurs, comme Pierre Bousquet ou Léon Gaultier, qui furent Waffen-SS pendant la guerre. Dans ses premières années, le FN catalyse les mémoires blessées des anciens Les lieux de mémoire du fascisme sont aussi européens ; l'extrême droite française participe régulièrement aux événements organisés par les nostalgiques du fascisme dans les pays voisins. Le pèlerinage annuel à Predappio, village natal de Mussolini, voit parfois le déplacement d'un contingent français en Italie. On trouve également des néofascistes français dans le cortège néonazi qui, chaque 13 février à Dresde, commémore le bombardement de la ville par les Alliés en 1945. Ces deux hommages annuels ont connu un succès croissant dans les années 2000 et 2010, au point de rassembler des milliers de personnes, dans un contexte d'essor des droites radicales en Europe. Le nationalisme européen des militants néofascistes français s'attache à des figures passées aussi diverses que José Antonio Primo de Rivera, fondateur de la Phalange espagnole, ou Léon Degrelle, principal représentant du fascisme belge. Ce fonds mémoriel, qui s'incarne dans des pratiques, participe à une culture militante des droites radicales.Quant au Rassemblement national de Marine Le Pen, il a voulu rejeter clairement l'héritage du fascisme en repoussant à ses marges les éléments radicaux, susceptibles de véhiculer cette mémoire. Ponctuellement, ses militants s'inscrivent même dans la filiation de figures historiques de la lutte contre le fascisme : en 2016, une campagne d'affichage du parti indique ainsi que « Léon Blum voterait Front national ». Dans le même temps, le maire de Béziers Robert Ménard s'inscrit dans la filiation de Jean Moulin. La mémoire du fascisme reste donc marquée d'infâmie, et sa perpétuation demeure le fait d'acteurs marginaux dans le champ politique.

	Une mémoire de « réprouvés »
	Une mémoire européenne
	Dans ce contexte, quelques passeurs transmettent la mémoire de l'expérience fasciste dans
	l'extrême droite groupusculaire de l'après-guerre. C'est le cas de Marc Augier, dit Saint-
	Loup (1908-1990), ancien volontaire sur le front de l'Est et Waffen-SS qui, dès la fin des
	années 1940, recourt au genre romanesque pour diffuser ses souvenirs du combat armé aux
	côtés des nazis. Il centre son récit sur la geste héroïque des combattants français, sacrifiés
	sur l'autel d'une Europe unie contre le bolchevisme. À partir de la décennie 1960, ce sont
	les héros des romans de Jean Mabire (1927-2006), auteur proche de la mouvance
	néofasciste, qui incarnent le combat pur et valeureux des engagés français sur le front de

l'Est (Ill.1). Vendus à plusieurs dizaines de milliers d'exemplaires dans les années 1970, les livres de Mabire, derrière le paravent de la fiction, perpétuent la mémoire d'un engagement réprouvé, et cherchent à dissocier la mémoire du fascisme français de celle du nazisme, à l'heure où l'opinion française est sensibilisée à l'ampleur du génocide des Juifs d'Europe.

Une référence fascistes, vichystes et nostalgiques de l'Algérie française. Jusqu'à la mort du numéro deux François Duprat en 1978, les militants se réclamant de l'héritage du nazisme forment une tendance structurante au sein du parti. Hors du FN, certains groupuscules se présentent comme les héritiers de mouvements fascistes de l'entre-deux-guerres, comme l'OEuvre française, fondée en 1968 par l'ancien milicien Pierre Sidos, qui s'inspire du Mouvement franciste, mené par Marcel Bucard entre 1933 et 1944 (parades en uniforme, entrainements armés en vue d'un coup d'État fantasmé). Certains lieux de mémoire du fascisme français permettent également de fédérer les droites radicales dans leur diversité. L'homme de lettres et journaliste collaborationniste Robert Brasillach, fusillé le 6 février 1945, fait ainsi figure de martyr pour une grande partie de ces courants. Il incarne aux yeux de ces groupes, encore aujourd'hui, la figure du « mort pour la cause » susceptible de fédérer un camp politique. Le poète est tombé pour un « idéal » ; la « pureté » de ses convictions fascistes est toujours dissociée des conséquences du fascisme, toujours perçues comme des « dérives regrettables ».

Au lendemain de la Seconde Guerre mondiale, la plupart des anciens fascistes sont morts, ou végètent en prison. Beaucoup d'entre eux sont rendus inéligibles. En plus de la législation de 1881, la loi de 1949 sur les publications destinées à la jeunesse, bientôt suivie de la loi Pleven en 1972 condamnant la provocation à la haine raciale, forment un arsenal juridique par lequel l'État cantonne aux arrière-boutiques les publications à la gloire du fascisme. La mémoire du fascisme en France est donc, dès l'origine, entravée dans son expression publique.En détention, les anciens fascistes trouvent dans le réconfort du groupe les ressources pour construire une mémoire souterraine, victimaire, fondée sur le sentiment d'avoir été injustement punis par des « Résistants de la dernière heure ». Comme pour la mémoire du vichysme, l'Épuration constitue l'expérience fondatrice de la mémoire du fascisme en France. À leur sortie de prison, permise en partie par les lois d'amnistie comme celle de 1953, les fascistes français forment un petit entre-soi replié sur lui-même. Quelques personnages, comme MauriceBardèche (1907Bardèche ( -1998)), beau-frère de Brasillach et père du négationnisme français, jouent un rôle central dans la reconstitution, dans la sphère privée, d'une sociabilité née de l'Épuration, qui entretient la mémoire française du fascisme.


Moise Deroh

Erwan Lucas

Bertrand Kibler

W Liang

V S Ilchenko

D Seidel

T W Bendahmane

T Herr

V Brasch

J D Jost

C Y Wang

N M Kondratiev

X Xie

M Jiang

Xiao

Dispersion engineering in Brillouin fiber laser cavity for Kerr frequency comb formation

We conduct numerical and experimental investigations on Kerr comb generation in a nonlinear and nonreciprocal fiber cavity by leveraging both stimulated Brillouin backscattering and cascaded four-wave mixing. By engineering the net cavity dispersion to be either normal or anomalous, we enable the formation of diverse patterns and localized structures in the cavity field. The comb's properties depend crucially on the mismatch between the frequency spacing of the bichromatic pump and the free spectral range of the Brillouin laser cavity in both cases. Particularly, in the anomalous regime, adjusting this parameter yields coherent, stable frequency combs in the modulation instability regime. This allows control and expansion of the spectral bandwidth up to 2 THz in normal dispersion and to 6 THz under anomalous net dispersion. This versatile and easily reconfigurable method holds potential for applications in high-speed communications and microwave synthesis.

INTRODUCTION

Optical frequency combs (OFCs), comprising a series of equally spaced coherent lines in the frequency domain, have found widespread use in a wide panel of applications encompassing optical frequency metrology, spectrograph calibration, microwave generation, and beyond [1]. OFCs originate from various sources, including mode-locked lasers [2], electro-optic modulation [3,4], and passive nonlinear resonators [5]. The latter, using the formation of dissipative temporal cavity solitons in microresonators [6], generates smooth OFCs at high repetition rates, ideal for optical communications and LIDAR systems.

The pursuit of Kerr combs has not been confined to these traditional optical platforms. While early work on microresonators showed a competition between Kerr and Raman or Brillouin scattering [7], a novel approach has recently emerged, demonstrating the generation of soliton-based combs leveraging Brillouin lasing [8,9]. In this paradigm, the Brillouin gain in the cavity gives rise to counterpropagating Brillouin lasing [10] that serves as the coherent driving force behind Kerr comb generation. This paradigm has been extended to fiber cavity Brillouin lasers under bichromatic pumping, to trigger Kerr comb forma-24 tion at a high repetition rate while using a long cavity [11][12][13]. 25 Intriguingly, this dual-pumping configuration bestows an ad-26 ditional degree of freedom for manipulating cavity dynamics, 27 specifically the frequency mismatch between the comb repetition 28 rate and the cavity's free spectral range (FSR) [14,15], which had 29 not been investigated so far in these systems.

30

In this letter, we investigate the intricate interplay between The first segment is amplified using an erbium-doped fiber am- whose line spacing matches that of the initial Kerr comb, with a 180 frequency offset [23]. These sub-combs can be still synchronized, 181 under appropriate detuning conditions, to form one globally 182 coherent comb [24], which is shown in fig. 3e. This optimal 183 Brillouin pumps spacing is commensurate with the cavity's FSR, and new specialty fiber materials with strong nonlinearity.

EXPERIMENTAL SETUP AND RESULTS

31stimulated

  Brillouin scattering (SBS) and cascaded four-wave 32 mixing (FWM) in the nonlinear fiber cavity, to achieve coher-33 ent and stabilized frequency combs. We experimentally study 34 and numerically validate the impact of the frequency mismatch 35 parameter on the comb dynamics, and specifically its spectral 36 shape and bandwidth. In addition, we perform this analysis in 37 both normal and anomalous group velocity dispersion regimes, 38 since the net fiber cavity dispersion can be easily adjusted by 39 inserting a short fiber segment in the cavity. In each case, the 40 generation of switching waves or localized structures through 41 modulation instability (MI), from the initial bichromatic sinu-42 soidal modulation pattern, is investigated and characterized in 43 the spectral and temporal domains.

  44

  Fig. (a) Experimental setup for Kerr combs generation in a dual-frequency Brillouin fiber laser cavity (green rectangle) benefiting from the phase-locked stabilization loop diagram (purple rectangle). CW: Continuous wave, Polarization controller, IM: Intensity modulator, FC: Fiber coupler, EDFA: Erbium-doped fiber amplifier, OC: Optical circulator, SBS: Stimulated Brillouin scattering, FWM: Four wave mixing, OSA: Optical spectrum analyzer, PD: Photodiode, RFA: Radio frequency amplifier, ESA: Electrical spectrum analyzer, LO: Local oscillator, FPGA: Field-programmable gate array. (b) Principle of the offset sideband-locking for the Brillouin gain spectrum detuning scan.

Fig. 2 .

 2 fig.1b). Changing f synth = ∆ν/2 hence controls δΩ 2 and thereby 91

160B.

  fig.3b, provide good agreement with the experiment and help 173

184213Fig. 3 .

 3 scheme is the ability to easily change and reconfigure the disper-219

"Investments for the Future" operated by the National Research Agency 230 (EIPHI Graduate School, contract ANR-17-EURE-0002), and from Région 231 Bourgogne Franche-Comté and European Regional Development Fund.

Funding. The authors acknowledge support from French program