Fabien Siron

Dumitru Potop-Butucaru

Robert De Simone

Damien Chabrol

Amira Methni

Formal Semantics of the PsyC language

Keywords: Real-Time Systems, Multiform Logical Time, Logical Execution Time, Formal Semantics Semantique formelle du langage PsyC Système Temps-Réel, Temps Logique Multiforme, Temps d'Exécution Logique, Sémantique Formelle

Time must be taken into account from the very start of the design of real-time systems. Because exact computation durations are usually not available in early design phase, multiple formalisms based on the concept of Multiform Logical Time have been introduced. The synchronous approach introduced a discretized abstraction of time based on logical clocks, on which computation happens logically instantaneously. While being very expressive, the synchronous approach suffer from compilation issues when mapping logical time to non-negligible real-time computation durations. In answer, the Logical Execution Time (LET) paradigm has been introduced to give such a compromise between the strong expressiveness of the synchronous approach and traditional task scheduling, making LET a perfect fit for the temporal architecture and the software integration of real-time systems. In this report, we consider a variation of LET extended with logical clocks, namely synchronous LET (sLET), implemented in the industrial language PsyC. The sLET approach -and thus PsyC -allows to specify computation to be executed inside a logical interval up to the next occurrence of a logical clock expression (i.e. in opposition to a constant duration). As sLET is based on both LET and the synchronous approach, we give in this report two operational semantics of the PsyC language: a native semantics (or big-step) based on the Structural Operational Semantics approach (S.O.S.) and a synchronous semantics defined by translation to the Esterel language. The former gathers all valid computation schedulings as an equivalence class, of which the latter provides a specific representative (as-soon-as-possible execution). We show the semantics equivalence of those two semantics at interval boundaries. While the native semantics is mainly used for compilation, future work will show how logical timing properties can be verified using those two semantics.

Conclusion and Future Work 33 1 Introduction

Safety-critical real-time systems have to handle time in a predictable manner. That is, specified temporal requirements from the system specification should still hold in the final system. It is clear that time must be taken into account from the very start of the design. However, exact timing constants, e.g. 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 those real-time durations. Then, specific analysis, usually called schedulability analysis (or time safety analysis) fill the gap between logical and physical time, that is, they ensure that physical computations satisfy their logical time constraints.

The Synchronous-Reactive approach (SR) introduced a discretized abstraction of time based on logical clocks in which 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, 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 so-called "Long Task Problem". When different tasks of different rhythms are compiled, execution time variability is usually limited to a common cycle rate. More recently, the Logical Execution Time (LET) paradigm has been introduced to give a compromise between the strong expressiveness of the synchronous approach and the efficiency of traditional task scheduling [START_REF] Kirsch | The logical execution time paradigm[END_REF]. 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 communication can only happen on its bounds. That is, inputs can only be consulted at the start of the interval and outputs can only be made visible to other tasks at the end. Consequently, as communication can only be made at predefined instants, LET ensure the temporal determinism property. In this report, we call synchronous Logical Execution Time (sLET), a variation of the classical LET paradigm in which interval bounds are based on logical clock ticks, as in the synchronous approach. As a consequence, the duration of an interval is specified as being "up to the next n th tick" of a logical clock. It should be noted that such duration could not be constant across all reactions as it is specified relatively to a clock. In the simple case where there is only one universal clock used, then all logical durations become constants as in the case of the original LET paradigm. This makes sLET supersedes original LET. sLET (as classical LET) allows multiple valid schedule taking into account physical time that are mutually equivalent with respect to logical ticks. The synchronous semantics we give in this report is actually one of those in which computation happens logically synchronously to the start of sLET intervals and outputs are delayed to their end.

The sLET paradigm is implemented in the PsyC language which is an industrial language, developed by the company Krono-Safe, dedicated to the design of real-time safety-critical software [1].This reports introduces two operational semantics for PsyC execution: a native semantics is expressed in the celebrated structural operational semantics (SOS) format due to Gordon Plotkin [START_REF] Plotkin | A structural approach to operational semantics[END_REF]. This semantics could be qualified as big step since, for individual agents, it builds a single transition for a whole duration interval between two successive interval boundaries, called Temporal Synchronization Points (TSP). The case of composite networks (of agents) is slightly more complex, involving intermediate states, as time intervals in distinct agents may not terminate on the same instants. However, the dispatch of exact execution times for elementary computations are irrelevant, as long as they do not exceed prescribed interval boundaries. This semantics consider a native communication means using a valued event (e.g. similar to Esterel valued signal) that can be extended to multiple communication channels : temporal variable (i.e. a sampled shared variable) and stream (i.e. a fifo channel). in contrast, the second semantics called synchronous semantics expands temporally all behaviors onto the baseline discrete synchronous step and can thus be qualified as small step). It is defined by translating programs in a structural fashion into Esterel synchronous expressions. In essence it acts as if computations were all performed in the initial interval instant (but with effects remaining local), then waiting for the prescribed interval duration to terminate and show results, much as in discrete-event simulation frameworks, and respecting the LET philosophy.

Because computation effects can only be visible at interval boundaries (i.e. on TSPs), the second semantics can be abstracted and formally proven observationally equivalent to the first at this level. Consequently, it allows to retrieve compilation and verification techniques that have been defined for "pure" synchronous languages.

The outline of this report is organized as follows. Section 2 defines the synchronous Logical Execution Time paradigm and discuss its properties. Then, section 3 introduces the syntax of the PsyC subset considered in this report as well as some examples. Its native (or big-step) semantics is given in section 4 and 5 describing respectively the semantics of an individual agent and the semantics of a network of agents along with communication means. Section 6 defines an the synchronous semantics by translation to the Esterel language. Section 7 shows an equivalence criteria between both semantics and section 8 illustrates that result using a simple avionics case-study. Finally, section 9 discuss some implementation issues, due to the semantics, of some PsyC patterns.

Synchronous Logical Execution Time

Multiform Logical Time

The essential assumption of Logical Time is that time can be discretized according to a notion of base step (or instant), which is a subdivision of any behavior, and form the support for atomic reactions. Multiform Logical Time design, then, relies on the fact that designers can express timing of events using those logical clocks.

In this report, we call logical clock a totally-ordered sequence of events or instants at which it ticks [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF]. They are used to measure event occurence dates in a system by replacing physical dates by logical sequencing. As such, they can be defined by some monotonic function from integer to integer as well as some boolean sequence that express at which instant they tick. The former representation could then be used to define algebraic constraints that will seek a solution by an assignment of instants to clock ticks, corresponding in general to a particular schedule resulting from logical time design constraints. In synchronous languages, as well as in synchronous LET, logical clocks are usually related by some expressions or constraints. Thus, they are partially ordered. Definition 1. A logical clock c is defined by an infinite totally-ordered sequence (t i ) i∈N . A finite set of clock C can be constrained using precedence and simultaneity relations (e.g. periodicity).

Logical clocks can be associated with any events. Consequently, synchronous languages like Esterel use them to represent any countable units like seconds, meters, laps . . . As any units Inria (or sequence of events) can represent a unique logical time, the concept has been called multiform logical time in the litterature. As an automotive exemple, an engine can be modeled using two main logical clocks, one that describes a discrete physical clock and one that describes the angular position of a crankshaft. Note that many concrete engineering frameworks that use a the simple notion of nano or milli -second to break down atomic steps fall into this category, as long as these units are only used to express constraints/requirements put on specifications; in general, logical time step need not be associated to a pseudo-physical unit. Note, also, that the same abstract discretization assumption is reported in the notion of tagged-systems [START_REF] Lee | The tagged signal model-a preliminary version of a denotational framework for comparing models of computation[END_REF]. While classical LET approaches does not really build on logical clocks and multiform logical time, the sLET paradigm builds on both approaches in the same spirit as classical synchronous languages.

Functional and temporal determinism

It is highly desirable for industrial time-critical systems that they behave in a functionally deterministic (reproducible) and temporally deterministic (predictable) manner. Determinism can be sorted as internal; or external, depending on its source: internal non-determinism may rise from the fact that conditions on values guarding the control flow choices are uninterpreted. This is usually the case in early design phases, and at compilation time, when programs represent their whole sets of different executions. Internal functional non-determinism may lead to temporal non-determinism, as distinct execution branches may "cost" different durations; external non-determinism may come from uncertainly on input/clocks arrival times; if a sequential component is allowed to be sensitive to more than one input that may occur concurrently, then whichever arrives first may disable the dependance on others, together with their effects. Requesting the absence of such conflicts has been considered under many names in different frameworks (of input guards in CSP, conflict-freeness in Petri Nets, monotonicity in Kahn Process Networks, latency-insensitity in high-level hardware synthesis languages, endochrony in reactive synchronous formalisms . . . ). It is important to note here that temporal external non-determinism can lead to functional non-determinism as well, with phenomena known as timing anomaly at microarchitecture level [START_REF] Lundqvist | Timing anomalies in dynamically scheduled microprocessors[END_REF] or priority inversion in real-time scheduling theory [START_REF] Reineke | A definition and classification of timing anomalies[END_REF].

Enforcing uniform time boundaries at early design time level, as a requirement that will have to be respected and enforced later by implementation, is the main purpose of so-called Logical Exceution Time (LET) formalisms. Since the timing values used at this level do not need to be expressed in terms of physical time (which at this level is just as arbitrary values as any other sporadic events), then synchronous reactive languages (that were meant originally to prescribes exact activation logical instants), can be interpreted to provide boundary interval instants. This leads to the combination of synchronous LET (or sLET) described below.

The synchronous Logical Execution Time paradigm

Classical Logical Execution Time, introduced in languages such as Giotto [START_REF] Kirsch | The logical execution time paradigm[END_REF] or TDL [START_REF] Pree | Modeling with the timing definition language (tdl)[END_REF], basically defines the logical duration a task have to fulfill. This forms logical intervals in which communication can only happen on its bounds. Inputs are read at the beginning of the LET intervals while outputs are made visible at the end of them. Consequently, exact computation duration is totally abstracted by the logical duration of the interval. This ensures that, assuming that computation fits in the interval, temporal behavior is completely deterministic. Synchronous Logical Execution Time (sLET) extends the classical LET paradigm with the concept of logical clocks. A logical clock, in the sense of Lamport [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF], abstracts time through a series of totally-ordered event called clock ticks. These logical clocks can be either related or not. While in classical LET, interval duration is specified using a constant fixed duration (i.e. usually chronometric), in synchronous LET, interval duration can be specified relatively to clock ticks. Let's define more precisely what we mean by logical interval: Definition 2 (Elementary Action). A logical interval (or elementary action) is defined as a computation constrained by: an activation date d esd defined on a logical clock c start , on which input can be read; a termination date d ddl defined by a number of ticks of a logical clock c ddl on which outputs are made visible.

They both define synchronous instants called Temporal Synchronization Points (TSPs).

As an illustration, assume we have two clocks, M S and S related with an periodic relation; S ticks each 1000 M S ticks. Let's define advance n with c to be a synchronization of n ticks of clock c (which will be detailed in the next sections). In our paradigm, advance 1 with MS; advance 1 with S; is not equivalent to advance 1 with MS; advance 1000 with MS;. The former one describes a logical interval which starts on M S and lasts up to the next S tick (i.e. the exact duration can vary depending on when the interval has started) while the latter one describes a logical interval lasting exactly 1000 ticks of M S (i.e. the exact duration is fixed). This shows that a LET semantics based on multiple logical clocks (i.e. based on the Multiform Logical Time concept) provide more expressivity. While less used in the industry, the constraints can also be multiform in the sense that logical clocks can represent any event sequence. However, note that, while TSPs inherit their definition from the synchronous approach, the communication model still behave as in the classical LET paradigm, allowing a more flexible compilation.

Let's define the schedule of an sLET interval to be its corresponding computations that can happen anywhere in its interval with any physical duration. A schedule is said to be valid if the computation fits in their sLET interval. sLET (as well as classical LET) actually admits a whole class of different valid schedule that are observationally equivalent, i.e. they have the same behaviors with respect to TSPs. It is the role of the compiler to find such a valid schedule given the execution time of the computations (usually a preemptive schedule). However, from the semantics perspective, all valid schedules are strictly equivalent as they give the same observable behavior. Consequently, the synchronous semantics is actually one of those valid schedule where computation is infinitely fast. The synchronous behavior of a synchronous LET interval is then the following:

1. Inputs: On the interval activation, the inputs are read and saved in an internal state synchronously;

2. Compute: The actual computation is done synchronously with the interval activation but the outputs are not updated synchronously. Instead, it is saved in an internal state;

3. Wait: We wait for the interval deadline with respect to some clock expression, similarly to the Esterel await statement;

4. Display: The saved outputs are displayed and made visible to other tasks synchronously.

Hence, synchronous LET (as well as classical LET) have both a native behavior in which computation can happen anywhere in their interval and a synchronous behavior that only models the beginning and the ending of each interval. This motivates our work to define two different semantics of the PsyC language, which is introduced in the next section.

Inria 3 Overview of PsyC

The industrial language PsyC is a language developed by the french company Krono-Safe [1], 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] Chabrol | Oasis: A chain of development for safety-critical embedded real-time systems[END_REF]. The modern version of PsyC can use multiple logical clocks and thus, naturally implements the synchronous LET paradigm.

Logical Clocks In the spirit of the Multiform Logical Time concept, time is defined through the use of logical clocks, that is, totally-ordered sequences of ticks. The PsyC language allows to describe two levels of logical clocks: sources are externally-defined logical clocks, they can be mapped to a timer (i.e. pseudophysical 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 p × c + o with p and o being respectively the period and the offset with respect to another clock or source c. source realtime ; // assuming r e a l t i m e i s 1 ms clock c2 = 2 * realtime ; // c2 t i c k s each 2 ms clock c 4 2 = 2 * c2 + 1 ; // c 4 1 t i c k s each 4 ms s t a r t i n g a t 2

Tasks 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 to synchronize on a tick of a given PsyC clock. They specify both the deadline of preceding code, and the triggering of code following it. Moreover, following the LET semantics, the advance specifies the instants in which communication can happen. As an example, the following code describes an infinite loop (due to the body construction) of two functions f () and g() in which the former interval takes 2 ticks of clock A while the latter takes 3 ticks of clock B. Temporal Variable which 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. Stream which is a buffer shared between multiple producer and one consumer following the FIFO policy (First-In First-Out). Contrary to Temporal Variables, data are not always available (i.e. the buffer can be empty).

Determinism of communication is ensured by the, so-called, Visibility Principle. (see Figure 1). Considering that each exchanged data is timestamped:

1. a data can only be timestamped with a (logical) date greater or equal to its corresponding deadline;

2. a data can be consulted only if its timestamp is lower or equal to the current (logical) activation date;

Theoretically, more communication means can be defined, as long as they respect the visibility principle. However, in practice, Temporal Variable is the most commonly used. For that reason, the formal semantics defined in the next section will give the semantics of a generalized Temporal Variable channel that gives only the primitive to build any communication channel type (i.e. Temporal Variable, Streams or any new channel).

Also, the Visibility Principle can be partially relaxed to simulate synchronous communication. This mechanism, called Null-Latency communication is achieved using a intermediate tick defined on a Fractional Clock. However, as Null-Latency (NL) can be seen as an extension of PsyC, it is not in the scope of the present version of this report. The sLET formal semantics described in the next section is compatible with NL but the synchronous semantics needs more work.

Illustration As an illustration, the listing 2 shows a simple agent with a periodic filtering of an input which depends on a mode which states whether the filtering should be fast or slow. Depending on this, two implementation can be used, FilterFast and FilterSlow. The slow version can perform more heavy computation than the former but introduce an additional delay. This can be necessary, for example, if a system is set to a degraded mode because of a detected error, or if the system is not in a critical phase in which it needs quick reactiveness (e.g. take-off or landing of a plane). Additionnaly, this example shows an other feature of PsyC which is body handling. A body is basically an infinite loop except if one of the following statement is used : next which describes the next body to be executed (by default, itself), endbody which stop the current body execution to go to the next one and jump which immediately jumps to a specified body. In the example, the start body is the initialisation phase of the agent (and is executed only once at the beginning), while the loop body is the nominal phase (and is executed indefinitely).

Abstract Syntax To describe the formal semantics of PsyC in the next section, we first give an abstract syntax of the language. We choose to take a subset of PsyC excluding all advanced expressions and statements of the C language (in fact, most of the C constructions are temporal t mode mode = SLOW with c10ms ; temporal t i n i n p u t with c10ms ; temporal t o u t output with c10ms ;

agent F i l t e r ( starttime 1 with c100ms ) { display output : a l l ; consult 1 $ i n p u t ; consult 1 $ mode ; body s t a r t { F i l t e r I n i t ( ) ; next l o o p ; advance 1 with c100ms ; } body l o o p { i f ( $ [ 0 ] mode == SLOW) { output = F i l t e r S l o w ( $ [ 0 ] i n p u t ) ; advance 3 with c10ms ; advance 1 with c100ms ; } e l s e { output = F i l t e r F a s t ( $ [ 0 ] i n p u t ) ; advance 1 with c10ms ; } } } Figure 2: PsyC implementation of task GNC
not interpreted by the PsyC compiler). The abstract syntax is described in Figure 3. The left column specifies the PsyC constructions defined at the application level (e.g. communication channels, clocks) while the right column describes the PsyC constructions at the agent level. Aside from the syntaxical constructs, the definition of a PsyC application that we consider should respect the following constraints:

A temporal variable can be displayed by only one agent and can be consulted by multiple agents.

We assume that the starttime value could be 0 while advance value could never be 0.

The starting body of an agent is called "start" by convention.

All execution paths inside a body should declare at least an advance statement. We now provide the SOS big-step semantics [START_REF] Plotkin | A structural approach to operational semantics[END_REF] [3] for single agents; the case of agent networks will be dealt with in next section. The semantics amalgamate structurally the run of all elementary computations until (and including) the occurrence of the next advance statement, resulting in a single compound transition for a sLET behavior that lasts the prescribed interval.

= id := f (exp * ) | stmt 1 ; stmt 2 | if (exp) stmt 2 else stmt 3 | while exp [n] do stmt | while exp do stmt | advance n with c | endbody | next b | jump b | nothing exp ::= id | $[n]id
As always with SOS rules, operational transitions can be collected in a transition system, which in the case of PsyC control-flow restrictions is actually a finite state machine (FSM). We first provide necesssary notations (something somehow tedious), then provide in turn SOS rules for the non-temporal control-flow features, then for temporal clocks advancements, and finally for the merge in a single form at the agent declaration level.

Notations

Operational semantics rules are usually given as a relation over a possible rewritting. Let's consider the relation x ---→ x which basically means that a given state x can be rewritten in x (also call the residual) after the transition. In a rule, either the relation is given alone, then it's said to be an axiom or it's given with respect to some assumptions. In this article, inference rules are represented as following:

h 1 h 2 . . . h n x ---→ x (1)
This means that if all assumptions are true (i.e. h 1 , h 2 . . . h n ), then the transition relation can be used. Additionally, the program state has often a program environment that keeps track of the environment valuation. For a given environment E, all declared variables x can have their value accessed using the notation E(x).

Configuration syntax

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

E, T output , b
where E is the private environment of the agent, b is the identifier of the next body to be executed and T ouput is the public environment of the agent. This allows to distinguish values that can be access by other tasks (through the communication mechanism) and values that shouldn't be accessed.

Transition Syntax

The semantics of PsyC is described in this paper using two complementary relations, one for (logically) instantaneous behavior and one that represents time progress in term of logical instants. We shall call the former non-temporal transitions and the latter temporal transitions.

Non-temporal transitions

For non-temporal transitions, the following relation is used:

C t ---→ C t
where C, C denote the agent configuration respectively before and after the transition and t, t denote the agent statements in the same way.

Temporal transitions

Temporal transition are due to advance statements making the time progress and is defined in a similar way:

C t = == ⇒ n×s C t
where n ∈ N * and s is a source denoting a temporal transition that has a duration of n ticks of the source s.

They can be composed with instantaneous statements as long as the sequence of instantaneous transitions terminates with a temporal transition:

C t ---→ C 1 t 1 ---→ . . . C n t n = == ⇒ C t C t = == ⇒ C t
Finally, we note ---→ * the sequence of zero, one or more rules ---→,

Sources and Clocks

Consider the following clock c = n 1 × c p + n 2 where n 1 ∈ N * and n 2 ∈ N. Its semantics is given by the following equations, which give respectively the source, the period and the offset of the clock:

Source(c) = c, if c p is a source Source(c p ), if c p is another clock (clk-source) Π(c) = 1, if c p is a source Π(c p ) × n 1 , if c p is another clock (clk-period) Φ(c) = 0, if c p is a source n 2 × Π(C p ) + Φ(n 2 ), if c p is another clock (clk-offset)
Additionally, to avoid keeping an unbounded date for each source, we assume that d c gives the (current) date of c modulo its period. Note that, for each of these definitions, we assume that clock dependency cannot be cyclic and forms either a tree or a forest, depending on wether a unique source is used or not. if statements terminate instantaneously and are rewritten with the branch selected by the condition.

Semantics Rules

[

[ exp ]] E = 0 E, T, b if (exp) s 1 else s 2 ---→ E, T, b s 1 (if-1) [[ exp ]] E = 0 E, T, b if (exp) s 1 else s 2 ---→ E, T, b s 2 (if-2) Inria 4.5.

While statements

While statements are instantaneous and rewritten the sequence of its body followed by itself if the condition is evaluated to true

[[ exp ]] E = 0 E, T, b while exp do s ---→ E, T, b s ; while exp do s (while-1)
While statements are instantaneous and rewritten to nothing if the condition is evaluated to false.

[

[ exp ]] E = 0 E, T, b while exp do s ---→ E, T, b nothing (while-2)

Bounded while statements

Bounded while statements are instantaneous and behave like classical while except that they have a counter n representing the maximum iteration bound

[[ e ]] E = 0 n > 0 E, T, b while e [n] do s ---→ E, T, b s ; while e [n -1] do s (bounded-while-1) [[ e ]] E = 0 E, T, b while e [0] do s ---→ E, T, b nothing (bounded-while-2) [[ e ]] E = 0 E, T, b while e [n] do s ---→ E, T, b nothing
(bounded-while-3)

Sequence statements

The sequence statement is instantaneous if its first statement terminates instantaneously.

C s 1 ---→ * C nothing C s 1 ; s 2 ---→ C s 2 (seq)
We assume that this rule is extended to also propagate temporal transitions.

Advance statement

The advance n with c is not instantaneous. In fact, it is the only PsyC statement that takes time. Thus, it is rewritten to nothing and takes takes exactly the length specified by the advance statement (with respect to the source clock).

N = Duration(n, c, date) T = UpdateOutputs(E) E = ResetOutputs(E) s = Source(c) E, T, b advance n with c = == ⇒ N ×s E , T , b nothing (advance-1)
As written in the rule above, the Duration function need another date parameter (left undefined in this rule) to convert a deadline relative to a clock tick to an absolute deadline represented as a duration in source ticks.

Additionaly, the UpdateOutputs function extracts all the outputs from the internal environment to the external visible one and the ResetOutputs function removes all the outputs from the internal environment (alternatively, they can be defined to a special non present value like ⊥). This will allow other agents or some communication mechanism to know when an output value has been produced or not. Definition 4 (Logical Duration). Considering a date d s assigned to each source s (and updated at each s source tick), Duration can be defined with respect to a deadline date:

LastTick(c, d) = d -Φ(c) Π(c) Deadline(n, c, d) = Π(c) × (n + LastTick(c, d) + Φ(c)) Duration(n, c, d) = Deadline(n, c, d) -d
However, this definition is not satisfying. First, the formula has unnecessary complexity due to the conversion between clock tick index (e.g. LastTick) and source dates (e.g. Deadline). Secondly, the use of a date require using an unbounded integer which adds a big complexity in the semantics. Indeed, most model-checking techniques require finite state models, and thus, we would need to convert back an infinite model to a finite one.

Let's define an other Duration function using the clock state d c which which is finite:

Definition 5 (Finite State Logical Duration). Duration (n, c, d c ) = n × Π(c) -d c Theorem 1. Let d c (d) = (d -Φ(c)) mod Π(c), then Duration(n, c, d) = Duration (n, c, d c )
Proof. By definition of mod:

d c (d) = (d -Φ(c)) mod Π(c) = (d -Φ(c)) -Π(c) × d -Φ(c) Π(c) ) n × Π(c) -d c = n × Π(c) -(d -Φ(c)) + Π(c) × d -Φ(c) Π(c) ) Duration 2 (n, c, d c ) = Π(c) n + d -Φ(c) Π(c) + Φ(c) -d Duration 2 (n, c, d c ) = Duration 1 (n, c, d)

Body handling

For body handling, we assume that a special body, called current is used only to keep track of rewriting. That is, it's initially a copy of the start body and it is then updated at each source tick of the agent. When it's empty, it's content becomes a copy of the next body.

A body takes time if its content takes time (i.e. typically due to an advance statement). Then, at the next step, the current body will be assigned to the residual statement of the latter.

C B(current) = == ⇒ C stmt B = B[current ← stmt ] C B = == ⇒ C B (body-1)
A body terminates instantaneously if it's content is composed of a sequence of instantaneous relations terminating by a nothing statement. Then, at the next step, the current body will be assigned to the last target body given by b .

C B(current) ---→ * E , T , b nothing B = B[current ← B(b )] C B ---→ E , T , b B (body-2)
Note that we have also, implicitely, a third rule for body in the case of endbody that aborts the current body to start the next one. However, we did not represent it for simplicity.

Agent handling

We then wrap everything in the rules of the PsyC agents.

An agent first transforms its starttime expression into a one that depends only on source tick. Note that, given the specification, the target body b is initially equal to "start".

n > 0 N = Duration(n, c, 0) -1 s = Source(c) C agent id (n with c) B = == ⇒ N ×s C agent id (0 with ) B (agent-1)
An agent with a starttime expression equal to 0 starts the execution of its bodies.

C B = == ⇒ N ×s C B C agent id (0 with ) B = == ⇒ N ×s C agent id (0 with ) B (agent-3)
An agent with a starttime expression equal to 0 with multiple instantaneous relations on its bodies can squash them, as long as they are followed by a non-instantaneous relation.

C B ---→ * C B C B = == ⇒ N ×s C B C agent id (0 with ) B = == ⇒ N ×s C agent id (0 with ) B (agent-4)
A general observation is that PsyC agent are can only do temporal transitions, in other words, they always advance in time.

5 Native sLET semantics of a PsyC agent network

Global states vs intermediate states

The native sLET semantics of PsyC agent is defined quite classically by a transition expressing some rewriting of the agent. However, more interestingly, those transitions also express some (logical) duration with respect to some logical clock (or source clock) which is the foundation of synchronous LET; they allow to express sLET intervals (as well as classical LET intervals).

However, problems arise when building the network of agents. Indeed, in a classical synchronous language, the semantics naturally gives a synchronous composition as each instant have the same duration, that is, the cycle rate. In (synchronous) LET, multiple sLET intervals might have different durations. Consequently, in the native semantics, one cannot express directly the agent composition with only agent states.

To resolve this issue, we shall define two kinds of agent states in the context of an agent network:

1. Global states, which corresponds to the actual agent states from the native semantics (i.e.

the boundaries of an sLET interval) 2. Intermediate states, which corresponds to intermediate states in an sLET interval, typically resulting from the overlaping of the global state of another agent.

Futhermore, multiple agent transitions might have different durations based on different sources. Whereas the composition of multiple agents based on a unique source (but possibly different logical clocks based on the same source) express a total ordering, the composition of multiple agents shall also handles the case of multiple sources expressing a partial ordering coming from external non-determinism. The next section illustrates the different overlapping patterns between agents.

Overlapping patterns

The figure 4 illustrates all the different overlapping patterns between sLET intervals. All the cases have two agents, a blue and a red one executing both an sLET interval (but not necessarily synchronized). For each agent, a filled half circle represents a global state while an empty half circle represent an intermediate state. advance denotes the logical time of the whole interval while remaining denotes the logical time remaining in the current interval, due to overlapping.

The case 4a shows two agents synchronized, they both start and end in a global state;

The case 4b shows one agent (the blue one) longer than the other one, the longer interval shall then be split in sub interval, thus introducing an intermediate state and a remaining time;

In the previous case, both agent still start at the same time. However, in the case 4d, the blue agent is already in the middle of an interval, thus starting in an intermediate state. Nonetheless, they both end synchronously as the remaining time of the blue agent and the logical time of the red one are equal.

The case 4c extends the previous case in having a longer remaining time for the blue agent than the logical time of the red one. Thus, the blue agent starts and ends on intermediate states.

The case 4e is another variation of the two previous cases in which the red agent has a remaining time smaller than the logical time of the blue one. Hence, the blue agent ends on an intermediate state while the red one start on an intermediate state but ends in a global state.

The reader might remark that the case where both agents end in an intermediate state is not covered. This should actually not happen for two agents as the one with the smaller logical time should ends with a global state.

The rules of the next sections formalize these patterns and extend them to a (non-empty) vector of agents. Similarly, at least on agent should end in a global state.

Notations

The agent semantics relation is defined on a set of pair configuration/agent. Each reaction is based on three steps. First, each agent advance of one step and potentially update their outputs if they terminate their interval. Then, all visible temporal variables are extracted. And finally, each configuration is updated with respect to the new visible temporal variables. Note that it's the local environment which is updated in the resulting configuration so that the temporal variables are available in the expressions. The source set S is deliberated left undefined as it is an input of our application, any source can tick on any instant.

In a parallel setting, an agent can be either in a global state, that is on the bound of one of its interval or in an intermediate state, which is somewhere during its interval. To convey this idea, we extend the notation of the state of an agent. We note: C P @N × s which denotes an intermediate state of an agent with a remaining of N ticks of source s. If only one source is used we may simplify to the following notation C P @N ; C P which denotes a global state, as in the previous sections.

Futhermore, as we consider multiple agent, we denote a vector of agents as follows: [ag 1 , ag 2 , . . . ag n ] with ag i being an agent state as described above.

Semantics rules

This section gives the semantics rules to yields the native semantics of agent to a network of agents as explained in the two previous sections.

First of all, we have to define how to handle an intermediate state for a given agent. For that, we define an additional agent relation as following:

T = U pdate(T, E) E, T ag@n × s = == ⇒ n×s E, T ag (agent-5)
The rules should now handle two cases, agent-network-1 which is used for a network of agent using one source and agent-network-2 which is used for multiple sources.

ag 1 = == ⇒ k1×s ag 1 ag 2 = == ⇒ k2×s ag 2 . . . ag n = == ⇒ kn×s ag n k = min(k 1 , k 2 , . . . , k n ) s ∈ S T = n i=1 T emporal(ag i ) if k = k i ∅ otherwise [ag 1 , ag 2 . . . ag n ] S = === ⇒ k×s [∆ k/k1 (ag 1 , ag 1 , T ), ∆ k/k2 (ag 2 , ag 2 , T ), . . . ∆ k/kn (ag n , ag n , T )] (agent-network-1)
ag 1 = == ⇒ k1×s1 ag 1 if s 1 ∈ S otherwise k 1 = 0 ag 2 = == ⇒ k2×s2 ag 2 if s 2 ∈ S otherwise k 2 = 0 . . . ag n = == ⇒ kn×sn ag n if s n ∈ S otherwise k n = 0 T = n i=1 T emporal(ag i ) if k i = 1 and s i ∈ S ∅ otherwise [ag 1 , ag 2 . . . ag n ] S = === ⇒ 1×S [∆ 1/k1
(ag 1 , ag 1 , T ), ∆ 1/k2 (ag 2 , ag 2 , T ), . . . ∆ 1/kn (ag n , ag n , T )] (agent-network-2) Finally, we define ∆ k which denotes an intermediate advance of k steps on a network of agents. This operator is defined as following:

∆ k/0 (ag, , ) = ag (delta-stuttering) ∆ k/kag ( E, T P @ k ag , E, T P, T app ) = E ∪ T app , T P, if k = k ag E, T P @ (k ag -k), otherwise (delta-intermediate) ∆ k/kag ( E, T P, E , T P , T app ) = E ∪ T app T P , if k ag = k E , T P @ (k -k ag ) otherwise (delta-global)

Inria

In the equations above, all the patterns described in figure 4 are covered. First, for multisource application delta-0 handles the case of agent stuttering (the agent does nothing on this step), delta-1 covers the case of figures 4c and 4d in which the blue agent starts in an intermediate state while delta-2 covers the case of the figures in 4a, 4b and 4e in which the blue agent starts in a global state. The section above described only communication between tasks through a generic temporal variable which is available only on producer ticks and transmitted directly to any consumer. Based on this mechanism, in all PsyC communication means, data can only be produced or consumed on visibility instants, which correspond to interval boundaries. This means that on the start instant of all agent intervals, the corresponding inputs are updated and at the end instant, the corresponding outputs are updated to be available to other agents. Consequently, in temporal variables as well as streams (detailed below), writing is effective only on the deadline of the current interval. The mechanism formalized in the last sections share similarities with Esterel valued signals. As such, more practical communication channels can be built using intermediate synchronous components (i.e. fifo, shared variable . . . ) as long as they only synchronize using PsyC clocks. The PsyC language define two of those, although more can be defined. We discuss now those two channel types and how they can be handled:

Communication channels

The actual Temporal Variable which, in practice, is persistent and also features sampling. This can be defined with a function tv consumer = T emporal(tv producer , clk) where tv consumer is a persistent tv producer sampled on clk. Figure 5 illustrates such behavior.

The Stream which acts as a fifo between the producer and the consumer. Its definition is more complex as we have to deal both with the push() statements of the producer as well as the pop() statements of the consumer. Intuitively, all the push() statements of an sLET interval outputs an array from the producer and all the pop() statements outputs a pop counter from the consumer. Then, the communication function can be defines as s consumer = Stream(s producer , nb consumer ) where each time an s producer is sent by the producer, it is concatenated in the global fifo where nb consumer previously read elements deleted (in a fifo fashion).

The communication functions defined above are synchronous and thus their semantics is better defined using the synchronous approach. Basically, they can create a new temporal environment T such that T = {t | ∀c ∈ Channels, f c (T ) = t } where Channels denotes the set of communication channels of the application and f c its communication function.

Note that, even if communication channels only synchronize on PsyC clocks, like the agents, the logical instants on which they read or write values from agents is of prime importance. The good rhythm of data exchange is actually the key factor for the correction of the whole system. It is needed in properties such as end-to-end latencies or freshness. Verify those properties is one of the possible applications of this semantics as well as the synchronous one defined in the next section.

Although theoretically, those definition of communication channel also work in the case of agents based on different sources, we only consider mono-source communication in this document as:

1. It can be difficult to implement those communication channels (e.g. due to potential infinite buffers);

2. The PsyC compiler in its current state does not implement it.

The next section introduces the synchronous semantics and defines one communication function : the Temporal Variable with a sampling history which is the main communication channel of PsyC.

Synchronous Semantics of PsyC

While the sLET paradigm has an native real-time interpretation which is amenable to efficient compilation and scheduling analysis, the synchronous approach is more abstract and thus, more adapted for model-level analysis such as formal verification. The strong semantics of synchronous languages allows supporting foundations such as Mealy machines and digital circuits which are universally recognized formalisms used, among other, by formal verification tools. As stated in the description of the formalisms, the sLET and the synchronous model have a very close semantics as they both rely on the Multiform Logical Time concept.

Esterel translation principle

This section gives an other semantics of PsyC as a translation to a synchronous language, the Esterel language. We choosed this language as PsyC and Esterel are actually quite close syntaxically; they are both imperative and control-flow.

The translation principle is quite straightforward. All PsyC clock ticks are translated using Esterel signals, even intermediate ticks not used for agent synchronization. Those "synchronization" signals can only be emitted from the environment or from periodic clock components. Agents synchronize on these clock signals using the Esterel await statement, which has an equivalent semantics to the PsyC statement. The agent control-flow statements can be translated to the equivalent Esterel ones without difficulties.

The main difference lies in the communication handling. In PsyC, an elementary action starts on some clock tick and end on some other. Any emitted value in an elementary action has to wait for its ending to be displayed (i.e. made visible to others). Similarly, any read value in an elementary action has to be consulted at its start. In Esterel, all computations are virtually instantaneous with respect to some global instant. In our Esterel translation of PsyC, any computation is done synchronously to the start of the elementary action, thus reading input on Inria the same instant. However, outputs has to be kept internally (i.e. via a variable) until the end of the elementary action, on which it is then emitted.

All agents are composed in parallel as well as communication channels, like temporal variables. The latter is treated similarly to the agents as they can only synchronize on clock signals. However, contrary to the agents, they take input and outputs from agents that can be processed synchronously.

Sources and Clocks

Agent declaration

The declaration of an agent is more complicated as it is no possible to implement a generic module agent as for clocks or temporals. Hence, each agent has to be translated to a dedicated Esterel module. Let's consider that our agent, named ID, has the body b start , b 1 , ...b K and the clocks c 1 , c 2 , ..., c J . The temporal variables consulted (i.e. in input) by the agent are temporal in 1 , temporal in 2 ..., temporal in N and the displayed ones (i.e. in ouput) are temporal out 1 , temporal out 2 , ..., temporal out M . Their respective types are T IN i for inputs and T OU T i for output. Futhermore, inputs also have its depth DEP T H i , which is its array size, associated to its type. Finally, the starttime's value is STARTTIME VALUE while its clock is STARTTIME CLOCK. For simplicity, we present first the agent interface: i n t e r f a c e Agent ID I n t f :

--c l o c k s input c 1 , c 2 , . . . , c J ; --i n p u t s input temporal in 1 : T IN 1 [ DEP T H 1 ] ; input temporal in 2 : T IN 2 [ DEP T H 2 ] ; . . . input temporal in M : T IN M [ DEP T H M ] ; --o u t p u t s output temporal out 1 : T OU T 1 ;
output temporal out 2 : T OU T 2 ; . . . output temporal out N : T OU T N ; end i n t e r f a c e

The main ideas of this translation are the following: initially, the agent waits for its starttime. then, after initializing its variables (i.e. its next body state, its private temporal variables and potentially its local variables) the agent enters an infinite loop in which the matching body is called, i.e. initially its start body; when a body is terminated, the loop handles the call to the next matching body; Inria when a body is aborted, i.e. via a jump or endbody statement, the trap catches the body exit and the loop handles the call to the next body. Note that, all displayed temporal variables are duplicated with private copies that are variables. Body state is also handled by a variable because it may change multiple times during an instant. As the body content b i is actually a PsyC statement, T (s) actually denotes the translation of a statement described in the next section.

Agent Statements

PsyC nothing is just translated by: n o t h i n g PsyC assignation of temporal x, x := exp is translated by: private temporal out x := T (exp) PsyC assignation of variable x, x := exp is translated by: v a r x := T (exp)

RR n°9506

PsyC statement's advance, of the form advance n with c and assuming var1, var2 . . . varN are all the temporal variables in output of the agent, is translated by: await n c ; emit temporal v ar1 ( private t emporal v ar1 ) ; emit temporal v ar2 ( private t emporal v ar2 ) ; . . . PsyC sequence statement is translated by:

T (stmt1) ; T (stmt2)
PsyC condition statement, if (exp) stmt1 else stmt2 is translated by: i f T (exp) then T (stmt1) e l s e T (stmt2) end i f PsyC while statement, while exp do stmt, is translated by a combination of a trap/exit, handling the exit condition and a loop: trap e x i t w h i l e i d i n loop i f T (exp) e l s e e x i t e x i t w h i l e i d ; T (stmt) end loop end trap PsyC bounded while statement, while exp [n] do stmt, is similar to the while statement but with an additional bound which is decremented at each iteration and can also act as an exit condition. It is translated by: var w h i l e i d c o u n t := N i n trap e x i t w h i l e i d i n loop i f T (exp) and w h i l e i d c o u n t > 0 e l s e e x i t e x i t w h i l e i d ; w h i l e i d c o u n t := w h i l e i d c o u n t -1 ; Inria T (stmt) end loop end trap end var

Agent Expressions

PsyC agent expressions can be evaluated into an equivalent form in Esterel. However, we will not dive into the details of expression translation as it is out of the scope of this report. Indeed, in PsyC, most complex C expressions are actually defined outside of the language, through function calls. We only give the translation of the temporal variable access.

A temporal variable access expression is expressed as $[n]temporal in which denotes the access temporal in on the n th last value sampled on its clock. It is translated by the following access on the input temporal variable array: t e m p o r a l i n [ n ]

Agent Application

The global PsyC application translation pattern is then simply the global parallel composition of all the modules defined above. Let's assume that we have an application with: In this translation pattern, agent parameters are given implicitely. This means that, in the agent modules, the exact parameter name should be used. Also, it should be surprising that there is no input nor output except the sources. But actually, in practice, such inputs or outputs might be dedicated tasks (potentially agents). For semantics purpose, some temporal variables could be however put in input or output of the application. Input temporal variables should be not yet sampled while output temporal variables should be already sampled (i.e. through the Temporal module). As an example, consider the following application module interface:

. . . end module

Of course, input and output temporal variables should not be redeclared as local signal in the application module.

Equivalence criteria between both semantics

Based on the introduced PsyC semantics and its Esterel translation, this section gives an observational equivalence between them for individual and network of agents.

To give an equivalence between the native semantics of PsyC and Esterel, we shall first have an operational semantics of both of them. The PsyC operational semantics has already been given in section 4 and various Esterel formal semantics have been given in the litterature. However our Esterel translation of PsyC heavily relies on data (e.g. private variables, body handling) and the original Esterel semantics does not consider data [START_REF] Berry | The Constructive Semantics of Pure Esterel[END_REF]. Hence, we will use the semantics described in [START_REF] Potop-Butucaru | Constructive operational semantics[END_REF] that extends the original one with data handling. This gives the following transition relation for Esterel: Inria Definition 6 (Esterel semantics). Given a constructive Esterel program P and a set of data, the semantics of its macro-step is given by the following relation: The equivalence theorem yields naturally from both semantics (PsyC and Esterel) and the data equivalence relation. Considering an 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 the source). If both data representation are equivalent at the start of the interval, then, they are also equivalent at the end. Proof. By structural induction on native rules structure Note that theorem 2 does not consider stuttering, that is, transition without source tick. However, this result extends easily to allow stuttering, Esterel transition does not change the program when no source tick is present.

P, data

Nonetheless, this equivalence result only adress a single agent while an application is actually a system of multiple agents, as described in both semantics. More precisely, the native semantics divides an agent interval into sub-intervals, introducing partial states, to allow the parallel product with other agents. This product operator thus models the beginning and the ending of all agents intervals in a synchronous fashion. Additionnaly, communication only synchronize on global logical clocks (i.e. sources or periodic). Consequently, because agents evolve independently in terms of synchronization, this equivalence result compose nicely and is thus preserved to the case of multiple agents. Full formalization is left for future work.

Case-Study

As an illustration, we shall consider a very simplified version of the control system of a spaceship introduced in [START_REF] Carle | From Dataflow Specification to Multiprocessor Partitioned Time-triggered Real-time Implementation[END_REF], called a Guidance, Navigation and Control system (GNC). This use-case is The GNC functional architecture composed of three tasks: Fast which interacts with the sensors and actuators, GNC which is responsible of the control and guidance functions and Thermal which is responsible of the thermal regulation. GNC has two different modes, one nominal mode and one degraded mode that has different periods constraints. The functional architecture is described in Figure 6.

Based on the functional and temporal requirements, the GNC task could be implemented in PsyC as detailed in Figure 8a and based on the Esterel translation, it can be translated to Esterel as shown in Figure 8b.

In nominal mode, the native semantics yields the following infinite trace for agent GNC:

C ag = == ⇒ 100 C 1 ag 1 GNC() = ======= ⇒ 30 C 2 ag 2 = == ⇒ 70 C 3 ag 3 GNC() = ======= ⇒ 30 C 4 ag 4 . . .
The source source ms is omitted for clarity reasons and the function GNC() has be annotated on its corresponding transition. If we take this transition, the Esterel translation yields the -------E

Ag GN C() Ag P 0 {ms} GN C() P 1 {ms} P 2 P 30 ≈ ≈ 30 ms (a) GNC semantics simulation diagram 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]
1 P 1 , data 1 ---- E 2 P 2 , data 2 . . . ----- E 30 P 30 , data 30
where data contains f ilteredSensors used for the computation in the first transition which outputs the updated updateCommands value only in data 30 , thus having an equivalent behavior as the native semantics described above. The simulation diagram in Figure 7a illustrates this equivalence at the agent level while Figure 7b illustrates how the parallel operator from section 5.4 allows to build a unique automata from a network of agent automata.

Implementation Issues

Without going into details into the compilation process, it is important however to raise some issues due to the expressivity of PsyC. Depending on the application domain, PsyC can be used with multiple sources or with only one temporal source (each logical clock can reduce to one clock). In this section, we shall consider the latter sub-case of PsyC which is predominant in our industrial work. (Of course, those problems also arise with multiple-sources, but the solution are more complex.)

The "mono-source" compilation process of PsyC starts by reducing all the clocks to one source clock. This is called the unfolding process. For each task, one get one unfolded automata using only the source clock, as given by the native semantics. The second compilation process is /* s t a r t : 0 , c o n s t r a i n t = 2 */ advance 2 ; // c o n s t r a i n t = 1 f ( ) ; advance 1 ; // c o n s t r a i n t = 1 advance 1 ; // c o n s t r a i n t = 2 f ( ) ; advance 2 ; // c o n s t r a i n t = 2 (c) Unfolded constrained PsyC code to pull up the temporal constraints on the start of a logical interval. This allows the execution platform to set up the correct timers before starting any computation. The Figure 9 sketches the different steps of the implementation process, constraints annotation then become system calls for the real-time platform which ensure that any computation following the constraint terminates (i.e. the next advance is reached) before the end of the allowed time.

However, the compilation is more complex when multiple advance statement with different values are reachable from the start of an interval. In that case, the compilation process could not predict which constraint is the correct one as illustrated in 10a. This is a consequence of the compilation model which could not evaluate conditional expression, thus having internal non-determinism when branching. (However, note that the operational semantics of PsyC is still deterministic.) The solution that have been implemented in the Krono-Safe compiler for years now, is a mechanism to release the constraint, after its initialization, during a computation in a logical interval. The initial constraint is thus the minimal constraint of all the reachable advance and when the execution chose a branch with a higher constraint that the one previously set, additional time is given to the constraint according to the new reachable advance. This mechanism is illustrated in 10b. However, in this example, one should note that h() should systematically fit in a logical interval of duration 2, even if the chosen branch has a constraint of 3. In the case of multiple sources, the problem is however harder to solve as one may not be Inria able to compute the min of multiple clocks related with partial order. This one of the reasons that multi-source handling is limited in the industrial compiler, in particular to one source by agent/task.

Related Work

Synchronous-Reactive languages Several models have been proposed to specify the timing behavior of real-time systems. The most classical approach is based on synchronous languages and the synchronous hypothesis. This includes the use of languages such as Esterel or Esterel. However, the compilation of synchronous languages may suffer from the so-called "Long Task Problem" when tasks of different rhythms are compiled; execution time variability is usually limited to a common cycle rate. More recently, synchronous languages, such as Esterel relax the synchronous hypothesis, and thus do not suffer from the same compilation problems, but are limited to the the use of strictly periodic clocks.

Logical Execution Time

The closest model to our work is the Logical Execution Time paradigm introduced in the Giotto language, later improved with the TDL language. These languages can express a set of periodic tasks with a succession of periodic constant Logical Execution Time intervals as well as a limited mode semantics. Comparing to synchronous languages, they trade expressivity with a simpler model, allowing a simpler and less pessimistic compilation. In particular, they could not express logical clocks nor more complex behavior such as aperiodic behaviors. Our work try to reach a compromise between classical Logical Execution Time and the synchronous approach. synchronous Logical Execution Time, and in particular the PsyC language, can describe a set of task that have an automata expressivity as well as some logical clocks used to set logical deadlines for each computation. In the sub-case where each logical clocks can be reduced to one pseudo-physical logical clock (mapped to real-time), classical Logical Execution Time compilation techniques could be re-used.

External Non-Determinism In the more general case in which logical clocks could be mapped to any event sequence, this raises concern, however, about external non-determinism. These problems have been heavily studied in the litterature in work such as CSP with the socalled "input guards", conflict freeness in Petri Nets, monotonocity in Kahn Process Networks, latency-insensitivity and endochrony of synchronous languages.

Logical Execution Time with events As synchronous Logical Execution Time (and PsyC) can also be used to describes events, its expressivity is also very close to the xGiotto language, extending Logical Execution Time with events. Nonethess, besides compilation issues, it seems that the so-called "multi-source" version of PsyC does not have great industrial interest yet. Most Krono-Safe industrial partners are satisfied with the "mono-source" version of PsyC.

Conclusion and Future Work

Through a generalization of Logical Execution Time, called synchronous Logical Execution Time, this report gave two formal semantics of PsyC, a native operational semantics and a synchronous semantics defined by translation to a synchronous language. It also introduced an observational equivalence criteria between both semantics. As PsyC faithfully represents the synchronous

  body s t a r t { f ( ) ; advance 2 with A; g ( ) ; advance 3 with B ; } Communication agents can communicate with each other through dedicated deterministic communication channels. Those communication channels only synchronize on PsyC clocks similarly to the agents. In PsyC, there are two types of communication channels:

Figure 1 :

 1 Figure 1: Visibility Principle. Here, the temporal variable has an harmonic relation with both the displayer and the consulter agent

Inria

  source s o u r c e m s ; clock c10ms = 10 * s o u r c e m s ; clock c100ms = 10 * c10ms ;

  source c clock ::= clock c 1 = n 1 * c 2 + n 2 agent ::= agent id (n with c) body+ body ::= body id stmt stmt ::

Figure 3 :

 3 Figure 3: Abstract syntax of a PsyC subset

  [[ exp ]] E denotes a more general evaluation of exp with respect to the environment E and E[x ← [[ exp ]] E ] denotes the update of the environment E with the evaluation of exp assigned to x.

Inria

Definition 3 (

 3 Clock State). A clock state d c is defined as d c = (d s -Φ(c)) mod Π(c) with respect to its corresponding source date d s .

4. 5 . 1

 51 Basic statementsnothing terminates instantaneously and can be rewritten to itself.C nothing ---→ C nothing(nothing)x := exp terminates instantaneously with an updated environment due to the evaluation of exp.E, T, b x := exp ---→ E[v ← [[ exp ]] E ], T, b nothing(assign) next b statement change the target body instantaneously E, T, b 1 next b 2 ---→ E, T, b 2 nothing (next) jump b statement change the target body instantaneously and exits the current body E, T, b 1 jump b 2 ---→ E, T, b 2 endbody (jump) endbody statement exists the current body and starts the target body instantaneously E, T, b endbody ---→ E, T, b abort current body and go to B initial (b) (endbody) with B initial the initial set of body of the current agent 4.5.2 If statements

Figure 4 :

 4 Figure 4: sLET Composition patterns

Figure 5 :

 5 Figure 5: Two agents separated by a synchronous component TV defining a temporal variable

  Sources are just pure input signals whereas clocks are signals defined with respect to other signal with the following generic Clock module: module Clock ; --i n p u t c l o c k input c l k i n ; --o u t p u t c l o c k output c l k o u t ; --c o n s t a n t s c o n s t a n t Period , O f f s e t : integer ; await immediate c l k i n ; await [ O f f s e t mod P e r i o d ] c l k i n ; loop emit c l k o u t ; each P e r i o d c l k i n ; end module 6.3 Temporals Let's consider first a basic sampling module defined as follow: module Sampler ; type T ; input In : T ; output Out : T ; loop emit Out ( ? In ) ; pause ; s u s t a i n Out ( p r e ( ? Out ) ) ; each C end module As with clocks, a generic module can implements the mechanism of temporal variable. The depth is given as a static parameter and the types are parametric.module Temporal ; g e n e r i c c o n s t a n t DEPTH : u n s i g n e d ; type T ; type T B u f f e r = T [DEPTH ] ; input C ; input Temporal In : T ; output Temporal : T B u f f e r ; [ run Sampler [ Temporal Input / In , Temporal [ 0 ] / Out , C/ Clk ] | | f o r i < N -1 dopar run Sampler [ s i g n a l p r e ( ? Temporal [ i ] ) / In , ? Temporal [ i + 1 ] / Out , C/ Clk ] end f o r ] end module

type

  Agt ID b o d i e s = enum {BODY B ST ART , BODY B 1 , . . . , BODY B K } ; module Agent ID : e x t e n d s Agent ID I n t f ; --s t a r t t i m e await STARTTIME VALUE STARTTIME CLOCK; --body h a n d l i n g var b o d y t a r g e t : Agt ID b o d i e s := BODY B ST ART , private temporal out 1 : T OU T 1 := init , private temporal out 2 : T OU T 2 := init , . . . private temporal out M : T OU T N := init i n loop trap b o d y e x i t i n s w i t c h c a s e b o d y t a r g e t = BODY B ST ART do T (b start ) c a s e b o d y t a r g e t = BODY B 1 do T (b 1 ) . . . c a s e b o d y t a r g e t = BODY B K do T (b k ) end s w i t c h end trap end loop end var end module

  emit temporal v arN ( private t emporal v arN ) ; PsyC statement next, next b, is just translated by: b o d y t a r g e t := body b ; PsyC statement endbody, is just translated by: e x i t b o d y e x i t ; PsyC statement jump, jump b, is the sequence of a next and an endbody statement, thus it is translated by: b o d y t a r g e t := body b ; e x i t b o d y e x i t ;

  the clocks being C1, C2, ..., CJ the temporal variables being tv1, tv2, ..., tvN, and the sampled temporal variables being tv1 sampled, tv2 sampled, ..., tvN sampled and the agents being ag1, ag2, ..., agM module A p p l i c a t i o n :--s o u r c e s input s1 , s2 , . . . , sn ; s i g n a l tv1 : T1 , tv2 : T2 , . . . , tvN : TN, t v 1 s a m p l e d : T1 [DEPTH1] , t v 2 s a m p l e d : T2 [DEPTH2] , . . . , tvN sampled : TN[DEPTHN] , C1 , C2 , . . . CJ i n [ run Clock [ s i g n a l c1 / c , c1 parameters ] | | run Clock [ s i g n a l c2 / c , c2 parameters ] | | . . . run Clock [ s i g n a l cJ / c , cJ parameters ] | | run Temporal [ s i g n a l tv1 / Temporal In , t v 1 s a m p l e d / Temporal , tv1parameters ] | | run Temporal [ s i g n a l tv2 / Temporal In , t v 2 s a m p l e d / Temporal , tv2parameters ] | | . . . run Temporal [ s i g n a l tvN/ Temporal In , tvN sampled / Temporal , tvN parameters ] | | run Agent ag1 | | run Agent ag2 | | . . . run Agent agM ] end module

  module A p p l i c a t i o n : --s o u r c e s input s1 , s2 , . . . , sn ; --t e m p o r a l v a r i a b l e s input t v 1 i n p u t : T1 INPUT , t v 2 i n p u t : T2 INPUT , . . . output t v 1 o u t p u t s a m p l e d : T1 OUTPUT [DEPTH1 OUTPUT] , t v 2 o u t p u t s a m p l e d : T2 OUTPUT [DEPTH2 OUTPUT] . . .

  where E i and E o are respectively the input and output signal set active on the current reactionIn our case, we only consider agent translation as Esterel program along with clock declaration, as illustrated in Figure8b. Esterel data corresponds to agent private variable, temporal variable copies, next body value etc, as expressed in the agent translation. We shall then give a data equivalence between Esterel data representation and PsyC data representation, called configuration in the semantics. Definition 7 (Data equivalence). Given a set of Esterel data and a PsyC agent configuration C, we note C ≈ data the equivalence relation between both representation

Theorem 2 .EP 1 ,

 21 Forall PsyC agent p ag and the Esterel translation T and for any agent transition of the form: C p ag = == ⇒ n×s C p ag Assuming, C ≈ data and s ∈ E, we have an equivalent sequence of Esterel transitions: T (p ag ), data ----data 1 . . . ----E P n , data n such that T (p ag ) = P n and C ≈ data n .

  Figure 6: The GNC functional architecture

Figure 7 :

 7 Figure 7: GNC semantics diagrams

Figure 8

 8 Figure 8: Task GNC

Figure 9 :

 9 Figure 9: Implementation

advance 1 ;

 1 // c o n s t r a i n t = 2 or 3? h ( ) ; i f ( /* some c o n d i t i o n */ ) { f ( ) ; advance 2 ; } e l s e { g ( ) ; advance 3 ; } (a) PsyC code with conditional constraint advance 1 ; // c o n s t r a i n t = min ( 2 , 3) h ( ) ; i f ( /* some c o n d i t i o n */ ) { f ( ) ; advance 2 ; } e l s e { // c o n s t r a i n t += 1 g ( ) ; advance 3 ; } (b) PsyC code with translated conditional constraint

Figure 10 :

 10 Figure 10: Implementation with conditions

RR n°9506

Inria

Siron & Potop-Butucaru & de Simone & Chabrol & Methni

route des Lucioles -BP 93 06902 Sophia Antipolis Cedex Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-6399

Logical Execution Time paradigm and more generally, the class of Logical Execution Time languages (e.g. Giotto, TDL, xGiotto), this equivalence result also applies to these languages. Verify timing properties is one of the possible applications of the native semantics as well as the synchronous one. Hence, future work will focus on developing a formal verification framework for the PsyC language based on this approach.