Guillaume P Bien D'autres

Je

Keywords: Systèmes Temps-Réel, Temps d'Exécution Logique, Langages Synchrone-Réactifs, Vérification Formelle Real-Time Systems, Logical Execution Time, Synchronous-Reactive Languages, Formal Verification. viii Real-Time Systems, Logical Execution Time, Synchronous-Reactive Languages, Formal Verification

Méthodologie de vérification formelle de propriétés temporelles pour les applications temps-réel critiques basées sur le concept de temps logique Résumé Les systèmes temps-réel critiques doivent respecter des contraintes temporelles strictes qui doivent être considérées tout au long du cycle logiciel. Cependant, du fait que les temps d'exécution exacts ne sont généralement pas connus lors de la conception, le temps logique fournit un moyen d'abstraire les contraintes temporelles et les exécutions du temps physique, dépendant de la plateforme. Dans cette thèse, nous nous concentrons sur deux formalismes basés sur le temps logique. L'approche Synchrone-Réactive abstrait totalement le temps physique en utilisant des bases de temps discrète sur lesquelles les calculs sont déclenchés. L'approche de Temps d'Exécution Logique utilise des bases de temps logique pour représenter non seulement les instants de déclenchement, mais aussi les durées des calculs élémentaires. Dans notre travail, nous commençons par définir une unification des approches Synchrone-Réactives et de Temps d'Exécution Logique, fournissant un cadre formel naturel pour définir la sémantique de PSYC, un langage temps-réel industriel expressif. Nous définissons deux sémantiques pour celui-ci : une sémantique native à grands pas, préservant les durées logiques des intervalles de temps, définie par des règles structurelles opérationnelles ; et une sémantique synchrone à petits pas définie par traduction vers un langage Synchrone-Réactif étendant les durées des intervalles de temps à une succession de transitions atomiques. Nous montrons que les deux sémantiques sont équivalentes. Cette formalisation de la sémantique de PSYC nous permet de définir une méthodologie de vérification formelle pour PSYC basée sur du model-checking symbolique. Pour réduire l'espace d'état pendant le model checking, nous définissons une technique d'optimisation inspirée du model-checking temporisé. Enfin, nous spécifions les exigences temporelles que nous voulons vérifier via un langage de spécification de contrainte d'horloge -CCSLqui sont ensuite traduites en observateurs synchrones.

Contents

1.1 General context Safety-critical real-time systems have to respect strict time constraints. Thus, time constraints must be considered throughout the software development cycle: from system specification to integration on a specific hardware platform. However, the exact execution time of computations is generally not known during the system specification and design phases, as they depend on a specific target. The Logical Time concept provides a way to abstract time constraints and execution from hardware Physical Time by providing discrete time bases on which computations react. At integration time, analyses are then used to ensure those physical time constraints -mainly execution time estimations -satisfy the logical time constraints necessary to ensure the system's safety.

In this thesis, we focus on two main formalisms based on logical time. The Synchronous-Reactive (SR) approach totally abstracts physical time by discrete time bases -called logical clocks -on which computations are executed atomically on specific ticks. Although SR is very expressive (partly due to its logical clocks), it suffers from implementation difficulties when using multi-scale time constraints. As an alternative, the Logical Execution Time approach uses logical time bases to represent not only triggering instants but also the durations of elementary computations. This defines time windows which contain the actual computation and on which communication can only happen on the boundaries of those logical time intervals. Both SR and LET provide a deterministic and concurrent way to deal with logical time constraints. ESTEREL and LUSTRE are examples of Synchronous-Reactive languages, while GIOTTO and TDL are examples of Logical Execution Time languages. However, LET suffers from expressivity limitations; in particular, timing durations are based on a unique chronometrical time base, and thus, cannot express timing constraints based on multiform logical time. XGIOTTO, LINGUA FRANCA and PSYC are examples of languages that include features from both SR and LET: Language Semantics PSYC inherits from both the Synchronous-Reactive (SR) and the Logical Execution Time (LET) approach. By identifying how SR and LET formalisms relate, we define in this thesis a synchronous generalization of LET called synchronous LET in which time interval boundaries are specified by synchronous instants. We use sLET as a semantics foundation for PSYC: we define a native big-step semantics preserving the logical durations of time intervalswhich is close to the one used in the compiler today -defined by structural operational rules and a synchronous small-step semantics defined by translation to the synchronous language ES-TEREL expanding time interval durations to a succession of atomic transitions. We show that both semantics definitions are equivalent on the boundaries of the LET time intervals.

Formal Verification From the synchronous semantics of PSYC, this thesis also defines a verification methodology for PSYC based on symbolic model-checking and on the modelization of timing requirements as synchronous observers. However, as the synchronous semantics expand all LET intervals in atomic transitions, this approach does not scale well. To solve this problem, we define an optimization technique inspired by timed automata model-checking, which preserves durations from the native semantics assuming that only one base clock is used in the program. Finally, we show how to encode our requirements in a clock constraint logic -CCSL -instead 1.2 -Contributions 3 Figure 1.1 -Global methodology proposed in this thesis CHAPTER 1 -Introduction of a more traditional temporal logic -such as LTL -as the program typically has multiple time scales among components. In both cases, however, requirements belonging to the safety class can be translated to synchronous observers.

Thesis Outline

The outline of this thesis is composed of three main parts:

-The first part presents the overall context and background of this thesis, both academically and industrially. In Chapter 2, we describe the overall context and industrial background. Then, in Chapter 3, we give an overview of various languages and formalisms used to specify, design and implement real-time systems.

-The second part focuses on semantics foundations for the PSYC language. Chapter 4 gives an overview of the PSYC language and defines synchronous LET as being a synchronous generalization of Logical Execution Time. It is then used in Chapter 5 to define the native and the synchronous semantics of PSYC. We also give an equivalence criterion between those semantics, which proof is sketched in Appendix A.

-The third part focuses on a verification methodology based on the semantics defined on the second part . Chapter 6 formalizes the different temporal requirements that we want to verify on PSYC programs. Then, Chapter 7 describes the overall verification methodology for the general case of PSYC programs. Finally, Chapter 8 focuses on the subcase of PSYC programs using only one base clock to define an optimization method compressing the state space.

-In chapter 9, as a final part, we give a global conclusion of this thesis as well as various perspectives.

Publications and Communications

In this thesis, we did multiple publications and communications. This section describes them by category.

International Conferences and Workshops

[1] Fabien Siron, Dumitru Potop-Butucaru, Robert De Simone, Damien Chabrol, and Amira Methni. Semantics fondations of PsyC based on synchronous Logical Execution Time. In TCRS 2023 -Time Centrics Reactive Systems, San Antonio, Texas, U.S.A., May 2023.

[2] Fabien Siron, Dumitru Potop-Butucaru, Robert De Simone, Damien Chabrol, and Amira Methni. The synchronous Logical Execution Time paradigm. In ERTS 2022 -Embedded Real Time Systems, Toulouse, France, June 2022.

-Publications and Communications

FIRST PART

Background

Learning never exhausts the mind.

-Leonardo da Vinci, (1452-1519).

CHAPTER 2

Safety-Critical Real-Time Systems

Today, in fields such as avionics and automotive, software plays an increasingly important role. Among the significant trends in these fields are automation and electrification. Examples include automatic landing systems [Air23] and electrification of aircraft landing gears [START_REF] Safran | Safran green taxiing[END_REF]. This results in increasingly complex systems, and, due to strong economic constraints, also results in harder integration process and bigger function concentration. For all these reasons, software reliability is becoming a major challenge in those fields. This thesis falls within this context. The following sections give global definitions characterizing the overall context.

Critical Systems

In this work, we focus on systems that are qualified as critical due to the consequences a system failure could have. We give below the definition from the IEEE * glossary [iee90]:

«

Software whose failure could have an impact on safety, or could cause large financial or social loss. » (IEEE)

Depending on these consequences, critical systems can be classified into two main classes:

-Safety-critical: A system whose failure could endanger people's safety. Examples include control systems of nuclear plants or control systems in civil aircraft; -Mission-critical: A system whose failure could endanger its mission and, thus, business operations. Examples include navigational systems of unmanned spacecrafts or bank management systems. In this work, we focus mostly on safety-critical systems; the targeted fields of the company KRONO-SAFE include mainly avionics and automotive industries. However, most techniques described in this work could be applied to both classes.

Real-time and reactive software In safety-critical real-time systems, timing is part of the system's functionnality; those systems have to respect a set of strict timing constraints to guarantee the overall safety. [START_REF] Kopetz | Real-Time Systems: Design Principles for Distributed Embedded Applications[END_REF] defines real-time systems as follows: 10 CHAPTER 2 -Safety-Critical Real-Time Systems

«

A real-time computer system is a computer system where the correctness of the system behavior depends not only on the logical results of the computations, but also on the physical time when these results are produced. » (H. Kopetz) However, real-time systems are not traditional sequential software programs. A typical traditional program computes output value from inputs values, and then stop as shown in 2.1b; they are often called Transformational [START_REF] Harel | On the development of reactive systems[END_REF]. However, real-time systems -and more generally reactive systems -continuously react to the environment by a sequence of reactions similar to Figure 2.1b as shown in Figure 2.1a; reactive systems, thus, react at a pace dictated by their environment [START_REF] Harel | On the development of reactive systems[END_REF]. Reactive systems call for concurrency; they are often composed of various communicating parallel components that react with their environment at different rate. Additionally, as reactive systems are often used in a critical context, they should be highly predictable, and thus call for determinism. A system is said to be deterministic if the same sequence of inputs always produces the same sequence of outputs [START_REF] Berry | The Esterel v5 Language Primer[END_REF]. Hence, as advocated in [START_REF] Edward | Computing needs time[END_REF], real-time and reactive software should consider time throughout the software cycle as functionality constraints rather than quality of service measurements. To do that, one should consider languages and formalisms with time as a first class citizen ensuring system's predictability.

The control system of an aircraft engine (called FADEC) is an example in which the control accuracy -and thus the whole system's safety -directly depends on temporal requirements dictated by the environment. Not respecting those requirements can lead to an engine failure, which could in turn jeopardize the system's integrity (here, the aircraft) and therefore the passengers safety. A FADEC is a very classical safety-critical real-time system and is one of the use-cases of the ASTERIOS technology, developed by KRONO-SAFE. Formal Design for Real-Time Reactive Systems As systems are becoming increasingly complex, traditional techniques face their limit: manual coding of functional source code may insert bugs, and test-based verification could fail to detect bugs due to the incompleteness of testing. Moreover, the later the bugs are detected the more expensive are the consequences. To overcome those issues, formal methods provide mathematically rigorous techniques for various activities of the software life cycle. We give below the definition of Clarke [START_REF] Clarke | Formal methods: State of the art and future directions[END_REF]: « Formal methods are mathematically based languages, techniques, and tools for specifying and verifying systems. » (Clarke) In real-time systems, the Multiform Logical Time concept [START_REF] André | Modeling time (s)[END_REF] (sharing a lot of similarities with the Tagged signal model [START_REF] Edward | A framework for comparing models of computation[END_REF]) mandates to deal with a formal abstraction of time through logical timing constraints dictated by high-level requirements and thus, independent from 2.0 -11 • Cadencing requirements (e.g., synchronization, periods);

• Flow requirements (e.g., freshness, end-to-end latency).

(Logical Time only)

Design Verification

Logical time based Software (in our case in PsyC)

(Adding platform provisions in physical time)

Implementation

• Scheduling policy;

• Compilation;

• Schedulability analysis. -The design phase allows for the design of logical timing constraints providing a deterministic timing behavior to be respected by the implementation.

-Then, the implementation phase allows logical timing constraints to be mapped to physical time based on platform timing provisions (e.g., estimation of worst case execution time) and real-time scheduling.

Logical timing constraints rely on logical clocks to express time; they denote sequence of instants either based on external events or on specific instants of physical time. Similarly to [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF], logical clocks are used to replace physical dates by logical sequencing. Real-time systems often rely on multiple logical clocks to express system components reacting on different pace. They are two cases of multi-clock systems:

-All logical clocks are derived (e.g., via periodic refinement) from a unique global logical clock, often mapped to a hardware timer during implementation;

-Logical clocks rely on multiple sources of logical time which could be independent or partially controlled.

In practice, most industrial systems fall in the first category due to safety considerations. Nonetheless, some examples still need multiple source clocks. For example, an automotive powertrain control is a typical system which relies on two time bases: a source clock based on the crankshaft position to trigger computations on specific physical state of the engine and a source clock based on a hardware timer to define timing constraints such as initialization time or deadlines [CDO + 14].

In this thesis, we focus only on the design phase as the implementation phase has been heavily covered by previous work from the CEA [START_REF] Lemerre | An Introduction to Time-Constrained Automata[END_REF]. The design phase can be a particularly challenging task due to the number of requirements to satisfy. In this work, we particularly focus on temporal requirements specifying either constraints among the rates of multiple components (e.g., synchronizations) or among the propagation of some data across multiple components (e.g., endto-end latency). Multiple techniques could be used then to ensure that logical timing constraints are compliant with high-level requirements. Among them, formal verification -and more precisely model-checking -is a generic and automatic technique to provide formal guarantees for the verification process. It has been heavily studied and used in formalisms based on logical time in academy [START_REF] Halbwachs | Synchronous Observers and the Verification of Reactive Systems[END_REF] and industry [START_REF] Bochot | Model checking flight control systems: The airbus experience[END_REF].

Industrial Considerations Formal methods are becoming a trend for safety-critical systems in various industrial domains. In railway, the Meteor project has been designed using the B method, a formal specification language based on proven refinements [AHC96]. In avionics, synchronous reactive formalisms such as SCADE [START_REF] Colaço | Scade 6: A formal language for embedded critical software development[END_REF] have been used successively in large scale avionics systems and provide formal verification techniques -mainly model-checking -that have been studied for realistic avionics systems [START_REF] Bochot | Model checking flight control systems: The airbus experience[END_REF].

Safety-critical systems are usually subject to safety standards defining legal and regulatory requirements to specify, design, develop and verify systems at various stages. For example, DO-178C [START_REF]Software Considerations in Airborne Systems and Equipment Certification[END_REF] focuses on avionics software, ISO-26262 [Org18] on automotive systems and IEC-62304 [START_REF]Medical device software -Software life cycle processes[END_REF] on medical software. As an illustration, Figure 2.3 shows the typical software process imposed by the DO-178C: the specification process typically produces a set of high-level requirements, then the design process produces both the software architecture and a set of lowlevel requirements, and finally the implementation and integration process produce respectively the source code and the executable object code. Verification activities are performed at each level, ensuring compliance with upper levels; this is often done with code inspections and test campaigns using strict coverage criteria.

Nonetheless, safety standards are being adapted to the use of formal methods techniques and languages:

1. In the avionics domain, DO-178C has an appendix, named DO-333, defining guidelines to adapt DO-178C objectives to the use of formal methods techniques and tools;

2. In the automotive domain, ISO-26262, advocates for the use of formal methods for the verification process of the most critical systems (ASIL-C and D);

3. In the industrial domain, IEC-61056, highly recommends the use of formal methods for the most critical systems (SIL-4).

In the particular case of the avionics domain -which is our main focus in this thesis due to its industrial context -NASA have worked on a detailed case study providing guidance on how to apply formal methods at various steps of the software process using the DO-333 [START_REF] Cofer | Do-333 certification case studies[END_REF]. In this thesis, we focus on model-checking based techniques applied to formalisms based on logical

CHAPTER 3

Languages and Models for Real-Time Systems In this chapter, we give an overview of different languages and models used for the modelisation of real-time systems at various stages of the software life cycle. We first describe in real-time scheduling models that are typically used during the integration process and in real-time operating systems. We then give an overview of various languages and programming models dedicated to the modelisation of real-time constraints and typically used during the design process. We finally describe formalisms used to formally define high-level temporal requirements that are often used in a formal verification process.

Real-time scheduling models

A traditional way to model real-time systems is to consider a finite set of concurrent tasks (usually periodic), whose execution is dictated by a scheduler which decides which task is executed next at each invocation. In real-time systems, tasks are subject to strict real-time constraints 16 CHAPTER 3 -Languages and Models for Real-Time Systems coming from high-level requirements. However, in embedded real-time systems, tasks also have time provisions dictated by the platform's computing capabilities. The real-time scheduling field is therefore interested in tasks models, and the choice of scheduling policies as well as schedulability (or feasibility) analyses to ensure that platform's provisions could not invalidate real-time task constraints. The reader might want to read [START_REF] Ashford | Introduction to Embedded Systems: A Cyber-Physical Systems Approach[END_REF] which gives a good introduction to real-time scheduling models.

Task models

Task constraints We usually consider a finite set of tasks T in which each task τ ∈ T is executed by a sequence of task instance τ 1 , τ 2 , . . .. Tasks are usually defined to be either periodic or sporadic depending on the regularity of task instances. Formally, we define r i as being the activation instant of a task instance τ i .

In general, we define a periodic task by the activation function r i = O + (i -1) × T where O and T are respectively the offset and the period of the task. Sporadic tasks do not have a specific activation function for r i , however, activation should usually satisfy r i+1 ≥ r i + T min where T min is the minimal interval between two successive task activations.

The second typical temporal constraint of a task is the deadline of a task written δ i . It corresponds to the instant on which the task instance τ i has to be terminated. In a real-time system with hard critical constraints, a task instance τ i should fit between r i and δ i , otherwise it is considered as an error. Considering that s i and f i are respectively the execution start and termination of τ i , then τ i has to satisfy r i ≤ s i < f i < δ i . All those constraints are shown in Figure 3.1.

Task provisions

The constraints given above are induced by temporal requirements. However, to compute the instants on which computations start and terminate, s i and f i , dictated by a scheduling policy, it is necessary to give an estimate of the task execution time, which we write e i . In a preemptive model, e i is not necessarily equal to f i -s i ; execution can be broken down into several sub-windows in which the sum of the execution time should be e i . In traditional scheduling models, e i is often considered to be constant. Today, however, it is commonly accepted that this time is variable due to multiple factors: program control-flow, cache management . . . It is usually defined by a Best and Worst Case Execution Time (respectively BCET and WCET). e i is thus often an estimation of the WCET.

Scheduling policy and schedulability analysis

A scheduling policy elects which task should run at each invocation according to a desired objective. However, a scheduling policy may fail to satisfy some of the time constraints -typically the deadline -du to an incompatibility between real-time constraints and target provisions. In order to avoid this issue, the use of so-called schedulability analysis is needed to ensure that time provisions tasify task constraints. This analysis depends directly on the scheduling policy used, and is usually defined as a criterion demonstrating that f i < δ i for any execution.

r i s i preemption f i δ i + e i (activation) (start) (finish) (deadline)
Task instance τ i To illustrate the concept of schedulability analysis, let's take the EDF scheduling algorithm (i.e., for Earliest Deadline First). At each scheduling decision (e.g., at the end of task's execution), the next task to be executed is the one with the earliest deadline. In the case of a set of periodic task and with deadline δ = T , the schedulability analysis is defined as follows for a set of task

T = {τ 1 , τ 2 , . . . τ n }: n j=1 e j T j ≤ 1 (3.1)
This criterion, introduced in [XP90], ensures that the computational load is less than 100%. Hence, if the condition is met, real-time constraints are guaranteed to hold.

In practice, real-time scheduling models are rather low-lever, and do not allow reasoning from a programmatic point of view on a real-time software. This is because a scheduling model is not a programming model: there is neither communication model nor structured control. Additionally, response times are difficult to predict (f i -r i is variable at runtime) and can be a cause of non-determinism. Nonetheless, those models are very useful to study the capacity of a hardware platform to satisfy real-time task constraints. In this work, we focus on real-time constraints, that we will call logical constraints. We make the assumption that WCET estimation and schedulability analysis exist for the various languages described in this work.

Real-time languages and programming models

One of the greatest of the mid-20th century in computer science is the Church-Turing thesis, which shows the equivalence of several models of computation, such as the lambda-calculus or the Turing machine. However, those models are sequential. As discussed in the previous chapter, reactive real-time systems need model of computations relying on both concurrency and timing constraints. This section gives an overview of the main languages and programming models highlighting those aspects that are all based on logical abstraction of time. For each, we also discuss the notion of determinism, which is often mandatory in the context of safety-critical systems.

Process algebra

Process algebras are specific languages defined in the context of concurrency theory defined by Milner [START_REF] Milner | A Calculus of Communicating Systems[END_REF]. These languages enable us to describe formally interactions, synchronizations and communications between process -or agents. Most algebras define the following elements [START_REF] Milner | A Calculus of Communicating Systems[END_REF] [Hoa78]:

-Inter-process communication mechanisms; -Sequential composition; -Parallel composition which is generally asynchronous; -And finally, replication mechanisms such as loops or recursion.

One of the most famous examples of process algebra is the modelisation of a Coffee Machine (CM). We give here its behavior using a simplified syntax of CCS:

CM = coin.(coffee + tea).brewing.CM
This machine is defined by a recursive sequence of action. We use two operators "+" which defines choice and "." which defines sequential composition. The behavior then the following: first the machine waits for a coin, then it proceeds to either brewing coffee or tea depending on the one selected before returning to its initial state. Let's now define the typical behavior of users who either try to get a coffee for free if it's possible or gives a coin before talking. USER = (coffee + coin.coffee).talk.USER Using the parallel composition " ", we can now define the interactions between the two process, USER and CM. This illustrates the mechanism of handshaking which synchronizes corresponding actions.

(CM USER) = coin.coffee.(brewing talking).( CM USER)

However, generally, process algebras allow defining concurrency but at the price of determinism. Due to the asynchronous composition of process, the algebras cannot guarantee that the resulting process is deterministic. Furthermore, process algebras are not adequate to specify temporally predictable requirements. Nonetheless, multiple approaches extend process algebras to support determinism or predictable temporality: SCCS [START_REF] Milner | Calculi for synchrony and asynchrony[END_REF], Meije [START_REF] Austry | Algebre de processus et synchronisation[END_REF] or CoReA [START_REF] Boniol | CoReA: A synchronous calculus of parallel communicating reactive automata[END_REF] to name a few.

Synchronous-Reactive languages

To combine concurrency and determinism, dedicated languages based on the Synchronous-Reactive (SR) programming model have been introduced [START_REF] Benveniste | The synchronous approach to reactive and real-time systems[END_REF]. In a SR language, time is abstracted by a sequence of instants on which computations (often called reactions) are triggered. Those sequences of instants are called logical clocks and this time abstraction, logical time. Multiple logical clocks can exist in SR programs; however, the semantics of SR languages usually impose to expand each behavior on a unique base clock. The SR programming model is based on two main principles:

-Synchrony: the output of a computation is available to all other computations triggered on the same instant; hence, communications are synchronous. The synchronous hypothesis states that all computations triggered on some instant should terminate before the next one.

-Causality: the output of a computation must be available before any other computations could use it on the same instant; hence, communications are causal.

Based on both synchrony and causality properties, SR languages provide support for modeling complex concurrent programs while ensuring determinism. SR programs focuses on temporal constraints -based on logical time -while physical time mapping is left to the implementation. Figure 3.2 shows a typical execution of a synchronous-reactive program -Statements that don't take time, which are logically instantaneous like send s which sends a signal s or present s then P else Q which execute P or Q depending on the presence of signal s (note that even if reacting to s does not take time, P or Q may take time); -And statements that take time -one or multiple instants -like pause which waits for the next instant or await S which awaits an instant in which signal s is present.

in 0 in 1 in 2 in 3 in 4 in 5 out 0 out 1 out 2 out 3 out 4 out 5 in 0 in 1 in 2 in 3 in 4 in 5 out 0 out 1 out 2 out 3 out 4 out 5

Logical time

Physical time interpretation

The example in Listing 3.1 illustrates the main features of ESTEREL. This program awaits signals A and B on its inputs -in any order -and emits O when both signals are received. Signal R allows the reset of the program. A detailed description of the language is given in Chapter 5 in the semantics definitions of PSYC. Imperative SR languages are however not adapted for control systems. In this domain, computations are usually described by block-diagrams in which blocks corresponds to operators and transitions to dataflow dependencies.

Lustre LUSTRE [START_REF] Caspi | LUSTRE: a declarative language for real-time programming[END_REF] is a declarative dataflow SR language used to model such control systems. It defines a set of mutually recursive equations operating on data streams. A stream is a sequence of values based on a (logical) clock, which specifies the presence or absence of values on each instant of a global base clock. LUSTRE defines two types of equation operators:

-Traditional operators which depend on the value's type; arithmetic operators for integers or boolean operators for boolean values.

-Synchronous operators which allow the manipulation of stream history; pre(X) defines delayed values of X by one instant and X -> Y defines X on the first instant, then Y . LUSTRE also defines sampling/merging operators that we omit here. node Edge(X : bool); returns (Y : bool); let Y = False -> X and not (pre X) ; tel Listing 3.2 -LUSTRE raising edge example Listing 3.2 shows the most classical LUSTRE example which defines a raising edge detector. Y is set to true when X is true on the current instant but was not on the previous instant. Listing 3.3 shows how the raising edge detector can be used to define a similar program to the ABRO ESTEREL example. Basically, O is the raising edge of the conjunction of A and B which are held while R is not present. Table 3.3 gives a possible execution of the ABRO program.

Signal SIGNAL [START_REF] Benveniste | Synchronous programming with events and relations: the SIGNAL language and its semantics[END_REF] is also a dataflow SR language, really similar to LUSTRE. However, contrary to LUSTRE, SIGNAL can deal with the clocks of its streams. only partially defined by relations (instead of deterministic operators). Then, it is the job of the compiler to synthesize those clocks while respecting various relation constraints. Hence, SIGNAL allows the design of programs containing multiple -partially-related -clocks; hence, it is often considered as a polychronous language.

However, while SR languages allow mixing both concurrency and determinism, their semantics usually impose to expand reactions on a common global base clock. Consequently, even "long" computations (i.e., which physical duration lasts multiple instants of the base clock) are semantically projected on the base clock and have to terminate before the next instant (i.e., synchronous hypothesis). Hence, programs composed of various components with multiple time scale (both logically and physically) are often impossible to compile using traditional SR compilation techniques.

Logical Execution Time languages

The Logical Execution Time (LET) [START_REF] Christoph | The logical execution time paradigm[END_REF] paradigm takes a different approach to specify temporal constraints; instead of specifying the computations by a reaction triggered on a clock tick, the execution time of those computations is abstracted such that a computation always behaves as if it lasts exactly a constant and fixed logical execution time. This defines an abstract time windows which contains the actual computation. However, to guarantee determinism, communication are done only on the boundaries of the LET time interval; inputs are read automatically on the start of the interval and outputs are produced automatically on the end of the interval. Figure 3.4 illustrates how LET abstracts computations: the upper part is the logical view interpreted by the model and the lower part is the physical view of a typical real-time implementation. The yellow symbol shows that in LET, execution can be typically preempted by other concurrent tasks while maintaining the communication behavior. Hence, contrary to SR, the semantics of LET allow more execution time variability for computations as (logical) computation durations are part of the semantics. This allows classical scheduling algorithms -such as EDF -to be used in the implementation. GIOTTO is a time-triggered language implementing the logical execution time paradigm. It allows the definition of multiple modules parametrized by their periods which are, in turn, composed of tasks defined by their frequency. Tasks also have deterministic communication channels implementing LET communication to communicate together. Even if GIOTTO permits to describe mode and mode transition, tasks are basically strictly periodic which limits considerably its expressivity. Additionally, all constraints are expressed respectively to physical time; there is no clear distinction between logical time and physical time, nor discrete time basis as logical clocks. TIM-ING DEFINITION LANGUAGE (TDL) is an other language implementing LET extending GIOTTO concepts with a more advanced module and mode system. However, TDL suffers from the same issues as GIOTTO.

in 0 in 1 in 2 in 3 in 4 out 0 out 1 out 2 out 3 out 4 in 0 in 1 in 2 in 3 in 4 out 0 out 1 out 2 out 3 out 4

Logical time

Physical time interpretation

Other languages based on logical time

Traditional Logical Execution Time languages suffer from expressivity limitations; they are often limited to multi-periodic behaviors with limited mode handling, but more importantly, timing durations are based on a unique chronometrical time base. This section describes languages mixing aspects from both synchronous-reactive and logical execution time languages; they all rely on multiform logical time while also allowing logical durations of computations to be expressed.

The XGIOTTO language

XGIOTTO is a language implementing LET (as GIOTTO) but supporting events to specify synchronizations (i.e., to specify LET boundaries) [START_REF] Ghosal | Eventdriven programming with logical execution times[END_REF]. In its principle, this language is closer to SR languages as logical time could express both timing or events. However, inter-arrival time assumption of events has to be encoded implicitly in the program using a rather complex mechanism called event scoping [START_REF] Christoph | The logical execution time paradigm[END_REF]. Event scopes define the computation to be taken in a given time span -specified by chronometrical time or events -and can be nested. Hence, the logical duration of a computation has to be refined to a chronometrical time basis for inter-arrival time to be considered. Hence, in this thesis, we consider that XGIOTTO computations can be triggered by events, but their deadlines are still specified by a chronometrical time basis, as in traditional LET.

The example below shows part of an automotive engine controller inspired by [START_REF] Ghosal | Implementation of afr controller in an event-driven real-time language[END_REF] based on two time bases: crankshaft and milliseconds. The controller is started on event start and immediately stopped -due to the ASAP policy -on event stop. Two concurrent tasks are shown: time which is triggered each millisecond and lasts one millisecond, and cycle which is triggered each crankshaft event and lasts two milliseconds.

Listing 3.4 -XGIOTTO controller example

The LINGUA FRANCA language LINGUA FRANCA (or LF) [START_REF] Marten | Reactors: A deterministic model of concurrent computation for reactive systems[END_REF] is a coordination language based on a logical time framework called the Tagged Signal Model [START_REF] Edward | A framework for comparing models of computation[END_REF]. The components of the language are called reactors and are essentially composed of input port, output port, and reactions that reacts to input events -called tags -coming from input ports. An application is defined by multiple reactors composed concurrently and by their port connections.

CHAPTER 3 -Languages and Models for Real-Time Systems

We show in Listing 3.5 a very simple pipeline example using LINGUA FRANCA taken from [START_REF] Edward | Generalizing logical execution time[END_REF]. The reactors are composed of a sensor task, two computing tasks and an actuator task connected in this order. The rate of the reactors are given by a logical clock (called timer in LF) triggering the sensor reaction each period, by default 10 milliseconds. In the semantics, by default, connected tasks are synchronous; when some reaction receives a message on a logical instant t, then it can produce an output message on the same logical instant t. As explained in [START_REF] Edward | Generalizing logical execution time[END_REF], LF can model LET behaviors using delayed connections between ports as shown in Listing 3.6 below; reactors task1 and task2 are assigned a LET duration of 10 milliseconds using the after construction. Note that, unlike traditional LET of GIOTTO or TDL, the semantics of LF is fully compatible with the synchronous-reactive one. Hence, reactors can be triggered by any event, or more generally, logical clocks. It is not clear however if the after construction allows the LET duration to be defined similarly, using a clock or event synchronization.

... main reactor(period:time(10 ms)) { ... task1.out -> task2.in after period; task2.out -> actuator.out after period; } Listing 3.6 -LINGUA FRANCA LET pipeline example

The PSYC language PSYC is an industrial language developed by Krono-Safe [START_REF] Krono-Safe | [END_REF]. It is a language inspired by process algebras, synchronous-reactive languages, and with a principle very similar to Logical Execution Time. PSYC actually stands for Parallel SYnchronous C, thus highlighting the two main principles of the language: synchronous and parallelism (both in the model and in the implementation). In this thesis, we define PSYC based on an intermediate formalism that inherits from both synchronous-reactive and logical execution time approaches, called synchronous Logical Execution Time (sLET). In sLET, both the triggering instants and the duration of the computations are expressed using logical clocks. Hence, whereas in traditional LET a timing window is specified by a triggering instant and a chronometrical duration, in sLET, a timing window is specified by two successive synchronous instants that we call synchronization points (or instants).

Thus, comparing to ESTEREL, sLET (and PSYC) can specify the logical duration of computations, but inherit the delayed communication model from LET. Comparing to traditional LET languages such as GIOTTO, sLET uses logical clocks instants to specify interval boundaries instead of a unique chronometrical time basis. Both XGIOTTO and LINGUA FRANCA can rely on logical clock instants (respectively events and tags) to specify triggering instants and can specify the logical durations of the computations. However, logical durations are expressed by a chronometrical time basis in both cases; XGIOTTO rely on event scoping to encode implicitly inter-arrival times [START_REF] Christoph | The logical execution time paradigm[END_REF] and LINGUA FRANCA uses chronometrical time to express delays between reactors. The table 3.5 gives an overview of the main differences.

A PSYC application is composed of a set of concurrent agents (or processes) communicating through data-flow channels, called temporal variables. Agents are composed of C code and a dedicated temporal synchronization primitive: the advance instruction. This instruction is used to set a synchronization instant, acting as a time barrier, between elementary actions, which are timing intervals between two successive synchronizations. According to LET communication semantics, communications only take place atomically on these synchronisation instants. On the other hand, unlike LET, those instants are modeled relatively to logical clocks. In the following example, the end of the first elementary action containing f , corresponds to a synchronization of 2 ticks of the clock C. At this point, y is made visible to the other agents, and g can begin execution with the x input captured at this same instant. y = f ( ) ; advance 2 w i t h C ; g ( x ) ;

We give an illustration of a PSYC task in Listing 3.7 describing an agent performing conditional filtering (i.e., typically according to a system mode). First, the agent starts on the first tick of clock c1s, hence, 1000 milliseconds. Then, when the condition is true, the function filter has a logical duration of 3 ticks of clock c100ms, which is equivalent to 300 milliseconds in that case. It is then followed by an empty elementary action terminating on the next c1s tick; this is used to resynchronize on the task period. Indeed, when the condition is false, the task only performs an empty elementary action terminating on the next c1s tick. As in LINGUA FRANCA, PSYC is a language based on logical time which inherit both from LET and Synchronous-Reactive languages. As in LF, it generalizes LET using a semantics based on the synchronous-reactive approach. However, while LINGUA FRANCA is a general purpose coordination language, PSYC is an industrial language dedicated to safety-critical real-time systems. Hence, in this thesis, we focus on PSYC for various reasons. First, the PSYC language is developed by the company KRONO-SAFE who is funding this work. But most importantly, PSYC allow us to focus on a language that inherit from multiple logical time approaches while having major industrial projects using it (e.g., from the SAFRAN group). A detailed description of PSYC is given in chapter 4.

Language

Triggering

Temporal Requirements Formalisms

To define temporal requirements -also called properties -on the languages defined in the previous sections, we also need specific specification languages -actually closer to logicsallowing for a specific set of temporal behaviors. Ultimately, those specification languages are often used in formal verification to model-check the requirements on the program.

Temporal logic

Formally reasoning about time goes back to Aristotle to interpret sentences such as "Tomorrow, there will be a sea fight" for philosophical purposes [START_REF] Vardi | From Monadic Logic to PSL[END_REF] -U p q (or Until p q), holds if p holds on all instants until an instant on which q holds; -p (or Always p), holds if p holds on all the following instants; -p (or Eventually p), holds if there exists a future instant on which p holds.

Additionnally, properties are often classified into two main classes:

-Safety properties state that "something bad should not happen". Typically, we want to prevent a bad condition to happen often modeled as an invariant that should hold on all reachable states of the program.

-Liveness properties state that "something good will happen". Contrary to safety properties, liveness properties guarantee that a good condition will hold sometimes in the future.

The vision of time described by LTL is, by definition, linear; to satisfy an LTL property, a program has to satisfy the property on each of its execution path. Another approach is to consider path quantification as in the Computational Tree Logic (CTL) [START_REF] Baier | Principles of Model Checking (Representation and Mind Series)[END_REF]. CTL has two operators dedicated to path quantification: A p and E p to consider respectively universal and existential quantification for property p on execution paths of the program. Examples of LTL and CTL properties are shown in Figure 3.6. Additionnally, MTL is an other classical variations of LTL dedicated to quantitative temporal properties [START_REF] Koymans | Specifying real-time properties with metric temporal logic[END_REF]; classical LTL operators are extended with intervals that specify when the operator applies. As an example, [0;10] p specify that p should be reachable in the next 10 instants.

In our case, we want to focus on safety and linear properties as we want them to hold for all execution paths and mainly to prevent "bad things to happen" due to the safety-critical context. We also consider bounded liveness properties for latencies, but this is actually a special case of safety. However, in practice, programs based on logical time often rely on different timelines due to the use of multiple external clocks or tasks with different timing constraints. Temporal logic does not capture well properties that rely on multiple time scales -or multiple logical clocks.

Clock Constraint Specification Language

CCSL is a specification language dedicated to the modelisation of temporal requirements defined as a set of constraints between logical clocks [START_REF] André | Syntax and semantics of the clock constraint specification language (ccsl)[END_REF]. Those logical clocks can be any sequence of events, similarly to the one considered in temporal logic. In this work, we choose CCSL to capture requirements as relations between the timing of multiple tasks because in PSYC, agent have usually different rates or time scales.

CCSL defines the four main following constraints:

c 1 ⊂ c 2 which denotes that c 1 should be a subclock of c 2 ; thus, on each instant, if c 1 holds then c 2 should hold.

c 1 ≺ c 2 which denotes that c 1 strictly precedes c 2 ; thus, the n th tick of c 1 strictly precedes the n th tick of c 2 .

c 1 c 2 which denotes that c 1 precedes c 2 ; thus, the behavior is similar to the constraint above except that tick coincidence is allowed.

c 1 # c 2 which denotes exclusion between c 1 and c 2 ; thus, c 1 cannot tick on the same instants as c 2 .

Additionnally, each clock can be refined using CCSL expressions. We omit them here as an extensive description of CCSL is given in chapter 6. From a theoretical aspect, CCSL and temporal logic are very close. [START_REF] Gascon | Logical time and temporal logics: comparing uml marte/ccsl and psl[END_REF] shows that the safety subset of PSL -an industrial variant of LTL -is equivalent to a bounded subset of CCSL. Unbounded CCSL specification is due to the operators generating counters to encode the difference between two clocks; however, most specification can be bounded by adding additional causality constraints as in the tiny example above.

Synchronous observers

Synchronous observers is not a specific language to model properties, but instead, an approach to model properties inside SR languages by continuously observing the program [START_REF] Rushby | The versatile synchronous observer[END_REF]. This approach has been introduced in the context of SR language verification, and, in particular, for the language LUSTRE [START_REF] Halbwachs | Synchronous observers and the verification of reactive systems[END_REF]. In this approach, a SR program is considered as a model containing both the program to be verified and the requirements. Observers are then specific tasks containing requirements that observe the program's state and raise an error if one of the requirement is not satisfied. Typically, the supported properties are linear safety properties.

Both LTL and CCSL can be translated to synchronous observers; they are then used as a mean to verify the requirements either dynamically -by runtime monitoring -or staticallyby model-checking. In both case, the verification problem is reduced to a reachability analysis on the observer output; if an error is reachable, then the requirement is false. In chapter 7, we show how synchronous observers can be used to model and verify CCSL properties on PSYC code.

SECOND PART

Language and Semantics

Every Kairos is a Chronos, but not every Chronos is a Kairos.

-Hippocrates, Praeceptiones (460-377 av.J.-C.).

CHAPTER 4

Synchronous Logical Execution Time in PSYC This thesis focuses on the PSYC language, developed by the company KRONO-SAFE. This language is based on both Synchronous-Reactive and Logical Execution Time foundations, making it ideal for studying its semantics based on logical time as well as verification techniques, detailed 34 CHAPTER 4 -Synchronous Logical Execution Time in PSYC respectively in chapter 5 and chapter 7 of this thesis. Hence, this chapter briefly describes the industrial context and tooling of the technology -called ASTERIOS -in section 4.1, then defines in section 4.2 a formalism unifying Logical Execution Time and Synchronous-Reactive approaches -called synchronous Logical Execution Time -used to give an overview of the PSYC language in section 4.3.

The ASTERIOS Software Suite

Origins of the technology

KRONO-SAFE is a spin-off company from the CEA * created in 2011 and whose objective is the industrialization of two research projects -OASIS and PHAROS -under the name AS-TERIOS. The company is now targeting domains such as avionics, railways and the automotive industry; those are all safety-critical domains requiring certified tools to the highest level of criticality. The origins of the ASTERIOS technology goes back to the end of the 1990s with the OASIS project defined as following in [ACA + 96]:

«

The OASIS proposes rules and methods for safety-critical application engineering allowing to design and implement concurrent programs with fully deterministic behaviours, and thus to guarantee some specified properties of dependability » (C. Aussagues and al)

At that time, the main targeted domain of OASIS was civil nuclear power. In particular, it was used to build a Qualified Display System (QDS) used in modern nuclear plant by FRAMATOME [DAL + 04]. A decade later, OASIS has been adapted to the automotive domain under the name PHAROS before becoming ASTERIOS with KRONO-SAFE in 2011.

Industrial context

In industry, functional modeling and software integration activities are generally separated. The former is responsible for the functional behavior of a subset of the system, while the latter is responsible for the software and hardware integration of multiple functional components. Code generation of functional models has been automated for years in tools such as SCADE or SIMULINK based on synchronous reactive approaches. These tools are not, however, well suited for the integration of functional components using different time scales. Also, they do neither propose seamless tooling for on-target integration with features such as real-time scheduling nor memory protection. For all these reasons, software integration is still largely done manually in industry. ASTERIOS proposes methodology and tooling to automate software integration activity based on a parallel and synchronous language called PSYC; the toolchain is detailed in the next section.

Tooling

The ASTERIOS toolchain is built around a language called PSYC. It is composed mainly of a compiler called PSYKO compiling PSYC applications to binaries which can be executed on an embedded target by a dedicated real-time kernel. Figure 4.1 how those tools interact.

The compiler, called PSYKO, take C code corresponding to functional components (e.g., generated by SCADE) as well as PSYC tasks, and generates various binaries. Firstly, it generates a set of Partitions each of which containing a set of compiled PSYC tasks corresponding to the same criticality level. Secondly, the compiler generates a Runtime containing all the configuration entries necessary to the execution model, such as a static scheduling plan, bounded communication buffers and memory descriptors.

Both Partitions and the Runtime are executed on an embedded target along with a dedicated real-time kernel certified to the highest level of criticality for the avionics safety standard (DAL-A, DO-178C). The kernel implements the execution model with spatial and temporal isolation constraints specified in the Runtime. Note that this kernel is not meant to be run with any other application that the one generated by PSYKO and those can only be executed by the kernel.

ASTERIOS also gives the possibily to simulate the behavior of the PSYC execution model. Instead of generating binaries for an embedded target, PSYKO can generate them for the host machine. Then, those binaries can be executed with a specific simulation library which simulate the behavior of the real-time kernel. Note that in this approach, the Partitions and the Runtime are generated very similarly as if an embedded target was selected to be as faithful as possible.

Finally, one might remark that in this process, only the real-time kernel is certified for the avionics safety standard. However, the compiler could insert errors during compilation. To solve this problem, ASTERIOS also contains a validation tool called CHECKER which verifies that the compiler's outputs are compliant with the corresponding inputs. For example, it verifies that the static scheduling plan contained in the Runtime is correct with respect to the temporal constraints described in PSYC files. This tool is qualified using the software tool qualification considerations of the avionics safety standard (DO-330) as described in [START_REF] Methni | Asterios checker: A verification tool for certifying airborne software[END_REF].

A synchronous generalization of Logical Execution Time

We now describe a generalization of Logical Execution Time (LET) compatible with the Synchronous-Reactive (SR) approach, called synchronous Logical Execution Time (sLET). sLET provides a natural framework for defining the PSYC language and its semantics given respectively in section 4.3 and chapter 5.

Overview of synchronous Logical Execution Time

The objective of synchronous LET (or sLET) is to extend LET with SR aspects. Contrary to LET, in synchronous LET, the boundaries of LET intervals are actually synchronous instants, hence, defined using logical clocks. The computation are specified similarly to the ones from LET as they are defined with a strictly positive logical duration forming temporal intervals; although contrary to LET, each interval is defined by two synchronous instants called Temporal Synchronization Points (TSP) forming its boundaries. As in SR, those TSP are defined respectively to some logical clock.

As an illustration, Figure 4.2 shows the typical behavior of a synchronous LET task. The synchronization instants are specified respectively to logical clock A and B, in an alternation pattern. Thus, each computation has a duration defined as either 1 tick with clock A or B. This forms intervals -called elementary actions -with a delayed communication model similar to the traditional LET approach. More generally, in PSYC, the span of an elementary action is defined by the n th tick of the specified clock after the activation instant.

Compilation, and more precisely, real-time analysis, is also very similar to the one of LET and relies on the same implementation hypothesis: a computation has to terminate before its deadline. Thus, a language based on synchronous Logical Execution Time is compliant with classical schedulability policy ensuring that a computation fit in its logical execution time interval.

Definitions

This section covers the main definitions of synchronous LET that would serve as a semantics foundations in the next sections.

in 0 in 1 in 2 in 3 out 0 out 1 out 2 out 3 Clock A Clock B Synchronous LET task Figure 4.2

-Execution of a synchronous logical execution time program in logical time

We start by defining logical clocks which is the base construction used to define all the temporal constraints: Definition 4.2.1 (Logical Clocks). A logical clock c is defined by a totally ordered set of ticks

(t i ) i∈N .
Based on the logic clocks defined above, sLET allows you to model time windows for computations -called elementary actions -similar to PSYC. These elementary actions are used to abstract the execution time of some computation by defining two synchronous instants: one corresponding to the activation instant and one corresponding to the deadline. Unlike LET, these two instants are synchronous and specified using logical clocks.

Definition 4.2.2 (Elementary Actions). A Logical Execution Time (or Elementary Action

) is defined by some computation reaction, constrained by two temporal constraints : -an activation date d esd defined on some logical clock c start ; -a deadline date d ddl defined on some logical clock c ddl , by the number of ticks to await Those two constraints are special synchronous instants are called Temporal Synchronization Points (TSPs) and are used to form elementary actions.

Finally, to guarantee the model determinism, communications have to rsepect a visibility criterion similar to the ones from LET. The definitions above form the basis of the synchronous LET model. Elementary actions are then typically composed sequentially -as in LET. The deadline TSP of some elementary action is also the activation TSP of the next elementary action building sequential agents which can then be composed in parallel.

About functional and temporal determinism

The visibility principle actually gives a key criteria to ensure communication determinism, and thus, to avoid that the instants on which the communication happens depend on the physical execution time of some computation -its platform provision -which would be unpredictable. Previous work from the CEA on PSYC [START_REF] Lemerre | A model of parallel deterministic realtime computation[END_REF] proved this determinism result in the case of one global source clock. Next chapter defines a synchronous semantics for PSYC in the general case of multiple source clocks. Hence, as the semantics of synchronous-reactive languages is deterministic [START_REF] Potop-Butucaru | Compiling esterel[END_REF], determinism also holds for the generalized PSYC model -but more generally, synchronous LET -when multiple logical clocks are involved.

Nonetheless, one might argue that, in practice (not in the model per se), we can face two types of non-determinism:

-Internal non-determinism can hardly be avoided in practice; while the semantics itself does not face non-determinism issues, the tools (e.g., the compiler) do not typically evaluate branching conditions in the control-flow. Hence, tasks are typically modeled as nondeterministic finite automata simplifying various analysis.

-External non-determinism arise typically when multiple logical clocks are used in input of the system (corresponding to multiple source in PSYC). When two tasks depend on different clocks that are not related, the ordering between them can be non predictable, and therefore cause different effects. Various solutions have been proposed in the literature (input guards in CSP, conflict-freeness in Petri nets, endochrony in SR languages . . . ). However, the simpler approach is usually to limit the task dependency to unrelated clock; in PSYC, industrial projects very often rely on a unique source clock -refined multiple time however -for safety reasons.

The PSYC language

PSYC is a language developed by KRONO-SAFE within the ASTERIOS toolchain. PSYC stands for Parallel Synchronous C and takes the form of C code to which synchronous and parallel primitives have been added. As mentioned in previous section, it inherits some aspects of both Synchronous-Reactive and Logical Execution Time formalisms. The remaining of this chapter gives an informal description of the PSYC language relying on synchronous Logical Execution Time. Full formalization is described in next chapter.

Source and clocks

Sources and clocks are the building block of the PSYC language modeling logical time basis which are used to trigger task computations.

Source clocks

Sources clocks represent logical clocks used as application inputs. They are very similar to ESTEREL input signals or to LUSTRE input stream's clock; source clocks define time basis on which task computations react. They can be assigned either to a hardware timer or to any input events by the toolchain. Syntaxically, source clocks are defined as following:

1 source <name>; Listing 4.1 -PSYC source declaration
We give here a proper definition of a source clock which correspond to the sLET definition given in section 4.2. Definition 4.3.1 (Source clock). A source clock s is defined by a totally ordered set of ticks (s i ) i∈N

Periodic clocks

Similarly to source clocks, periodic clocks in PSYC are also logical clocks defining a time basis on which task computation react. However, contrary to source clocks, they are defined respectively to other source or periodic clocks as periodic refinement. Syntaxically, they are defined as following:

1 clock <name> = <period> * <parent> + <offset>; Period and offset can be omitted in the syntax. In that case, they are defined with their default value, respectively 1 and 0. Definition 4.3.2 (Periodic clock). A periodic clock c is defined by (c i ) i∈N with respect to its parent cp where ∀i ∈ N, c i ≡ cp P ×i+O in which ≡ denote temporal coincidence (i.e., they are synchronous), P is the period and O is the offset. realtime is used to define two periodic clocks c2 and c4_2. Assuming that realtime is a hardware timer with a 1 millisecond period, then c2 has a period of 2 milliseconds as it ticks every two ticks of clock realtime. The second periodic clock, c4_2 has a period of 4 milliseconds as it ticks every two ticks of clock c2 which has a 2 milliseconds period.

Illustration: source and clocks

Additionally, c4_2 has an offset of 1 tick of clock c2 which correspond to 2 milliseconds.

Tasks

We now describe PSYC tasks which form the basic sequential execution unit of a PSYC application; the latter is composed of a set of concurrent tasks which are run in parallel on the target and can be assigned to a specific CPU core. In this thesis, we only define the main type of PSYC task called agent.

Elementary Actions

As explained in the section 4.2, elementary actions allow the definition of temporal window, similarly to Logical Execution Time, containing computations. It is defined by two synchronization instants, an activation and a deadline instant on which communication happen. Those are defined respectively to clock ticks by the advance statement as follows:

advance <n> with <c>;

Listing 4.4 -PSYC advance statement

Where n ∈ N * and c is a clock. It defines the next synchronization instant as being the n th tick of clock c after the preceding synchronization instant. It acts both as a deadline instant for code preceding it and as an activation instant for code following it.

The following example shows that f() has to terminate before n1 ticks of clock c1. This synchronization instant also acts as the activation instant of the next elementary action composed of g() which should terminate before n2 ticks of clock c2. To change the default looping behavior, dedicated statements can be used to change the body to be executed. next b selects the next body to be executed when the current one terminates and endbody aborts the current body to execute the next selected one, which is by default itself. Those two statements can be composed to form a new one jump b that jump to the specified body directly.

To illustrate those concepts, the example below defines three body scopes corresponding to different states -or modes -of the system's task. The first body is called start and is executed only once as body loop is selected as the next body to be executed. Then body loop loops unless an error is detected; in that case, it jumps directly to the failure body. They are defined as a set of body declaration in addition to a starttime parameter defining the first task synchronization instant, similarly to an advance statement. In this thesis, we consider that the starttime parameter can be omitted which is equivalent to immediately starting the first body on startup. Additionally, the first selected body is the start one -by convention -which have to be defined.

The example below illustrates the definition of a very simple agent which has a period of 1 tick of clock c and an offset of 1 tick of the same clock. We illustrate the concepts defined in the sections above with one of the most classical examples of a real-time system: a LED blinking controller. We give two variations of the same application: one defining the blinking of one LED, and the second defining the blinking of two LED (red and green) depending on the current mode with different frequency.

In both cases, the blinking specification is defined by the following requirements:

1. The periodicity of the LED pattern; 2. The causality of the LED pattern; switching on and off should alternate; 3. And the duty cycle of the LED pattern, defining the proportion in which the LED stays one with respect to the period. In other words, this defines the minimum and maximum latency between switching on and off the LED.

The chronogram below shows the typical timing that we expect from the application based on the requirements above. The period is defined by 10 ticks of clock c_period whereas the duty cycle is defined as being 40% to 60% of the period, which corresponds to a latency between 4 and 6 milliseconds.

Inter-task communication channels

The PSYC language has two deterministic communication means: temporal variables, which are dataflow channels that are updated on predefined instants, and streams, which are buffers with First-In First-Out policy.

Temporal Variables

A temporal variable is a shared variable between a producer -which update it on predefined instants -and its consumers. Additionally, temporal variable are sampled on clocks before being available to consumers; the latter can access to the last sampled value, which is the last updated producer value. Note that, in a dataflow channel, values are persistent; if no value is updated by the producer on some synchronization instant, the previous value is used. The chronogram below illustrates the mechanism of the temporal variable. Each clock tick of the temporal variable corresponds to the last value produced by the producer agent and each value read by the consumer corresponds to the value of the last clock tick of the temporal variable -but previous sampled values can also be accessed using the temporal variable history.

Producer agent Temporal Variable

Consumer agent

Syntaxically, a temporal variable is defined as following:

Illustration: control system

To illustrate the concept of temporal variables, we show in Figure 5.3 the simplified functional architecture of a guidance, navigation and control system, inspired from the one in [CPBL + 15]. In such system, communication is typically done using dataflow channels which can be implemented in PSYC using temporal variables. The system consists of two main communicating tasks: Fast which quickly interacts with hardware and GNC which interacts with Fast applying guidance commands. Between those two tasks, there are two temporal variables:

-fast_to_gnc sending data from Fast to GNC each 10 milliseconds; -and gnc_to_fast sending data from GNC to Fast, each 10 milliseconds with an offset of 3 milliseconds to match the end of GNC elementary actions.

Fast gnc_to_fast fast_to_gnc GNC

Streams

A stream is a queue belonging to a specific consumer and updated by an agent on predefined instants. A producer can push data into a stream and a consumer can pop them.

-The PSYC language 47

In PSYC, a stream is defined as follows:

stream <type> <stream_name> expiration <N>;

Listing 4.19 -PSYC stream declaration

Where <N> ∈ N * corresponds to the maximum duration (with respect to some source) that the data is available. It is used to ensure that the stream is always bounded; however, if some data expires in the stream, the system raises an error.

From the producer's side, the agent has to specify the stream that it is going to push on. Syntaxically, it is defined as following: 1. Popping from a stream without checking if the stream is not empty is unsafe; 2. Pushing too much data in a stream is also unsafe as it may raise expiration error if the consumer does not pop enough data.

In practice, most applications -which are generally control systems -use temporal variable instead of streams. Hence, this thesis focuses mainly on temporal variables; nonetheless, the methodology shown in this thesis also applies to streams.

Illustration: logging

Let's now consider a simple logging use-case in which a Logger agent pops data from a stream and log them. PSYC code is shown in Figure 4.6. The code shows two tasks, an agent called A sending data to stream s, and an agent called Logger with a period 10 times slower. A pushes one data each 1 milliseconds whereas Logger pops up to 10 data each 10 milliseconds (the up to is due to the loop decorator [10] which specifies an upper bound). Each 10 milliseconds, all data are popped from a stream. Because, the stream is defined with an expiration of 10 milliseconds, no data expires.

Summary

This chapter gave an overview of the PSYC language and its toolchain. In PSYC, agents can specify no only the triggering instants of their computations but also their logical duration respectively to a number of clock ticks. Consequently, the PSYC language relies on both the synchronous-reactive approach for its synchronization instants, and on the logical execution time approach for its elementary actions; both concepts are unified in the synchronous logical execution time model. The following chapter will give two different formal semantics for PSYC based on those concepts. This chapter describes the semantics of a subset of the PSYC language using two different approaches:

-A native "big-step" semantics preserving the logical duration of time intervals which is defined by a structural operational semantics approach. This semantics can be used to build automata -similar to Timed-Constrained Automata [LDAVN10] -used as a formal model for PSYC compilation.

= id := f (exp * ) | stmt 1 ; stmt 2 | if (exp) stmt 1 else stmt 2 | while exp do stmt | advance n with c, n ∈ N * | endbody | next b | jump b | nothing Figure 5
.1 -Abstract syntax of a PsyC subset -A synchronous "small-step" semantics defined by translation to a Synchronous-Reactive language -ESTEREL -expanding time interval durations to a succession of atomic transitions. This semantics directly supports formal models such as mealy machines which is used later in this work for formal verification.

We first describe a subset of the PSYC grammar considered in the semantics, then we formally define both semantics and we finish by giving an equivalence criteria between both semantics.

Abstract Syntax of PSYC

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 that are part of the C language (in fact, most of the C expressions are not interpreted by the PSYC compiler). The abstract syntax is described in Figure 5.1. 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 (e.g., statements). Aside from the abstracted expressions, we have the following assumptions on the grammar of PSYC:

-A PSYC application has to declare at least one agent and one clock so that the agent can specify synchronization instants;

-Temporal variables are associated to a unique producer agent;

-An agent should contain at least one body called start which is the first body to be executed;

-Finally, in a body, we assume that all paths should declare at least one advance statement to avoid instantaneous loop.

5.2 Native "big-step" Semantics of PSYC

Native semantics of one PsyC agent

We now provide the Structural Operational Semantics (S.O.S.) semantics [START_REF] Plotkin | A structural approach to operational semantics[END_REF] [Ber02] for single agents; the case of multiple agents -or agent networks -will be considered with in next section. The semantics amalgamate structurally all computations inside an elementary action until the next advance statement. This results in a single transition for an elementary action, labeled with the specified logical duration specified relatively to a source clock.

As always with SOS rules, operational transitions can be collected in a transition system, which in the case of PSYC is actually a Finite State Machine (FSM). This FSM can be seen as a generalization of Timed-Constrained Automata (TCA) introduced by Lemerre in [START_REF] Lemerre | An Introduction to Time-Constrained Automata[END_REF]; TCA abstract elementary actions by transitions labeled with absolute durations and with nodes corresponding a mix of before and after constraints but cannot specify logical durations specified relatively to a source clock. We first provide necessary notations, then provide SOS rules for the non-temporal control-flow features, then for temporal clocks advancements, and finally for the merge at the agent declaration level.

Notations

Operational semantics rules are usually given as a relation over a possible rewriting. Let's consider the relation s ---→ s which basically means that a given state s can be rewritten in s (also called 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 s ---→ s (5.1)
This means that if all assumptions are true (e.g., 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 values accessed using the notation E(x).

Configuration syntax

In this paper, an agent configuration -or state -is defined by the following tuple:

E, T, b

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

Transition Syntax

The semantics of PSYC is described in this work using two complementary relations, one for logically instantaneous behavior and one that represents time progress in terms of logical instants. We shall call the former non-temporal transitions and the latter 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 are due to advance statements making the time progress and is defined similarly:

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

They can be composed with statements which don't take time as long as the sequence of non-temporal transitions terminate with a temporal transition:

C t ---→ C 1 t 1 ---→ . . . C n t n = == ⇒ C t C t = == ⇒ C t
Finally, we note ---→ * the sequential composition 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: Additionally, to avoid keeping an unbounded date for each source, we assume that d c gives the (current) date of c modulo its period.

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
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 whether a unique source is used or not.

Semantics Rules

Basic statements We first consider basic statements, which corresponds to all non-temporal statements apart from control-flow statements.

nothing 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)
Where AbortBody() terminates instantaneously the current body. Full definition of this rule would require extending transitions with dedicated abort signal, similarly to exit statement in ESTEREL.

If statements

if statements terminate instantaneously and are rewritten with the branch selected by the condition.

[

[ 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)

56

CHAPTER 5 -Formal Semantics of PSYC 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)
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)
-The sequence statement takes time if its first statement takes time.

C s 1 = == ⇒ N ×s C C s 1 C s 1 ; s 2 = == ⇒ N ×s C s 1 ; s 2 (seq)
Advance statement Contrary to the previous statements advance is not logically instantaneous.

In fact, it is the only PSYC statement that takes time. Thus, it is rewritten to nothing and takes exactly the logical duration specified by the advance statement (with respect to the source clock).

N = Duration(n, c, date) T = UpdateOutputs(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 needs a date parameter to convert a deadline relative to a clock tick to an absolute deadline represented as a duration in source ticks. Additionally, the UpdateOutputs function extracts all the outputs from the internal environment to the external visible one. 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 declaration For body declaration, 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, its 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 its 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)
Agent declaration We finally define rules for PSYC agents that compose the rules defined above.

58

CHAPTER 5 -Formal Semantics of PSYC -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 (starttime n with c) B = == ⇒ N ×s C agent id (starttime 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 (starttime 0 with _) B = == ⇒ N ×s C agent id (starttime 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 (starttime 0 with _) B = == ⇒ N ×s C agent id (starttime 0 with _) B (agent-4)
The semantics rules of a PSYC agent always yield temporal transitions because all paths in a body have at least one advance statement.

Native 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 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 define two kinds of agent states in the context of an agent network: 1. Global states, which correspond to the actual agent states from the native semantics (i.e., the boundaries of an sLET interval) Next section illustrates the different overlapping patterns between agents for the mono-source case.

Overlapping patterns

The figure 5.2 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 5.2a shows two agents synchronized, they both start and end in a global state; -The case 5.2b 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 5.2d, 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 5.2c 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 5.2e 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 end with a global state.

Next section introduce formal rules to formalize these patterns and extend them to a vector of agents.

Notations

In a parallel network, an agent can be either in a global state, that is on the boundary of one of its interval or in an intermediate state, which is an intermediate instant 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 ; 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 that define the native semantics of 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 that to handle intermediate states as shown below:

T = U pdate(T, E) E, T ag@n × s = == ⇒ n×s E, T ag (agent-5)
Furthermore, we define an helper function ∆ k/kag which denotes an agent partial advance of k instants to a possible intermediate state, while the remaining time of the agent elementary action is of k ag instants. The operator is defined below first for stuttering (no source tick), then for intermediate state and finally for global states.

∆ 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)
In the equations above, all the patterns described in figure 5.2 are covered. For multi-source application delta-0 handles the case of agent stuttering (the agent does nothing on this step), delta-1 covers the case of figures 5.2c and 5.2d in which the blue agent starts in an intermediate state while delta-2 covers the case of the figures in 5.2a, 5.2b and 5.2e in which the blue agent starts in a global state.

The rules should now handle two cases, agent-network-mono-source which is used for an agent network defined on a unique source and agent-network-multi-source which is used for an agent network defined on multiple sources. In the former, delta is used to perform intermediate advance as shown in Figure 5.2 while in the latter, the semantics is closer to an asynchronous product as found in process algebra. The transition is labeled by a duration with respect to a set of source that ticks on the current instant written S.

ag 1 = == ⇒ k 1 ×s ag 1 ag 2 = == ⇒ k 2 ×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/k 1 (ag 1 , ag 1 , T ), ∆ k/k 2 (ag 2 , ag 2 , T ), . . . ∆ k/kn (ag n , ag n , T )]
(agent-network-mono-source)

ag 1 = == ⇒ k 1 ×s 1 ag 1 if s 1 ∈ S otherwise k 1 = 0 ag 2 = == ⇒ k 2 ×s 2 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/k 1 (ag 1 , ag 1 , T ), ∆ 1/k 2 (ag 2 , ag 2 , T ), . . . ∆ 1/kn (ag n , ag n , T )]
(agent-network-multi-source)

Communication channels

The section above described only communication between tasks through a generic temporal variable channel which is available only on producer ticks and transmitted directly to any consumer. From that mechanism, which is similar to ESTEREL valued signals, 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:

-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.

-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 defined as s consumer = Stream(s producer , nb consumer ) where each time an s producer is sent by the 5.3 -Synchronous "small-step" Semantics of PSYC 63 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.

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 "small-step" Semantics of PSYC

The last section presented a native semantics of synchronous LET that preserves the logical durations of the computations. It is used in practice to get efficient compilation and scheduling analysis. In this section, we define a simpler semantics -called synchronous semantics -defined as a translation from PSYC to the Synchronous-Reactive language ESTEREL. We chose ESTEREL because its syntax is very close to the PSYC language; they are both imperative and control-flow oriented. Contrary to the native semantics, the synchronous semantics do not preserve durations. Instead, they are all expanded into unit step transitions; it is hence considered as "small-step". Due to its synchronous foundation, this semantics directly supports formal foundations such as mealy machines and digital circuits which are universally recognized formalisms, and are heavily used for formal verification. Hence, the goal of this semantics is twofold:

1. to study the relation between the two semantics, and thus, models the synchronous behavior of sLET languages;

to have a simpler model to start formal verification activities by reusing state-of-the-art synchronous verification techniques.

The semantics is defined by structural translation from PSYC to ESTEREL. Thus, we start by giving a brief overview of ESTEREL before defining the translation rules.

The ESTEREL language

This section gives a quick overview of the ESTEREL language inspired from [Ber02].

Signals and Reactions

ESTEREL is a Synchronous-Reactive language and thus, reacts continuously to inputs to give, logically instantaneous outputs. Said differently, an ESTEREL program maps an input sequence to an output sequence. At each reaction, outputs are given by a function from inputs as well as an internal state computed at the preceding reaction.

As other SR languages, ESTEREL is inherently concurrent and determinist. Internal and external communication is done through broadcasted signals that carry both:

-A status that denotes the presence or the absence of the signal; -And an optional value which is persistent when assigned. To distinguish both cases, signals are called valued when they carry a value and pure when they do not carry any value.

An ESTEREL program is wrapped-up in modules that can instantiate other modules: Here, the module M takes input I to compute output O using its internal statements as well as the local signal L. A reaction then computes a set of output status/value at each instant.

Statements

The core of the ESTEREL language is composed of imperative statements. In this work, we use a variation of those core statements that handle variables and valued signals as defined in [START_REF] Potop-Butucaru | Compiling esterel[END_REF].

p, q ::= nothing | pause | emit S | await S | v := exp | if c then p else q end | while c do p end | p ; q | p q | trap T in p end | exit T
Most of the statements detailed above a very classical and are defined in books such as [START_REF] Berry | The constructive semantics of pure esterel[END_REF]. nothing and pause respectively does nothing and pause (i.e., wait for) the current reaction. emit and await respectively sends and awaits a signal. A variable v can be assigned and can be used in if and while which are generalizations of, respectively, a condition and a conditional loop with condition c based on boolean variable evaluation. Finally, the last statements express the more classical control-flow. We also omit signal and variable declaration for clarity.

Overview of the semantics

The behavioral semantics of ESTEREL is classically described in terms of rewriting rules, similarly to our native semantics described in the previous section. Each statement is rewritten to another one and reacts instantaneously to input signals with output signals. As in our native semantics, a statement rule can either take time or not; however, contrary to our native semantics, a rule taking time only takes one instant of some global base clock. Additionally, we consider a variation of the classical semantics taking into account variables and valued signals as shown in [START_REF] Potop-Butucaru | Compiling esterel[END_REF]. Definition 5.3.1 (Esterel semantics). Given a constructive ESTEREL program P and a set of data, the semantics of its transition is given by the following relation:

P, data Eo k ------ E i P , data
where E i and E o are respectively the input and output signal set active on the current reaction, and k, a boolean denoting the termination status (i.e., if it takes time or not) Let's describe more precisely the different statements given in the preceding section:

nothing rewrites to itself without taking time; -pause rewrites to nothing taking a single instant; -emit S emits S synchronously and rewrites to nothing without taking time; -v := exp assigns a variable and rewrites to nothing without taking time; CHAPTER 5 -Formal Semantics of PSYC if exp then p else q end rewrites without taking time to p or q depending on the expression evaluation;

while exp do p end rewrites without taking time to its body p followed by itself or to nothing depending on the expression evaluation;

p ; q rewrites to q if p rewrites to nothing or to the rewriting of p followed by q;

p q rewrites to the parallel execution of both of its statements being rewritten and takes time only if one those does;

exit T is a special statement which doesn't take time but break the current control flow emitting a special signal;

trap T in p end works with the previous statement catching special exit signals and rewrite to nothing in this case.

await S takes an instant and rewrites to itself while the signal S is not present in the inputs.

There are classically two variants of this statement: immediate if it can terminate instantaneously or non immediate if the first instant always takes time. In this work, we use the second variant with an additional counter n on the number of awaited signal await n S More details on the ESTEREL semantics is given in appendix A.

ESTEREL translation principle

The translation principle is quite straightforward. All PSYC clock ticks are translated using ESTEREL signals. Those "synchronization" signals are either application inputs (i.e., source clock), or are generated by periodic clock modules (i.e., periodic clock). Agents are translated to modules which only synchronize on these clock signals using the ESTEREL await statement, replacing the PSYC advance statement. Finally, the control flow of the agent is very similar in PSYC and ESTEREL considering that body declarations and statements can be simulated by ESTEREL trap and exit statements.

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

An application is then composed of multiple concurrent agent modules, clock modules as well as temporal variable modules. There is no causality issue as 1) clock signals are only used by agents and cannot be emitted by them, 2) circular clock definition is forbidden in PSYC and 3) communication signals are always emitted in a delayed fashion, thus breaking all potential causality loops.

Translation Rules

Sources and Clocks Source clocks are just pure input signals whereas periodic clocks are signals generated by a clock module defined with respect to an other clock signal. It is composed of three advance statements: one to model the periodic delay, one to model the offset delay and an initial one to model the synchronization with the first tick of the input parent clock, only necessary when the latter is not present on the initial instant (i.e., translated by immediate in ESTEREL).

Listing 5.4 -Esterel translation rule of PSYC temporal variable

Agent The declaration of an agent is more complicated as it is not possible to implement a generic module agent similarly to clocks or temporal variables. Hence, each agent has to be translated to a dedicated ESTEREL module. Let's consider an agent, named ID, that is composed of the body b start , b 1 , ...b K and use the clocks c 1 , c 2 , ..., c J . Additionally, 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 output) 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. Furthermore, inputs temporal variables also have a depth parameter DEP T H i , which correspond to the history size. Finally, the agent starttime value is STARTTIME_VALUE while its clock is STARTTIME_CLOCK. For simplicity, we first give the definition of the agent interface below. -Initially, the agent waits for its starttime.

-Synchronous "small-step" Semantics of PSYC

69

-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 corresponding body is called -i.e., initially its start body;

-When a body has terminated, the control loops and the switch statement calls the corresponding next body;

-When a body has aborted -i.e., via a jump or an endbody statement -the trap catches the body exit and then the behavior is then similar as above. Listing 5.15 -Esterel translation rule of PSYC condition statement PSYC while statement, while exp do stmt, is translated by the equivalent ESTEREL while statement as shown below. It can be recreated with the core ESTEREL statements using the a combination of a trap/exit to model the exit condition and a loop.

while T (exp) do T (stmt) end Listing 5.16 -Esterel translation rule of PSYC loop statement 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 thesis. Indeed, in PSYC, most complex C expressions are actually defined outside of the language. The only specificity of PSYC expressions is the access to a temporal variable. This expression is expressed as $[n]temporal_in which denotes the access to temporal_in on the n th last sampled value.

It is translated by the ESTEREL expression below which access to the input temporal variable array at the corresponding depth. temporal_in[n]

Listing 5.17 -Esterel translation rule of PSYC temporal variable expression

Application The global PSYC application translation pattern is then the global parallel composition of all the modules defined above. Let's assume that we have an application composed of:

-the sources s1, s2, ..., sn -the clocks c1, c2, ..., cJ;

-the temporal variables tv1, tv2, ..., tvN with the respective history depth DPETH1, DEPTH2, ..., DEPTHN;

-and the agents ag1, ag2, ..., agM.

Listing 5.18 -Esterel translation rule of a PSYC application

In this translation pattern, agent parameters are given implicitly. 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 apart from the source clocks. But actually, in practice, 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.

-Equivalence between both semantics 73

Equivalence between both semantics

Based on the introduced PSYC semantics and its ESTEREL translation, this section gives an observational equivalence between them for individual agents. Informally, both semantics define equivalent states on the boundaries of the elementary actions since the synchronous one only expand time interval into a succession of atomic transitions. By equivalent state, we mean that the syntaxical states from each semantics are equivalent with respect to the synchronous translation pattern and that the local environments from each semantics are also equivalent. However, the intermediate states of the synchronous semantics inside an elementary action can not be compared to any states of the native semantics for individual agents; informally, they represent evolution of the clock constraints but not the computations. This result is based on the PSYC operational semantics that has been given in chapter 5.2 and the ESTEREL semantics that is sketched in section 5.3.1.3.

We first consider equivalence of data between the PSYC native semantics and the ESTEREL translation. Similarly to the PSYC native semantics environment, the ESTEREL data environment corresponds to agent private variable, temporal variable copies, next body value . . . Thus, we write E ≈ data which denotes that PSYC agent environment E is equivalent to ESTEREL environment data.

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.

T (p ag ), data E -----P 1 , data 1 . . . E -----P n , data n such that T (p ag ) = P n and C ≈ data n .
Proof.

By structural induction on native rules structure. Full proof is given in appendix A.

Note that theorem D.1 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. Additionnally, this equivalence result only adress a single agent while an application is actually a system of multiple agents, as described in both semantics. However, as this equivalence holds for each agent, it naturally generalizes multiple agents.

Nominal mode only

Degraded mode only

Fast GNC

Illustration

As an illustration of both semantics, we shall consider a very simplified version of the control system of a spaceship introduced in [CPBL + 15], called a Guidance, Navigation and Control system (GNC). This use-case is composed of three tasks: Fast which interacts with the sensors and actuators, GNC which is responsible for the control and guidance functions and Thermal which is responsible for 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 5.3.

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

In nominal mode, the native semantics yields the following infinite trace for agent GNC: 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 following unit transitions:

C ag = == ⇒ 100 C 1 ag 1 GNC() = ====== ⇒ 30 C 2 ag 2 = == ⇒ 70 C 3 ag 3 GNC() = ====== ⇒ 30 C 4 ag 4 . . . 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]
P, data GN C() E 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 5.4a illustrates this equivalence at the agent level while figure 5.4b illustrates how the parallel operator from section 5.2.2 allows building a unique automata from a network of agent automata.

THIRD PART

Formal Verification for synchronous LET

For it would suffice for them to take their pencils in their hands and to sit down at the abacus, and say to each other : calculemus.

-G.W.Leibniz, Calculus Ratiocinator (1670).

CHAPTER 6

Temporal Requirements In the first part, we detailed the need for an approach based on logical time to specify precise and deterministic temporal constraints, mandatory for safety-critical domains. In the last part, we gave the formal semantics of PSYC based on synchronous LET, a formalism inherited from both Synchronous-Reactive and Logical Execution Time. PSYC allows the temporal behavior of such program to be specified precisely.

More specifically, the PSYC language focuses on the specification of explicit temporal constraints inside sequential agents (i.e., using the advance statement). These agents then communicate together through dedicated dataflow channels. Hence, more global temporal requirements such as the relative rate of multiple agents or the end-to-end latency of communication chains are largely implicit. The goal of this chapter is to formalize a set of common temporal requirements that will be used in the following chapters in PSYC formal verification problems.

Temporal requirements for PSYC

Formally, the synchronization instants of agents are also logical clocks. We can also consider a subset of them corresponding to the activation instants of some specific function, as well as some conditional activation corresponding to a PSYC conditional branch. In this chapter, we assume that we already have those clocks modeling some agent instants; next chapter clarifies the link between those clocks and the PSYC code. Considering that the execution of a PSYC application can be represented as a set of logical clocks, a PSYC application is actually multi-clock even if all agents are based on a unique source clock. Thus, the requirements that we want to specify are mainly temporal constraints among multiple agents; they specify constraints among the rate of multiple agents or constraints among the data propagation among multiple agents.

In this thesis, we focus on four kinds of requirements inspired by specification languages such as TADL2 [START_REF] Peraldi-Frati | A timing model for specifying multi clock automotive systems: The timing augmented description language v2[END_REF] or AUTOSAR Timing extensions [START_REF] Scheickl | Tool support for seamless system development based on autosar timing extensions[END_REF]:

-Repetition requirements specify a constraint on the repetition of successive instants of a single logical clock. It is typically used to show the periodicity of a clock.

-Synchronization requirements specify the synchronization among multiple logical clocks. It is typically used to show that multiple concurrent computations are triggered on the same instant. More generally, we consider that synchronization requirements correspond to invariants among multiple agents. This includes synchronization, but also exclusion or subclocking constraints.

-Causality requirements specify that the instants of an agent precedes the instants of an other agent. More generally, causality requirements can specify alternation patterns between two agents. They are often used to specify communication patterns between agents such as no data is loss or the consumer is twice as fast as the producer.

-Delay (or latency) requirements specify the delay between a stimulus instant and a response instant. Delay requirements can be applied either on two instants of a same agent or on instants of multiple agents to model the propagation of a data. In that case, if the delay is applied for each response instants, this requirement is often called Freshness, and if the delay is applied for each stimulus instant, this requirement is often called Reaction. The former is usually used in systems such as automatic cruise control in which the age of a data is really important, and the latter is usually used in systems such as airbag control in which the presence of a response is critical.

In addition to those requirements, agent instants can be causally related to model agent communication; this is often called functional chain or event chain [START_REF] Feiertag | A compositional framework for end-to-end path delay calculation of automotive systems under different path semantics[END_REF]. Informally, if a data is tagged and used as a stimulus to the model, assuming that the tag is propagated in all computations, then its corresponding response also contains that tag. However, defining functional chain usually faces two issues:

1. When a consumer has a higher frequency than a producer, then some values are read multiple time; this is called oversampling. In that case, the functional chain is split into multiple branches, going to different consumer instant.

2. When a producer has a higher frequency than a consumer, then some values are overriden; this is called undersampling. In that case, the functional chain faces a "dead-end"; the data is not propagated.

Usually, in the literature [START_REF] Feiertag | A compositional framework for end-to-end path delay calculation of automotive systems under different path semantics[END_REF], a Reaction requirement considers only the first branch derivation (issue 1) and a dead-end is considered to be an error, due to infinite latency (issue 2). On the contrary, a Freshness requirement considers all the branch derivations (issue 1) that yield a response; so dead-ends are ignored (issue 2).

As mentionned in the introduction, the most common logics used to formalize requirements are temporal logics. However, in our case, the requirements are expressed as constraints among multiple logical clocks -the agent synchronization instants. Thus, we use CCSL as it naturally express constraints among different logical clocks whereas the operators of temporal logics focuses on a single timeline. Next section gives an overview of the CCSL specification language.

The CCSL language

This section gives an overview of the CCSL language inspired by the presentation given in [START_REF] Mallet | Correctness issues on marte/ccsl constraints[END_REF].

Time model

A CCSL specification is defined as a set of logical clocks, as defined in cahpter 4, constrained by a set of constraints defining when the clocks can tick. The definition of those logical clock is the same as the one used for synchronous LET; it is a sequence of instants, totally ordered, that can represent any action of the system (e.g., task activation, communications . . . ). The CCSL constraints specify causal and simultaneity constraints between clocks; they are used to constrain the clocks either for synthesis (finding a schedule of the clocks) or verification (verify the constraint on the system events). Definition 6.2.1 (CCSL clock). A CCSL clock is a logical clock defined by an infinite sequence of instants (c i ) i∈N * (i.e. the clock ticks) Definition 6.2.2 (CCSL specification). A CCSL specification is defined as a tuple C, Cons , where C is a finite set of logical clocks and Cons a finite set of constraints.

A schedule of a CCSL specification states when clock tick in the system. It assigns a date to each tick of a clock set using a common time basis. It can be seen as a possible execution of the model, and is considered valid only if it satisfies the constraints of the specification defined in the next section. We also define the state of a clock that we call history. Informally, the history of a clock at an instant i with respect to some schedule is the number of ticks the clock has made before (and including) this instant.

CCSL Constraints

: c 1 ⊂ c 2 Subclock c 1 ≺ c 2 Strict Causality c 1 c 2 Causality c 1 ∼ c 2 Alternation c 1 # c 2 Exclusion c 1 ≡ c 2 Coincidence CCSL Expressions : c 1 + c 2 Union c 1 * c 2 Intersection c 1 ∧ c 2 Infimum c 1 ∨ c 2 Supremum c 1 -- c 2 Strict Sampling c 1 -- c 2 Sampling c 1 $ n on c 2 Delay
χ σ (c, 0) = 0 ∀n ∈ N * ,χ σ (c, n) = χ σ (c, n -1) if c ∈ σ(n) χ σ (c, n -1) + 1 otherwise
In the literature, CCSL is often used in synthesis problem: one want to find an execution, or a schedule which satisfies the specification. But CCSL can also be used in verification problem. In that case, the clocks are mainly mapped to events of the system to be verified. Thus, they already have schedules corresponding to system executions. In our case, the events of the system are the agent clocks. Definition 6.2.5 (CCSL verification). A system satisifies a CCSL specification C, Cons if and only if all the execution paths of the system σ system is a valid schedule.

Additionally, CCSL clocks can also be refined using expressions. Next section describes both CCSL constraints and expressions.

Constraints and Expressions

There are two kinds of CCSL constraints: stateless and stateful. The former only relies on the presence or absent of clock ticks while the latter also relies on the state of the clock. The Figure 6.1 shows the syntax for the main constraints and expressions of CCSL that we use in this work.

A first basic constraint is the subclock constraint, which states that a clock has all its tick that coincides with those of another clock. Definition 6.2.6 (subclock). Let a, b be two logical clocks, then a is a subclock of b (noted

a ⊆ b) if: a ⊆ b ∀i ∈ N, a ∈ σ(i) =⇒ b ∈ σ(i)
We will also use the exclusion constraint which states that two clocks never have ticks that coincide. Definition 6.2.7 (exclusion). Let a, b be two logical clocks, a is in exclusion with b (noted

a#b) if: a#b ∀i ∈ N, ¬(a ∈ σ(i) ∧ b ∈ σ(i))
Some other constraints are stateful. As an example, the causality constraint states that a clock on a given index, a clock instant a i always happen before another clock instant b i .

Definition 6.2.8 (causality). Let a, b be two logical clocks, a causes b (noted a b) if: a ∀i ∈ N, χ(a i ) ≤ χ(b i ).
The causality constraint can be made strict (noted a ≺ b) when a strict order is used between history of both clock.

Basic logical operator can be used between clocks as expressions; they are applied to each instant of a schedule. Definition 6.2.9 (union/intersection). Let a, b and c be three logical clocks, c is the intersection (resp. union) of a and b (noted

c a ∧ b, resp. ∨) if: ∀i ∈ N, c ∈ σ(i) ⇐⇒ a ∈ σ(i) ∧ b ∈ σ(i) (resp.∨)
Another expression, more specific to CCSL is the Infimum (resp. supremum) expression which defines the slowest (resp. fastest) clock of two other clocks. Definition 6.2.10 (infinum/supremum). Let a, b and c be three logical clocks, c is the infinum (resp. supremum) of a and b (noted c a ∧ b, resp. ∨) if: ∀i ∈ N, χ(c, i) = min(χ(a, i), χ(b, i)) (resp. max) CCSL also defines sampling operator which defines a clock corresponding to a sampling of one clock to another. This can be used to model sampling communication. Definition 6.2.11 (sampling). Let a, b and c be three logical clocks, c is the (strict) sampling of a

on b (noted c a - - b) if: ∀i ∈ N, c ∈ σ(i) ⇐⇒ (∃j < i, b ∈ σ(j) ∧ b ∈ σ(i) ∧ (χ(b, i) - χ(b, j)) = 1 ∧ (∃k, j ≤ k < i, a ∈ σ(k))) If sampling is non strict, the ordering is j < k ≤ i.
Finally, we also define the CCSL delay operator which is used for latency and delay constraints. Definition 6.2.12 (delay). Let a, b, and c be three logical clocks, c is a delayed by

N ∈ N * based on clock b (noted c a $ N on b) if: ∀i ∈ N, c ∈ σ(i) ⇐⇒ b ∈ σ(i) ∧ ∃j ≤ i, a ∈ σ(j) ∧ (χ(b, i) -χ(b, j) = N )
We also often used a clock which is delayed on itself; we write it a $ N which is equivalent to a $ N on a.

Various extended constraints and expressions operators can be derived using the basic one defined above. Coincidence is derived by a double subclocking -a ≡ b is true when a ⊂ b and b ⊂ a -and (strict) alternation is derived by a double causality with delay -a ∼ b is true when a ≺ b and b ≺ (a $ 1). For an in-depth introduction to CCSL, the reader might consult [START_REF] André | Syntax and semantics of the clock constraint specification language (ccsl)[END_REF]. As explained in [START_REF] André | Verification of clock constraints: Ccsl observers in esterel[END_REF], CCSL can also be used along with a system model to perform verification. Traditionally, in the Synchronous-Reactive community, properties to be verified are expressed as synchronous observers. They are synchronous components that observe the system's behaviors and raise an error signal if the property is invalid. This approach is actually quite similar to more traditional model-checking in which a language acceptor -usually a Buchi automata -validate the system's traces. In [START_REF] André | Verification of clock constraints: Ccsl observers in esterel[END_REF], CCSL constraints are translated to synchronous observers encoded in the ESTEREL language using the CCSL semantics. Figure 6.2 is extracted from [START_REF] André | Verification of clock constraints: Ccsl observers in esterel[END_REF] and gives an overview of the methodology: CCSL constraints are translated to observers and CCSL expressions to generators; both are encoded in ESTEREL and connected with the main ESTEREL program. Full verification methodology is detailed in next chapter and uses this encoding along with the ESTEREL translation of PSYC given in chapter 5.

Synchronous observers

Encoding requirements in CCSL 6.3.1 Repetition requirement

The repetition constraint is basically a delay constraint between successive instants of a clock. In its most simple form, the repetition constraint can be defined as a coincidence with some periodic clock.

Repeat(c, P , O, b) c ≡ c P ×b+O (6.1)
where c P ×b+O is a periodic clock defined with respect to b with a period P and an offset O.

However, if we want to omit the offset parameter, we have to specify a constraint in which two successive instants shall exactly have a delay of a period respectively to some base clock. It is defined as following:

Repeat(c, P , b) c $ P on b ≡ c $ 1 (6.2)
where P is the period and b is the base clock.

The constraint can be generalized with a delay interval between successive instants defined by P min and P max .

Repeat(c, P min , P max , b) c $ P min on b c $ 1 c $ P max on b (

There exists multiple variations of the definitions above such as defining repetition by a jitter on some reference clock. In this work, we only use the basic definitions above, but variations can also be defined using CCSL.

Synchronization requirements

The synchronization constraint, in its strict form, can simply be defined as a coincidence between clock.

Synchronization(c 1 , c 2 , . . . c n ) c 1 ≡ c 2 ∧ c 2 ≡ c 3 ∧ . . . c n-1 ≡ c n (6.4)
Additionally, the constraint can be extended with a tolerance parameter that defines the delay between the first and the last synchronized clock. This is defined using the inf and sup parameters to define the first and last clock a synchronization:

c min n i=1 c i (6.5) c max n i=1 c i (6.6) Synchronization(c 1 , c 2 , . . . c n , T, b) c max c min $ T on b (6.7)
Where T is the tolerence parameter defined on b, a base clock.

Causality requirements

We also consider various variations of causality requirements. In its most basic form, causality is directly represented with the causality operator in CCSL:

Causes(c 1 , c 2 ) c 1 c 2 (6.8)
However, implementing this operator would require an unbounded counter. Hence, we consider only bounded variations of this operator mostly based on the alternation constraint.

Delay and Latency requirements

The delay constraint is probably the most complex due to the multiple semantics variations. We consider first a strict delay constraint in which the delay between two instants with index i of two clocks c stimulus and c response is bounded by some interval [D min ; D max ]:

StrictDelay(c stimulus , c response , D min , D max ) (c stimulus $ D min on b) c response (c stimulus $ D max on b) (6.9)
However, in some situation such as reaction requirements, one only wants to specify the delay between the instants of c stimulus and the upcoming instants of c response . In other words, we also want to specify for a given instant of c stimulus , the minimal and maximal delay up to the next instant of c response . We call it forward delay and define it as following:

F orwardDelay(c stimulus , c response , D min , D max ) (c stimulus $ D min on b) (c stimulus - - c response ) (c stimulus $ D max on b) (6.10)
Alternately, in freshness requirements, one may also want to specify the delay between the instants of c response and the foregone instants of c stimulus . We call it backward delay because we use the c response clock as reference; in this semantics, contrary to Forward or Strict delay, a stimulus event might not be mapped to a response event; however, all response events should have a preceding stimulus event. We specify here the maximal delay between a given instant of c response and the previous instant of c stimulus as following:

BackwardDelay(c stimulus , c response , D max ) (c response - - (c stimulus $ D max on b)) (c response $ D max on b) (6.11)

-Encoding requirements in CCSL 87

We don't show minimal backward delay constraint as its formalization is more complex; the idea is the same, however. Additionnally, as the two constraints ForwardDelay and BackwardDelay are used for end-to-end latency, they need to focus on a specific data propagation in the system. Next section details how to extract those paths using functional chain definitions.

Functional chains

We now define functional chains that can be used with the requirements defined in the previous sections. Informally, a functional chain represents a possible data propagation in a system modeled by a sequence of task writings and readings (hence, by TSPs). The modeling of such requirement is rather complex due to the existence of multiple data propagation path, due to communication over/under-samplings, and that it depends on the communication semantics of the system. In this paper, we consider a semantics based on a buffer-like communication using PSYC temporal variables and sLET synchronization.

We give the semantics of a functional chain composed of tasks t 1 , t 2 , . . . t n . Those tasks are composed of two events t i start and t i end corresponding to the activation and deadline instant of the elementary action of the agents.

A functional chain is composed of specific instances of those tasks corresponding to a data propagation path. We note them p 1 , p 2 , . . . p n and we define their start and termination such that:

∀i ∈ [1, n], p i start ⊂ t i start ∧ p i end p i start - - t i end
Then, the propagation rule relates a producer and a consumer using a simple constraint; the producer termination instant is related to any of the upcoming consumer starting instant before the next producer termination instant (in which a new data is propagated). This is defined as following:

∀i ∈ [1, n -1], p i end p i+1 start ≺ (p i end - - t i end )
Then, for all input data x such that x ⊂ t 1 start and x = p 1 start ; the constraints above define all the possible data propagation path in which p n end is the functional chain output. It can be used either with forward delay, for reaction constraints, or with backward delay, for freshness constraint.

However, the rule above assume that the producer and consumer communicate directly, but in practice PSYC use communication means. The rules are rather generic and can be adapted to a temporal variable tv i , as they can be modeled as synchronous tasks (i.e., tv i = tv i start = tv i end ).

Hence, assuming task t i communicate with task t i+1 using tv i , the rule can be adapted as following:

∀i ∈ [1, n -1], p i end tv i ≺ (p i end - - t i end ) ∧ tv i p i+1 start ≺ (tv i - - tv i )

Example

Let's consider again the GNC example shown in chapter 4 and 5. On such use-case, the typical requirements are -a repetition requirement on the Fast agent as a period of 1 millisecond; -a causality requirement between Fast and GNC to specify that Fast should be 10 times faster than GNC. Thus, one value is actually used by GNC every 10 occurrence of Fast.

-a reaction end-to-end latency requirement between Fast, GNC and back to the Fast task which should be smaller than 130 milliseconds. Figure 6.3 illustrates the end-to-end latency requirement on the GNC example. The red instants and arrows represent the possible propagation of the functional chain. Such functional chain can be modeled in CCSL using the definitions shown in section 6.3.5, on which the BackwardDelay as defined in section 6.3.4 can be used.

Summary

This chapter gave formal definitions of the most common requirements that we are interested, in the context of synchronous LET models and the PSYC language. Most of these properties are highly inspired from AUTOSAR related work, such as TADL2. Regarding CCSL, all these definitions are also pretty classical except the end-to-end latency requirement.

Verification: General Case Two formal semantics are given for PSYC in the second part of this thesis: a native semantics preserving the logical durations of elementary actions and a synchronous semantics in which elementary actions are expanded into a succession of atomic transitions. In this chapter, we consider the synchronous semantics for formal verification as it naturally generalizes to PSYC programs with multiple source clocks and directly supports formal models such as mealy machines. We detail how CCSL temporal requirements -described in chapter 6 -modeled as synchronous observers can be verified on a PSYC program. To do that, we encode both the observers and the program in Symbolic Transition Systems (STS) -which correspond to symbolic representation of mealy machines -and then give them to symbolic model-checkers.

However, this approach has an obvious drawback; synchronous Logical Execution Time uses logical time to specify both the triggering instants and the durations of computations. PSYC programs often have long durations, that are split in a succession of atomic reactions by the synchronous semantics. This yields a lot of unnecessary states that makes model-checking blow-up.

Next chapter discusses how the native semantics can be used to compress the state space using techniques inspired from timed automata model-checking.

Background

Circuit semantics of Esterel

Historically, the ESTEREL Inria compiler had two main compilation techniques: automatabased and circuit-based. The former generates a global automata based on the ESTEREL behavioral semantics while the latter generates a digital circuit represented as a netlist based on the ESTEREL circuit semantics. In practice, automata-based compilation technique does not scale to reasonable applications; the generated automata can grow exponentially due to concurrency. Circuit-based compilation, while being usually slower at runtime, scales better and is thus, more adapted to formal verification. Formally, a digital circuit is equivalent to a symbolic representation of mealy machine that we call symbolic transition system; it is detailed in next section. The ESTEREL circuit semantics is used both for PSYC programs using the synchronous semantics and for CCSL modeled as synchronous observers. We now give a brief overview of the ESTEREL circuit semantics.

The interface of an ESTEREL statement is shown in the leftmost circuit of

Symbolic Transition System

Most modern model-checking tools use a symbolic representation of the state space to avoid dealing with the expanded state space in input. Some model-checkers, such as CADP [START_REF] Garavel | Cadp 2010: A toolbox for the construction and analysis of distributed processes[END_REF], then expand the state space to verify properties -they are called enumerative -while others, such as NUXMV [CCD + 14] or PROVER PSL [pro23], use symbolic verification techniques to avoid expanding the state space -they are called symbolic. In practice, symbolic model-checkers scale way better for Synchronous-Reactive languages [START_REF] Raymond | Synchronous program verification with lustre/lesar[END_REF]. We define in this section the concept of Symbolic Transition Systems (STS) as a common input formalism to the two modelcheckers that we use -NUXMV and PROVER PSL -as they take a syntaxical variation of STS in input, namely SMV and HLL. Symbolic Transition Systems is, informally, just a symbolic representation of state machines such as mealy machines. The idea is that a state is modeled by a valuation of a finite set of variables. Initialisation and transitions are then both modeled by predicates defining respectively possible initialisation valuations and possible valuation transitions. ESTEREL circuit semantics can directly be modeled as STS considering that registers are state variables and wires are equations. Definition 7.1.1 (Symbolic Transition System (STS)). A symbolic transition system is a tuple V, Init, T rans where:

1. V is a finite set of (finite) typed variables for which a valuation represents a state of the system;

2. Init(V) is a predicate representing the initial states;

3. T rans(V, V ) is a predicate representing the state transitions.

As an example, let's consider a clock of period P . The following STS models the dynamic behavior of this clock:

V = {c, t} Init c = 0 ∧ t = true T rans c = (c + 1) mod P ∧ t = (c = 0)
where c is an integer defined on [0; N [ and t is a boolean which denotes the clock ticks.

Symbolic Model-checking

Symbolic model-checking then uses the synchronous composition of an observer and a PSYC program modeled as STS. Basically, those tools only perform a reachability analysis on the observer output to ensure that violation of the observer never happens. Additionally, observers can also be used to model assumption of the environment; in that case, the output of the requirement observer is checked only if the output of the "assumption" observer is correct. This approach is often called "assume-guarantee" [BCE + 03]. -

Init 0 = M Init(M 0 ) ∧ P Init(P 0 ) -T rans i = M T rans(M i-1 , M i ) ∧ P T rans(P i-1 , P i ) -OK i is the ok signal in P i (at instant i)
In the literature, there exists a lot of different techniques to perform reachability analysis on STS-like models. Let's describe the main ones:

-Enumerative technique: the traditional approach is to compute the set of reachable states R by successively applying the transition formula until a fixpoint is reached. Then, one has to ensure that bad states B are not contained in the reachable set R ∩ B = ∅. This approachcalled forward reachability -tends not to scale as it explicitly computes the reachable set.

-Binary Decision Diagram techniques (BDD): BDD model-checkers implement a variation of forward reachability in which the set of reachable state is represented symbolically using Binary Decision Diagrams. These data structures provide a more efficient representation and manipulation on the state space. NUXMV is a model-checker that implements BDD forward reachability.

-Bounded Model-Checking technique (BMC): Bounded model-checking encodes a variation of our reachability definition to check successively if the property is true until a bound k ∈ N * , using SAT or SMT solvers. Both PROVER PSL and KIND2 [START_REF] Champion | The kind 2 model checker[END_REF] are modelcheckers that implement BMC, the former uses SAT while the latter uses SMT.

-Induction techniques (IND): induction techniques try to solve the incompleteness of BMC. Instead of verifying the property until a bound k, the property is proven using an induction principle. Basically, the idea is to show that:

1. Init 0 |= OK 0 2. ∀i ∈ N * , T rans i ∧ OK i-1 |= OK i
Model-checkers like PROVER PSL and KIND2 use a variation of this induction principle called K-induction to prove properties using SAT and SMT. In complement to induction, they also both support invariant generation and interpolation techniques This section gives the translation rules to encode PSYC programs as STS. To do that, we combine the synchronous semantics of PSYC and the ESTEREL circuit semantics sketched in the preceding section. Encoding of CCSL observers in STS is beyond the scope of this thesis, but is described in [START_REF] André | Verification of clock constraints: Ccsl observers in esterel[END_REF].

Extending PSYC agents with verification signals

For verification, agents should be extended with dedicated signals used for verification; they are logical clocks modeling the rate of agents or one of its functions. We extend PSYC using three different annotations:

1. First, we can name advance statements using the syntax @name, advance ... with ...;

When the advance statement terminates, a signal is emitted named after the label.

2. Second, we add probe statements in PSYC code using the syntax probe @name;

When the preceding statement terminates, a signal is emitted named after the label.

3. Finally, as data is not evaluated in our STS encoding, we can also annotate the conditions using the syntax @name if ... then ... else ...

If the name label is present, then the condition of the if statement is driven by an input signal named after the label, otherwise, it's a non-deterministic choice as expressions and values are not interpreted.

Translation principle

Instead of taking the circuit generated from the Inria compiler, we chose to give a dedicated circuit translation optimized for the PSYC language as the synchronous semantics only deals with a small part of the ESTEREL language.

The ESTEREL circuit interface can be highly simplified due to the structure of PSYC programs. This simplified interface is shown in the rightmost circuit of Figure 7.1:

-First, in the inputs, only the Go pin is necessary. Res and Susp can be removed as the ESTEREL Abort and Suspend statements are never used. Furthermore, Kill is also not necessary because Exit and Trap correspond to a change of Body. In that case, the registers are unset because of the sequential behavior of a PSYC agent.

-Second, in the outputs, Sel can be removed for the same reasons as Res. Moreover, Stop can be deduced from Term and Trap, which is renamed endbody to fit the PSYC vocabulary. -Finally, we split the input signals in the top part to have a separated input set called Clock, which is a set of input signals that trigger PSYC advance statements. Data correspond to input and output variables of a statement. The PSYC circuit interface described above is only used for PSYC statements; we describe source and clocks in the next section using STS. As explained in the last chapter, we do not translate expressions as values are not interpreted. Also, temporal variables components are not translated either as they are modeled into the functional chain definitions of the properties.

Sources and clocks

Similarly to the synchronous semantics, source clocks are just input of the model; periodic clocks are encoded in STS as following:

V = {parent, c, t} Init c = (O if parent else O + 1) ∧ t = ((c = 0) ∧ parent) T rans c = ((c -1 if c > 0 else P -1) if parent else c) ∧ t = ((c = 0) ∧ parent )
which corresponds to following PSYC clock definition clock t = P * parent + O;.

The initialization of the counter c might seem surprising as depending on initial value of the parent clock, we set it to O or O + 1. It is because the offset is counted starting on the first tick of the parent clock, hence: -If the parent clock is present on the first instant, we start immediately to count the offset; -Otherwise, we wait for the first tick of the parent clock before counting the offset. Hence, we wait for O + 1 tick. In the synchronous semantics, the clock is encoded starting by the statement await immediate parent; it can be proved equivalent to this STS definition.

Statements

Basic statements

All the basic statements of PSYC are translated straightforwardly using the ESTEREL translation. As shown in Figure 7.2, nothing terminates instantaneously, next sets the next body variable and endbody terminates instantaneously and exit the current control flow. One might remark that we do not consider computations and variable assignments; as we cannot interpret them, they are abstracted in the circuit translation. 1. When Go is selected, then reg is set and the agent stops on this advance statement; 2. While Clock(c) is not absent, reg is reloaded at each instant; 3. When Clock(c) is present (and Go is not set again), reg is unset and Term is set; the instruction has terminated.

Remark that endbody is always absent as the advance instruction never break the control-flow; once started, it can only stop or terminate.

This statement can be generalized easily using a counter as shown in Figure 7.4. The advance1 circuit is reloaded until the counter is bigger than zero. The buffers denote local update or condition on the counter state variable. One may remark that there is a potential conflict on the or gate when merging different assignment of the counter variable. In fact, both are mutually exclusive: as an agent is sequential, if the go signal is set, it means that the current statement is either not active or has terminated in the same instant. In the latter case, the counter is equal to zero, so the upper branch of the or gate is not set.

Control statements

The PSYC sequence statement s 1 , s 2 , . . . s n is translated in the circuit shown in Figure 7.5. Basically, when a statement terminates, the next one starts unless the endbody is set (both outputs are mutually exclusive). The PSYC if statement if (exp) s 1 else s 2 is translated in the circuit shown in Figure 7.6. First, the expression exp is replaced by a fresh signal called condition as we abstract expressions. This new signal is an input of the model and could also be used in the verification; next sections will show how it could be done. This condition signal is used in the circuit to start the correct statement. The PSYC while statement while exp do s is translated in the circuit shown in Figure 7.7. Similarly to the if statement, exp is replaced by a fresh signal called condition. The internal statement circuit is started when condition is set and either when the whole while statement has been started or when the internal statement has terminated. Conversely, the while statement terminates when the condition is unset and either when the whole while statement has been started or when the internal statement has terminated. which is set on the initial instant and unset on subsequent ones, and the current_body is initially set to "start".

2. When the starttime has terminated, the selected body is started. When this body has terminated or has reached an endbody statement (early exit), the next selected body is started, and so on.

Example

Let's consider again the GNC PSYC agent and its ESTEREL translation, used in previous chapters. Figure 7.9 shows on the left side a modified version of the GNC agent in which verification signals have been added while the ESTEREL translation is given on the right side. This updated ESTEREL version have additional emit statements to broadcast specific synchronization instants

Experiments

Implementation

The methodology has been implemented in a tool called PsykAnalyst which takes a PSYC program, a CCSL specification and outputs HLL or SMV models used by external model-checkers -respectively NUXMV and PROVER SAT -for the verification process. Only basic optimisations are performed in PsykAnalyst, such as cone of influence analysis or structural simplifications. This tool has been implemented in the OCAML language in approximatively 5000 lines of code. Generation time is basically negligible comparing to verification time. Next section shows experiments on various use-case; they have all been performed on an Intel Core i9-2.3GHz machine, with 32Gb of RAM.

Benchmarks

The benchmark is composed of seven main use-cases; each one contains various variations. Unfortunately, we were unable to access to real industrial use-cases. However, we think that those applications cover different complexity aspects of the PSYC language. The following paragraphs quickly detail the different use-cases and various metrics are shown in Figure 7.11.

LED blinking

The LED blinking use-case is described in chapter 3. Two tasks are responsible to respectively switch on and off a led. The blinking period differ depending on a chosen led color in input. While not really realistic, this tiny example is sufficient to evaluate the verification of basic properties: a blinking period, an alternate causality constraint and a minimal and maximal delay between actions to model the duty cycle. Each of them should be verified in both mode.

Anti-lock Braking System The Anti-lock Braking System is a simple modal system modeling an automotive braking controller. When a pedal sends a brake commands, braking is computed by three set of tasks: a sensing task for each wheel, a common controller and a braking task for each wheel. The specification is composed of a repetition constraint on the sensing task, a reaction latency constraint on the whole functional chain and a synchronization constraint on the sensing task (breaking should be synchronized on all the wheels).

Rosace Rosace is a simplified longitudinal flight controller commonly used in control system papers. In practice, this use-case is very similar to the industrial use-case we have encountered; the latter usually have similar characteristics but are bigger. The particularity of Rosace is its simplicity; all tasks have a very simple periodic pattern. However, the difficulty lies in the verification of end-to-end constraints, namely, reaction and freshness latencies. Of course, in such systems, various approaches perform better than model-checking [START_REF] Forget | Verifying end-to-end real-time constraints on multi-periodic models[END_REF] but our approach tackles the general verification problem in PSYC allowing both advanced control-flow and multiple source clocks. Nonetheless, it is necessary to evaluate the performance of our tool using simpler applications. Landing Gear System (LGS) The Landing Gear System is a simplified landing gears controller of an aircraft which is detailed more precisely in the next chapter. On the opposite of the Rosace use-case, this system has complex control-flow due to the handling of the extension and retraction gears sequence. The system is composed of a main controller task embedding the system logic as an automaton and four other simpler auxiliary tasks to handle various pre and post processing of the data. As in Rosace, the two main constraints to be verified are a reaction and a freshness constraint. The former applies on the full extension/retraction sequence while the latter applies on the cockpit feedback.

Powertrain The final use-case is a simplified controller of an automotive powertrain. The architecture is composed of three main set of tasks: a task responsible to take the user pedal value, a set of task to compute the injections and a set of tasks which emit the injection pulses programmed by configuring bank resource. In our case, we consider the freshness of the emitted pulses according to the pedal command. This property is rather challenging because we have to relate both source clocks: one based on the crankshaft position and one based on a timer. In our case, we assume that the crankshaft clock has a repetition constraint between 200 microseconds and 1 millisecond (this corresponds roughly to 1000-5000 RPM); all the task activations are based on the crankshaft except the pedal one which has a period of 10 milliseconds.

Evaluation

In this section, we give quantitative results for each system model grouped by each constraint type: repetition, causality, synchronization and delay requirements. All requirement verification is evaluated with multiple solvers: Bounded Model-Checking (BMC) with PROVER PSL (up to an estimated model's diameter), Inductive (IND) and Interpolation with PROVER PSL, and Binary Decision Diagram (BDD) with NUXMV. Additionnally, the timeout has been set to 2 minutes. As shown in Figure 7.12, SAT techniques (both IND and BMC) tend to be quicker than BDD except on two requirements ABS2 and ABS3 which are actually requirements of the "long" mode of the ABS system. BMC tends to be quicker than SAT, but finding a correct model's diameter can be hard; in our case, the diameter corresponds roughly to the hyper-period of the systems. As discussed at the beginning of this chapter, all the verification techniques and tools do not give equivalent guarantees. We now discuss the soundness of our methodology divided in two axes:

-First, the generation of the output model by PsykAnalyst is quite direct, and the implemented optimization steps have already been detailed a lot in the litterature. The soundness of the translation procedure is a result of the equivalence criterion between the native and the synchronous semantics.

-Summary

103

-Then, the second part is the verification tool itself. BDD techniques, in our case using NUXMV, gives sound and complete results; this approach has been used in most classical synchronous verification problems. However, now, SAT and SMT techniques replace gradually BDD techniques. In our case using PROVER PSL, SAT techniques often gives better results than BDD. Among them, Bounded Model-Checking gives interesting results but, while being also a sound procedure, suffers from completeness problem; it can be hard to find a bound to stop safely the verification process. Induction is an other SAT technique which solves the completeness problem; the verification process can be quite fast when the model is inductive, but might also not converge otherwise. In our experiments, we heavily used the invariant generation and the interpolation engines of PROVER PSL to avoid non-convergence.

Summary

In this chapter, we showed how a circuit semantics as defined for ESTEREL can be used in the PSYC language, based on its synchronous semantics to give Symbolic Transition Systems. Then, we adapted the traditional verification methodology used in Synchronous-Reactive formalisms to PSYC: we showed how to extend PSYC with verification signals which are used by synchronous observers generated from CCSL constraints; the final model can then be verified using various verification strategies (BDD, BMC, IND . . . ).

CHAPTER 8

Verification: Mono-Source Case The methodology detailed in the last chapter give a direct solution to tackle the PSYC verification problem. However, as it is based on the synchronous semantics, durations are not preserved; they are split in sequence of atomic reactions. Hence, this approach suffers from scaling issues. However, to avoid external non-determinism -and thus ease certification -industrial applications are very often based on a unique source clock, leading to a simpler model. This chapter proposes different solutions to handle the "mono-source" verification problem. The common idea is to re-use, to some extent, the native semantics to keep only the states corresponding to synchronization instants (i.e., interval boundaries).

Problem statement

Consider again the simple task GN C considered in the previous chapters. This task has a period of 1 second and a duration of 300 milliseconds based on a source clock corresponding to a physical period of 100 milliseconds. Depending on the chosen periods, the number of states might change considerably, although the overall complexity of the system is exactly the same. The We can see that, even if the number of state variables is quite large due to the structural translation, it does not change even if the task period changes. However, the number of states grows linearly when the task period increases as well as the system's diameter. Nonetheless, in the four variations above, the example is functionally equivalent; we might want the state space -and more particularly the verification time -to not change significantly.

An obvious solution to this problem is to use the "best" clocks to limit the size of the state space. However, changing the clock definitions is not always simple or even possible. For example, a system might use very small durations in a some mode while having bigger one in an other mode. The system could also have some small duration that happen sparsely, for example once in a system's hyper-period. In such cases, it is not possible to change the clock definitions to obtain a smaller state-space.

Existing approaches

Abstract Interpretation Synchronous-reactive languages have usually a semantics that rely on atomic reactions even for long duration computations; this approach is not only an issue for realtime implementation, but also for formal verification. In this context, [START_REF] Halbwachs | Delay analysis in synchronous programs[END_REF] introduced an approach to extend BDD model-checking with abstract interpretation in the model-checker LESAR. This work has been then extended in the NBAC [START_REF] Jeannet | Dynamic partitioning in linear relation analysis: Application to the verification of reactive systems[END_REF]. In both cases, the approach relies on abstract domains -such as polyhedra -for the numerical part of the model while relying on BDD for the boolean part.

We first tried the tool LESAR using the polyhedra option without any success. However, we got encouraging results with the NBAC tool. Nonetheless, this approach tends not to be highly stable; it was unclear when the verification procedure could converge or not, due to the incompleteness of abstract interpretation. Timed Transition Systems Another approach is to consider that the system only has one external clock, which is often the case in industrial systems. In that case, timed verification techniques could then be used. The most popular one is probably model-checking of timed automata using Difference Bound Matrices (DBM) as in the tool UPPAAL [START_REF] Kim G Larsen | Uppaal in a nutshell[END_REF]. Other approaches based on Timed Transition Systems and SAT also exist as the one from NUXMV; however, very little details are given on how the verification process is done. This approach could not work directly on STS coming from the synchronous semantics as we need the durations of the model. Nonetheless, we could use durations coming from the native semantics; we can keep the structure of STS while having transitions based on those durations.

-A temporal optimization approach 107

We tried various examples with UPPAAL. When the examples were very simple, UPPAAL did perform great. However, in more realistic examples, UPPAAL was either significantly slower without optimization or performed similarly with optimizations such as convex hull. Additionnally, it seems that UPPAAL does not scale well when the model contains a lot of control. Also, this approach has been done manually with a lot of "manual" optimization. As the encoding is really different from STS, it has not been automated.

Integer Linear Programming In the particular context of multi-periodic system, we might also consider techniques independent from the control flow. In that case, the verification instants are reachable using linear expressions. Hence, Integer Linear Programming (ILP) could be used for the verification process. This approach also requires a significantly different encoding than STS and would only be usable only on a tiny subpart of PSYC.

Next section presents a more general approach relying on STS with durations, and fully compatible with all the model checkers we used in the last chapter.

A temporal optimization approach

We describe now a novel approach to handle durations symbolically. It is motivated by the fact that timed automata or timed transition systems can be simulated using classical transition systems. Some work show that internal structures of timed model-checkers -namely Data Bounded Matrices -can be used to simulate symbolically the durations of a timed automata. In our case, our problem is simpler as we only have to deal with constant durations (due to the mono-source constraint) but we focus on verification instead of simulation.

Symbolic Transition System with durations

The full advance statement circuit adds a counter to repeat n times the advance 1 circuit as shown in chapter 9. However, an other approach is to keep the logical duration of the advance statement coming from the native semantics. The Figure 8.1 shows the encoding of an advance in which a trigger of some clock c triggers the transition to the next advance with duration N defined as in the rule: C advance n with c = == ⇒ N ×s C nothing.

However, one might notice than in the native semantics, multiple logical durations can be assigned to the same advance statement depending on the state of the PSYC periodic clocks. The native semantics shows that a PSYC code can be unfolded so that each advance statement has a single duration. In practice, all our examples respect this assumption, so we don't considered this case. Nonetheless, if needed, the circuit can be generalized to multiple durations.

Symbolic abstraction of durations

As explained in previous sections, in the case of long durations, a lot of intermediate states representing temporal progression are generated; we sketch here an approach to aggregate those states. Based on the advance circuit shown in previous section, we can add a scheduler component that activates each agent depending on their constraints and jumps multiple cycles at once. We call this methodology temporal optimization. At the end of this chapter, experiments show that in some cases, this temporal optimization might give significant verification speed-up.

Basically, in an agent, each advance statement is triggered by a unique clock and a new duration output is added to them giving the duration of the current elementary action based on the active advance statement. The scheduler outputs a Delta signal which denotes the number of cycles jumped at each step depending on the state and the duration of each agents as shown in Figure 8.2. ∆ can then be used by the properties to adapt the synchronous observers -especially the delay constraint.

Scheduler

} Init clock 1 ∧ clock 2 ∧ . . . ∧ clock n ∧ state 1 = 0 ∧ state 2 = 0 ∧ . . . ∧ state n = 0 ∧ ∆ = min(duration 1 -state 1 , duration 2 -state 2 , . . . duration n -state n ) T rans clock 1 = (∆ = (duration 1 -state 1 )) ∧ clock 2 = (∆ = (duration 2 -state 2 )) . . . ∧ clock n = (∆ = (duration n -state n )) ∧ state 1 = 0 if clock 1 else (state 1 + ∆) ∧ state 2 = 0 if clock 2 else (state 2 + ∆) . . . ∧ state n = 0 if clock n else (state n + ∆) ∧ ∆ = min(duration 1 -state 1 , duration 2 -state 2 , . . . duration n -state n )
The detailed behavior is the following:

1. First, depending on the previous agent states and the previous ∆, the scheduler computes which agent is active in the current state. That is, when the previous ∆ corresponds to the agent's remaining time after the previous step, i.e., duration -states.

2. Then, the scheduler computes the new agent states which model the offset in their current elementary actions. If the agent is active on the current step, it means that it has reached a synchronization point, so the new state is 0. Otherwise, the new state corresponds to the previous one plus the new delta.

3. Finally, depending on the new agent states and the agent durations, the scheduler computes the new ∆ which jumps as the minimum of the agent's remaining time.

This behavior is, unsurprisingly, the one shown in the composition rule of agent network in the native semantics.

Let's take the GNC task and its variations from section 8.1. Using the optimization described in the previous sections we get, as expected, the same compressed state space in each variation, composed of 4 states, as shown in the However, there is a limitation with this result. The measured state space is actually the reachable state space in which non-reachable states are not accounted. When trying to build the GN C models with the model-checker NUXMV, we get, as expected, almost instantaneous property checking even with the larger variation of GN C. However, building the model in itself takes a lot more time than without optimization as we introduce multiple integer variables -up to an hour in the last variation when the original model took a few seconds. It seems that, in NUXMV, building the BDD of the model doesn't work when large integer variables are used, even if few states are actually reachable.

The Landing Gear System use-case

This section shows how the methodology could be applied to a realistic safety-critical usecase from the avionics domain introduced in [START_REF] Boniol | The landing gear system case study[END_REF]. Different tasks are added to the original use-case to reflect the complexity of realistic industrial software. The use-case describes a controller to handle the landing gears operations of an aircraft: gears extension and retraction using a mechanical electro-valve system. It is composed of 5 different tasks. The main task is the SequenceController which handles the extension or retraction sequence of the landing gears similarly to a state machine. The SequenceController sends its commands to the EVManager, which interacts with the electro-valves part of the mechanical system. The task SensorManager handles (and filters) sensors data which are used by the SequenceController to ensure that there is no discrepancy between the controller state and the real physical state of the system. The last two tasks are the ones interacting with the pilot. PilotManager takes the pilot handle value to send it to the controller, and the PilotFeedback task monitors the system to give feedback to the pilot: gears extended (green light), gears retracted (no light), gears moving (orange light) or failure (red light). All those tasks have been implemented in the PSYC language; we cannot show them here due to space limitations. Evaluation For such system, both techniques give satisfying results. In the case of PROVER PSL, all requirements are checked in about a second. Temporal optimization gives up to 95% speed-up, although we see that in r1 and r5, there is no significant difference. This is because the model can never jump multiple cycles at once. In the case of NUXMV, all requirements are checked in tens of seconds except r1, and temporal optimization does not give any speed-up except for r4; temporal optimization even makes the results worst. We think that this can be linked to the NUXMV model building and optimizations which is harder in the case of temporal optimization.

Summary

Based on the assumption that only one clock is used in the model, various approaches may perform better than the classical synchronous model-checking shown in the previous chapter. This chapter presented a new technique -fully compatible with the one shown in the previous chapter -based on simulating durations in the model; this approach is strongly inspired from DBM model-checking in timed automata.

FOURTH PART

Conclusion and Perspectives

Summary

The main objective of this thesis was to give a formal verification methodology for real-time applications based on logical time. We focused on the PSYC language -a parallel synchronous language based on a variation of Logical Execution Time -mainly due to the industrial context of this thesis. Two main contributions emerge from this thesis: firstly, we give semantics foundations for the PSYC language based on a new formalism that we call synchronous Logical Execution Time (sLET), and secondly, we give a verification methodology applied to the PSYC based on its semantics definitions. The two following sections sum-up those two contributions.

Synchronous LET and operational semantics

The PSYC language, in his current form, has never been formalized totally nor positioned with other existing formalisms such as the Synchronous-Reactive (SR) and the Logical Execution Time (LET) approaches. The first contribution of this work comes from a simple observation: the PSYC language actually inherits from both SR and LET. Hence, we defined a new model called synchronous Logical Execution Time (sLET) as an synchronous generalization of LET with logical clock synchronizations as in SR languages. This model is then used, in turn, to define two operational semantics for PSYC: a classical structural operational semantics called native (or "big-step") that preserve durations along its transitions whereas the second one is defined by a structural translation to a SR language -in our case ESTEREL -which gives a "small-step" behavior in which durations are expanded on atomic transitions. While the native semantics is very close to the one used in the current industrial compiler, the synchronous semantics gives an abstraction, allowing synchronous analysis and verification tools to be reused. Finally, we have also given an equivalence criterion between both semantics; the proof is shown in the appendix.

CHAPTER 9 -Conclusion

Formal verification of temporal properties

The main properties that we wanted to verify on the PSYC language come from higher-level temporal requirements and focus mainly on the timing of system functions, and in particular, the relative timing of different functions and how they interact, similarly to requirements of automotive specification [START_REF] Peraldi-Frati | A timing model for specifying multi clock automotive systems: The timing augmented description language v2[END_REF]. Examples of such requirements are synchronizations, or latencies on chain of task communications (called functional chains). Hence, the second contribution of this work was to formalize those properties in the CCSL specification language, a language allowing for the formal specification of clock constraints.

Based on the defined synchronous semantics of PSYC, and its equivalence criterion with the native semantics, we have defined a methodology to formally verify properties on PSYC -which can be actually generalized to other (s)LET languages -using a structural translation to symbolic transition systems and synchronous circuits. In this approach, we chose to encode our CCSL requirements as synchronous observers in the same format. To verify the properties, we mainly used symbolic model-checking based on Binary Decision Diagram (BDD) and Satisfiability (SAT). We have proceeded to a series of experiments showing that with most of our applications from our benchmark, requirements were verified in a few seconds.

However, the verification becomes more complicated when applications use particularly long durations; verification time increases exponentially for programs when increasing logical durations. This is mainly due to the synchronous semantics expanding all duration to atomic transitions. To face this issue, we defined a temporal optimization procedure to reduce the state-space assuming that only one source clock is used -which is often the case in industrial applications. This approach permit to jumps multiple cycles at once. Instead of using only the synchronous semantics, we add task durations coming from the native semantics, and a scheduler to keep track of the state of each task. This approach has been evaluated on a Landing Gears System case study showing up to 95% speed-up using SAT model-checking.

Finally,the whole methodology described above has been prototyped in a tool called PSYK-ANALYST. All the experiments have been done using this tool and various third-party solvers: NUXMV, and PROVER PSL. The tool takes a representative sub-part of the PSYC language and verifies CCSL requirements using one of the solver strategies; if the property is false, a counterexample is shown based on the one from the solver.

Perspectives

Semantics of PSYC null-latency communications

Null-latency communication is a special feature of PSYC that allows for the synchronization and communication between two tasks during their elementary actions. This is used, in turn, to simulate causal communication using so called fractional clock. Without going into details, synchronous LET natively supports null-latency, as fractional clock is just another logical clock used to express activation and deadline constraints. There are however multiple syntaxical difficulties 9.2 -Perspectives 117 that makes structural definitions more complex, in addition of dealing with causality issues. As such, both semantics could be extended with null-latency constructions. Nonetheless, verification of properties based on null-latency can already been partially done using CCSL definitions. One could then use those definitions to check the causality of null-latency constraints as well as verifying classical latency properties.

Synthesis of temporal properties

Synthesis is an other interesting topic to study in PSYC. First, synthesis of temporal constraints from high-level temporal requirements would allow the automatic generation of PSYC code. It is, however, a very complex subject as it can be quite complex to automatically choose from multiple possible PSYC designs satisfying the same set of requirements. Nonetheless, this is an ongoing subject at KRONO-SAFE, and is currently prototyped in a tool called DESIGNER. Second, synthesis could also allow PSYC programs containing multiple source clocks to be refined to a unique source clock or to extract sufficient conditions on the relative triggering of clocks, satisfying a set of high-level requirements. This could be used to refine a complex multi-source design to a simpler single-source design simplifying its compilation process.

Compositional model-checking Finally, PSYC verification could be extended by considering assume/guarantee contract on C code inside elementary actions. Such contracts could be verified using deductive analysis techniques with tools such as FRAMA-C [CKK + 12]. Then, modelchecking could use those contracts to constrain which branch could be taken by each task on each instant.

nothing, data

C Sources and clocks

In the proofs, we will assume that source clock always tick (as stuttering doesn't change the code). However, PSYC periodic clocks can refine successively source clocks to give richer patterns. Let's remind the ESTEREL translation of a clock clk_out with parent clk_in and with Period and Offset: Without going in the full detail, it is rather obvious that starting on the first tick of clk_in, this code generates clk_out with Offset and Period respectively to clk_in. So, considering that those are the relative period and offset with its parent clock, we can also define the absolute period and offset as following: So, similarly, we can rewrite a relative duration (the advance parameter) to an absolute duration (always relative to a source). So, assuming d c is the state of the clock defined as in chapter 5, we have:

N absolute = (Period clk absolute -d c ) + (N clk relative -1) × Period clk absolute
Thus, in the next section, we assume that clocks are always present since 1) durations relative to periodic clocks can be refined to absolute durations with respect to source clocks and 2) when source ticks are absent (stuttering), agent state does not change.

D Equivalence proof

We sketch here the proof of the equivalence between the native semantics and the behavioral semantics of ESTEREL. -Case compute: idem.

-Case while: idem.

-Case if: idem.

-Case advance N: First, the initial ESTEREL transition transforms await N in await immediate N taking one instant. Then, if N > 1, the remaining transitions can be proven equivalent by induction on N resulting in N -1 transitions taking n -1 instants.

The remaining ESTEREL statements are await immediate 1 ; emit S. The first statement is instantaneous (and thus can be optimized) and the second one is also instaneous but makes communication visible, which is equivalent to the update of the visible environment T in the PSYC rules.

-Case sequence s 1 ; s 2 : The ESTEREL translation T (s 1 ; s 2 ) is equivalent to T (s 1 ) ; T (s 2 ). Thus, if s 1 terminates without taking time in the PSYC rule, its ESTEREL translation T (s 1 ) also terminates without taking time, and with an equivalent environment, according to the basic cases described above (induction hypothesis). Thus, the remaining statement of the sequence is s 2 in PSYC and equivalently T (s 2 ) in ESTEREL. Otherwise, if s 1 takes N instants to s 1 , it is equivalent to the N ESTEREL transitions to T (s 1 ) according to the cases described above (induction hypothesis). Thus, the remaining statement is the sequence s 1 ; s 2 in PSYC and equivalently T (s 1 ) ; T (s 2 ) in ESTEREL.

-Case composition rule: This last case directly holds due to the equivalence of the advance case. Instantaneous transition are equivalent, thus, they can be composed with the transitions taking time.

Méthodologie de vérification formelle de propriétés temporelles pour les applications temps-réel critiques basées sur le concept de temps logique

Abstract

Safety-critical real-time systems have to respect strict timing constraints. Thus, timing constraints must be considered throughout the software development cycle. As exact computation execution time are generally not known during design, logical time provides a way to abstract time constraints and execution from platform-dependent physical time. In this thesis, we focus on two main formalisms based on logical time. The Synchronous-Reactive approach totally abstracts physical time by discrete time bases on which computations are triggered. The Logical Execution Time approach uses logical time bases to represent not only triggering instants but also the durations of elementary computations. In this thesis, we start by unifying Synchronous-Reactive and Logical Execution Time approaches. This provides the natural formal framework for defining the semantics of PSYC, an expressive industrial real-time language. We define two formal semantics for PSYC: a native big-step semantics preserving the logical durations of time intervals defined by structural operational rules and a synchronous small-step semantics defined by translation to a Synchronous-Reactive language expanding time interval durations to a succession of atomic transitions. We show that the two semantics definitions are equivalent. This formalization of the PSYC semantics enables us to define a formal verification methodology for PSYC based on symbolic model-checking. To reduce the state space during model-checking, we also define an optimization technique inspired by timed automata model-checking. Finally, we show how to encode high-level timing requirements into a clock constraint specification language -CCSL -which are then translated to synchronous observers.

  Introduction 1.1 General context . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.3 Thesis Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.4 Publications and Communications . . . . . . . . . . . . . . . . . 4

  Figure 2.1 -Software class

Figure 2 . 2 -

 22 Figure 2.2 -Logical time application design methodology

Figure 2 . 3 -

 23 Figure 2.3 -DO-178 Software Process

Figure 3 . 1 -

 31 Figure 3.1 -Task model for real-time scheduling

Figure 3 . 2 -

 32 Figure 3.2 -Typical execution of a synchronous-reactive program in logical and physical time

CHAPTER 3 -

 3 Languages and Models for Real-Time Systems module ABRO: input A, B, R; output O; loop [ await A || await B ]; emit O each R end module Listing 3.1 -ESTEREL ABRO example Dataflow approach: LUSTRE, SIGNAL

Figure 3 . 4 -

 34 Figure 3.4 -Typical execution of a logical execution time program in logical and physical time

CHAPTER

Figure 3 . 5 -

 35 Figure 3.5 -Comparative of some languages based on logical time

CHAPTER 3 -Figure 3 . 6 -

 336 Figure 3.6 -LTL and CTL property examples

  As a tiny illustration, consider the following set of constraints:b ⊂ a, c ⊂ a, b # c, b ≺ c, c ≺ b $ 1.The expression $ n is a delay expression; it specifies that a clock is delayed with itself by n ticks. The chronogram in Figure3.7 shows a possible execution of clocks a, b and c that fulfill all CCSL constraints. Graphically, red dashed lines denote simultaneity and blue arrows denote strict causality. In a more realistic system, this example can typically represent a requirement specifying a communication pattern between a producer (clock b) and a consumer (clock c) based on a common clock (clock a).

Figure 3 . 7 -

 37 Figure 3.7 -Chronogram of a possible scheduling of the CCSL example

CHAPTER 4 -

 4 Synchronous Logical Execution Time in PSYC

Figure 4 .

 4 Figure 4.1 -PSYC toolchain overview

Definition 4 . 2 . 3 (

 423 Visibility Principle). Let's consider the elementary action of some producer (d w esd , d w ddl ) and the elementary action of some consumer (d r esd , d r ddl ) -An output produced by the producer task defines a visibility date such that d visibility ≥ d w ddl ; -An input can only by consulted by the consumer if its visibility date satisfies d visibility ≤ d r ddl Hence, LET corresponds to the particular case in which d visibility = d w ddl and should then satisfy d w ddl ≤ d r esd

Listing 4 . 2 -

 42 PSYC clock declarationwhere <period> ∈ N * and <offset> ∈ N.

Figure 4 .Figure 4 . 3 -

 443 Figure 4.3 illustrates the use of several clocks taken from a classical example using multiple source clocks, the control of an automotive powertrain. Two independent time bases are defined: one representing the angular position of the crankshaft via intermediate cranks, and the other representing a time coming from a hardware timer. These two time bases are defined with two source clocks, respectively, tooth and realtime:

Figure 4 .

 4 Figure 4.4 shows on the left side the implementation in which only one LED is blinking whereas it shows on the right side the implementation with two different LED, red and green, driven by some mode condition, with different frequency (and duty cycle) requirements.

Figure 4 . 5 -

 45 Figure 4.5 -Guidage, Navigation and Control (GNC)

Figure 4 .

 4 Figure 4.6 -Logging subsystem

51 52CHAPTER 5 -

 515 Formal Semantics of PSYC application ::= decl+ decl ::= clock | source | agent | temporal source ::= source c clock ::= clock c 1 = n 1 * c 2 + n 2 temporal ::= temporal id = v with c agent ::= agent id (starttime n with c) body+, n ∈ N body ::= body id stmt stmt ::

  [[ 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.

-

  next b statement changes the value of the target body instantaneously E, T, b 1 next b 2 ---→ E, T, b 2 nothing (next) -jump b statement changes the value of 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 AbortBody()

Definition 5 . 2 . 2 (

 522 Logical Duration). Considering a date d 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) -dWe consider below an other version of the Duration function based on the (finite) clock state d c defined in section 5.2.1.2 instead of an absolute source date d. 5.2 -Native "big-step" Semantics of PSYC 57 Definition 5.2.3 (Finite State Logical Duration). Duration (n, c, d c ) = n × Π(c) -d c Proposition 5.2.1. Let d c (d) = (d -Φ(c)) mod Π(c), then Duration(n, c, d) = Duration (n, c, d c ) Proof.

2 .

 2 Intermediate states, which corresponds to intermediate states in an sLET interval, typically resulting from the overlapping of the global state of another agent. Futhermore, multiple agent transitions might have different durations based on different sources. There are two main cases: -PSYC clocks rely on multiple source clocks and thus have a partial ordering due to external non-determinism. 5.2 -Native "big-step" Semantics of PSYC 59 -PSYC clocks rely on a unique source clock and thus have a total ordering allowing direct comparison of the agent intermediate states.

  (a) Case 1: synchronized elementary actions (b) Case 2: both agent starts simultaneously, but the elementary action of the blue agent terminate after the red one (c) Case 3: the elementary action of the red agent starts and terminates during the elementary action of the blue agent (d) Case 4: the elementary action of the red agent starts during the elementary action of the blue agent, but both terminate simultaneously (e) Case 5: the elementary action of the blue agent starts during the elementary action of the red agent, but terminate before

Figure 5 . 2 -

 52 Figure 5.2 -sLET Composition patterns

  input c1, c2, ..., cJ ; --inputs input temporal_in1 : T _IN1[DEP T H1]; input temporal_in2 : T _IN2[DEP T H2]; ... input temporal_inM : T _INM [DEP T HM ]; --outputs output temporal_out1 : T _OU T1; output temporal_out2 : T _OU T2; ... output temporal_outN : T _OU TN ; end interface Listing 5.5 -Esterel interface of PSYC agentThe main ideas of the agent translation are the following:

Theorem 5 .

 5 4.1. Forall PSYC agent p ag and the ESTEREL translation T (p ag ) 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:

Figure 5 . 3 -

 53 Figure 5.3 -The GNC functional architecture

  Figure 5.5 -Task GNC

Definition 6 . 2 . 3 (

 623 CCSL Schedule). The schedule of a set of clock C is a function σ ∈ N → 2 C in which σ(s) denotes the set of clocks that tick at step s. It is valid if for a given specification C, Cons it satisfies all the constraints ∀cons ∈ Cons, σ |= cons.

Figure 6 . 1 -

 61 Figure 6.1 -Abstract syntax of CCSL

Figure 6 . 2 -

 62 Figure 6.2 -Synchronous Observer approach using CCSL [And10]

Figure 6 . 3 -

 63 Figure 6.3 -Chronogram of GNC illustrating the end-to-end latency requirement

Figure 7 . 1 -

 71 Figure 7.1 -The leftmost circuit models the interface of a ESTEREL statement while the rightmost circuit models the interface of an equivalent PSYC statement.

Figure 7 .

 7 1. The left pins are basically inputs while the right pins are outputs. Additionnally, The top part correspond to input and outputs signals/environment interactions. The meaning of the pins is the following: -the Go pin starts a statement; -the Res pin resumes the execution of a statement; -the Susp pin suspends the execution of a statement; -the Kill pin unset the registers of the statement due to the exit of a trap statement; -the Sel pin indicates if an internal register is set; 7.1 -Background 91 -the Term, Stop, and Trap(s) pins are used as completion code (originally K0-2) of the statement. It means that the statement has respectively terminated, stopped due to a pause statement or exited from a trap.

7. 2 - 7 . 2

 272 Translating PSYC to Symbolic Transition Systems 93 Translating PSYC to Symbolic Transition Systems

Figure 7 . 2 -FalseFigure 7 . 3 -

 7273 Figure 7.2 -Circuit modeling of basic statements

Figure 7 .

 7 3 shows the translation of an advance 1 with c statement. The behavior is the one from the synchronous semantics:

cnt := cnt - 1 Figure 7 . 4 -

 174 Figure 7.4 -Circuit of the advance n with c statement of PSYC

Figure 7 . 5 -

 75 Figure 7.5 -Circuit of the sequence statement of PSYC

Figure 7 . 6 -

 76 Figure 7.6 -Circuit of the if statement of PSYC

Figure 7 . 7 -

 77 Figure 7.7 -Circuit of the while statement of PSYC

Figure 7 . 8 -

 78 Figure 7.8 -Circuit of the agent declaration of PSYC

Figure 7 . 9 -

 79 Figure 7.9 -Translation of a PSYC agent example. The leftmost listing shows the PSYC code of the agent while the rightmost figure shows its abstracted synchronous translation using the ESTEREL language

Figure 7 .

 7 Figure 7.10 -Circuit translation of the agent from Figure 7.9. Go is used to launch the agent; it is true on the first instant then always false. Mode can be used as a nondeterministic input to model the branch condition. GNC_consult and GNC_display are the signals used for verification.

Figure 7 .

 7 Figure 7.11 -Metrics of the considered use-cases. R denotes the number of repetition requirements, C the number of causality requirements, L the number of latency requirements and S the number of synchronization requirements.

102CHAPTER 7 -Figure 7 .

 77 Figure 7.12 -Verification results

Figure 8 . 1 -

 81 Figure 8.1 -Optimized circuit of the advance n with c statement of PSYC

Figure 8 . 2 -

 82 Figure 8.2 -Temporal optimization architecture

Figure 8 . 3 -

 83 Figure 8.3 -The Landing Gear System (LGS) functional architecture

Figure 8 . 4 -

 84 Figure 8.4 -The leftmost plot and the rightmost plot show the verification time for respectively nuXmv and Prover PSL. Absent values denote timeout (2h).

  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115 9.2 Perspectives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116

I

  data[v ← [[ exp ]] data ] await immediate n -1s, data if s ∈ I ∧ n > 1 await immediate ns, data O 1 -----I await immediate ns, data if s / ∈ I await immediate 1s, data O 0 -----I nothing, data if s ∈ I if exp then p else q end, data O 0 -----I p, data if [[ exp ]] data if exp then p else q end, data O 0 -----I q, data if ¬[[ exp ]] data while exp do p end, data O 0 -----I s ; while exp do s end, data if [[ exp ]] data while exp do p end, data O 0 -----I nothing, data if ¬[[ exp ]] data p ;

  a w a i t i m m e d i a t e c l k _ i n ; a w a i t [ O f f s e t mod P e r i o d ] c l k _ i n ; l o o p e m i t c l k _ o u t ; each P e r i o d c l k _ i n ;

  Period clk_out absolute = Period clk_out relative × Period clk_in absolute Offset clk_out absolute = Offset clk_in absolute + (Offset clk_out relative × Period clk_in absolute )

Theorem D. 1 .

 1 For each agent PSYC p ag and its ESTEREL translation T (p ag ), and for any transition of the form:C p ag = == ⇒ n×s C p agAssuming, C ≈ data and s ∈ E, we have an equivalent sequence of ESTEREL transitions:T (p ag ), data E -----P 1 , data 1 . . . E -----P n , data n with T (p ag ) = P n et C ≈ data n Proof.By induction on the structure of the native semantics rule = == ⇒:-Case skip: Trivially equivalent to the ESTEREL rule (considering n = 0) ESTEREL transition.

  Those clocks are typically node Abro(A, B, R : bool);

	returns (O : bool);
	var seenA, seenB : bool;
	let
	O = Edge(seenA and seenB);
	seenA = Hold(A, R);
	seenB = Hold(B, R);
	tel
			Listing 3.3 -LUSTRE ABRO example
	A	False	True	False False False False	True	False
	B	False False False False False	True	False False
	R	False False False	True	False False False False
	seenA	False	True	True	False False False	True	True
	seenB	False False False False False	True	True	True
	pre(seenA)	nil	False	True	True	False False False	True
	pre(seenB)	nil	False False False False False	True	True
	O	False False False False False False	True	False
	Figure 3.3 -Possible execution of the ABRO example in LUSTRE

main reactor(period:time(10 ms

	reactor Sensor(period:time(10 ms)) {
	output out:int;
	timer t(0, period);
	reaction(t) -> out {=
	...
	=}
	}
	reactor Task1 {
	input in:int;
	output out:int;
	reaction(in) -> out {=
	...
	=}
	}
	...
	)) {
	/ * we omit instantiation part * /
	sensor.in -> task1.in;
	task1.out -> task2.in;
	task2.out -> actuator.out;
	}
	Listing 3.5 -LINGUA FRANCA pipeline example

  3 -Languages and Models for Real-Time Systems

	clock c100ms = 100 * ms;
	clock c1s = 1000 * ms;
	agent Filter(starttime 1 with c1s) {
	consult raw_data, mode / * inputs * /;
	display filtered_data / * outputs * /;
	body start {
	if (mode == FILTER) {
	filtered_data = Filter(raw_data);
	advance 3 with c100ms;
	}
	advance 1 with c1s;
	}
	}
	Listing 3.7 -PSYC filter example

  Inter-task communication channels . . . . . . . . . . . . . 43 4.3.3.1 Temporal Variables . . . . . . . . . . . . . . . . 43 4.3.3.2 Illustration: control system . . . . . . . . . . . . 46 4.3.3.3 Streams . . . . . . . . . . . . . . . . . . . . . . 46 4.3.3.4 Illustration: logging . . . . . . . . . . . . . . . . 48 4.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48

	4.1 The ASTERIOS Software Suite . . . . . . . . . . . . . . . . . . . 34
	4.1.1 Origins of the technology . . . . . . . . . . . . . . . . . . . 34
	4.1.2 Industrial context . . . . . . . . . . . . . . . . . . . . . . . 34
	4.1.3 Tooling . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
	4.2 A synchronous generalization of Logical Execution Time . . . . 35
	4.2.1 Overview of synchronous Logical Execution Time . . . . . 36
	4.2.2 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . 36
	4.2.

3 About functional and temporal determinism . . . . . . . . . 38 4.3 The PSYC language . . . . . . . . . . . . . . . . . . . . . . . . . 38 4.3.1 Source and clocks . . . . . . . . . . . . . . . . . . . . . . 38 4.3.1.1 Source clocks . . . . . . . . . . . . . . . . . . . 39 4.3.1.2 Periodic clocks . . . . . . . . . . . . . . . . . . . 39 4.3.1.3 Illustration: source and clocks . . . . . . . . . . . 39 4.3.2 Tasks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 4.3.2.1 Elementary Actions . . . . . . . . . . . . . . . . 40 4.3.2.2 Body . . . . . . . . . . . . . . . . . . . . . . . . 41 4.3.2.3 Agents . . . . . . . . . . . . . . . . . . . . . . . 42 4.3.2.4 Illustration: LED blinking . . . . . . . . . . . . . 42 4.3.3

  Body is a dedicated syntaxical construction to PSYC allowing the definition of structures similar to state machines inside tasks. By default, a body is only a named scope containing a C-like compound statement acting as an infinite loop. It is defined as following:

	f(); advance n1 with c1; g(); advance n2 with c2;
	Listing 4.5 -PSYC advance statement example
	4.3.2.2 Body
	body <name> {
	<PsyC-statements>+
	}
	Listing 4.6 -PSYC body declaration
	Where PSYC statements can be any C statement in addition with dedicated PSYC statements such
	as advance.

  Listing 4.20 -PSYC agent pushto declarationThen, sending data to a stream is done by the push statement. Contrary to a temporal variable, multiple values can be pushed inside during an elementary action. Syntaxically, it is defined as follows:

	source realtime;
	clock c_base = realtime;
	stream float s with expiration 10 * clockperiod(c_base);	1 agent Logger(starttime 1 with c_base) 2 { 3 popfrom s;
	agent A(starttime 1 with c_base) { pushto s; body start { / * ... * /; push(s, data); advance 1 with c_base;	4 5 6 7 8 9 10 }	body start { while [10] (count(s) > 0) { log(pop(s)); } advance 10 with c_base; }
	}		Listing (4.25) Logger Task
	}
	Listing (4.24) A Task
	agent Producer(/ * ... * /) {
	pushto <stream_name>;
	/ * ... * /
	}
	agent Consumer(/ * ... * /) {
	popfrom <stream_name>;
	/ * ... * /
	}
	Listing 4.22 -PSYC agent popfrom declaration
	Then, poping from a stream is done using the pop statement which returns the oldest unpopped
	data from the queue.
	/ * ... * / = pop(<stream_name>);
	Listing 4.23 -PSYC stream pop statement

push(<stream_name>, <new_value>); Listing 4.21 -PSYC stream push statement From the consumer's side, the agent also has to specify the stream it is going to pop from. Syntaxically, it is defined as follows:

PSYC has also a statement called count(<stream_name>) which returns the number of available elements in a stream. It is used to avoid popping from an empty stream.

  Temporal variables A temporal variable is modeled by a sampling component that fetches the corresponding signal displayed by the producer agent on each tick of the temporal clock and emits a sampled signal to consumer agents. The history of the temporal variable is modeled by additional sampling components that propagate previous values on each clock tick.Let's consider first the module below that implements a basic sampler.From this sampler module, we define the temporal module as N concurrent instances of the sampler to model a temporal variable with history of size N as shown below.

	module Temporal;
	generic constant N: unsigned;
	type T;
	input C;
	input Temporal_In: T;
	output Temporal: T[N];
	[
		run Sampler[signal Temporal_Input/In, Temporal[0]/Out,C/Clk] ||
		run Sampler[signal pre(?Temporal[0])/In, Temporal[1]/Out, C/Clk] ||
		run Sampler[signal pre(?Temporal[1])/In, Temporal[2]/Out, C/Clk] ||
		module Clock; ...
		--input clock run Sampler[signal pre(?Temporal[N -2]/In, Temporal[N -1]/Out, C/Clk)]
	]	input clk_in;
	--output clock end module
		output clk_out;
		--constants
		constant Period, Offset : integer;
		await immediate clk_in;
		await [Offset mod Period] clk_in;
		loop
		emit clk_out;
		each Period clk_in;
		end module
		Listing 5.2 -Esterel translation rule of PSYC clock
		module Sampler;
		type T;
		input In : T; output Out : T;
		loop
		emit Out(?In);
		pause;
		sustain Out(pre(?Out));
		each C
		end module
		Listing 5.3 -Esterel sampler module

end switch end trap end loop end var end module Listing

  5.6 -Esterel translation rule of PSYC agentNote that each displayed temporal variables have copy in private variables. They correspond to the update of the temporal variables inside an agent. Body state is also handled by a dedicated variable body_target. 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. exp, is translated by the ESTEREL assignment statement to the private variable corresponding to the selected temporal variable as shown below.

	body_target := body_b; exit body_exit;
	Listing 5.13 -Esterel translation rule of PSYC jump statement
	private_temporal_outx := T (exp)
	PSYC sequence statement is translated by the equivalent ESTEREL sequence statement as shown Listing 5.8 -Esterel translation rule of PSYC assignment statement to temporal variable below.
	type Agt_ID_bodies = PSYC assignation of variable x, x := exp, is translated by the equivalent ESTEREL assignment statement to the variable as shown below. T (stmt1); T (stmt2)
	enum {BODY _BST ART , BODY _B1, ..., BODY _BK }; Listing 5.14 -Esterel translation rule of PSYC sequence statement
	module Agent_ID:
	extends Agent_ID_Intf; PSYC condition statement, if (exp) stmt1 else stmt2 is translated by the equivalent ESTEREL
	--starttime condition statement as shown below.
	await STARTTIME_VALUE STARTTIME_CLOCK;
	if T (exp) then
	T (stmt1)
	else
	T (stmt2)
	end if
	await n c;
	emit temporalvar1(privatetemporalvar1);
	emit temporalvar2(privatetemporalvar2);
	...
	emit temporalvarN (privatetemporalvarN );
	exit body_exit;
	Expressions and Statements PSYC nothing is translated the equivalent ESTEREL statement as Listing 5.12 -Esterel translation rule of PSYC endbody statement
	shown below.
	PSYC statement jump, jump b, is translated by a target body assignment followed by an exit
	statement as shown below.

--body handling var body_target : Agt_ID_bodies := BODY _BST ART , private_temporal_out1 : T _OU T1 := init , private_temporal_out2 : T _OU T2 := init , ... private_temporal_outM : T _OU TN := init in loop trap body_exit in switch case body_target = BODY _BST ART do T (bstart) case body_target = BODY _B1 do T (b1) ... case body_target = BODY _BK do T (b k ) nothing Listing 5.7 -Esterel translation rule of PSYC nothing statement PSYC assignation of temporal variable x, x := var_x := T (exp) Listing 5.9 -Esterel translation rule of PSYC assignment statement to private variable PSYC statement advance, of the form advance n with c, and assuming that var1, var2 . . . varN are all the output temporal variables of the agent is translated by an ESTEREL await statement followed (logically instantaneously) by an emit statement for each output temporal variable as shown below. Listing 5.10 -Esterel translation rule of PSYC advance statement PSYC statement next, next b, is translated by an assignment to the target body as shown below. body_target := body_b; Listing 5.11 -Esterel translation rule of PSYC next statement PSYC statement, endbody, is translated by an ESTEREL exit statement as shown below. It jumps to the agent parent scope, which then dispatch the control to the corresponding body.

  Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88 6.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88

6.1 Temporal requirements for PSYC . . . . . . . . . . . . . . . . . 80 6.2 The CCSL language . . . . . . . . . . . . . . . . . . . . . . . . . 81 6.2.1 Time model . . . . . . . . . . . . . . . . . . . . . . . . . . 81 6.2.2 Constraints and Expressions . . . . . . . . . . . . . . . . . 82 6.2.3 Synchronous observers . . . . . . . . . . . . . . . . . . . . 84 6.3 Encoding requirements in CCSL . . . . . . . . . . . . . . . . . . 84 6.3.1 Repetition requirement . . . . . . . . . . . . . . . . . . . . 85 6.3.2 Synchronization requirements . . . . . . . . . . . . . . . . 85 6.3.3 Causality requirements . . . . . . . . . . . . . . . . . . . . 86 6.3.4 Delay and Latency requirements . . . . . . . . . . . . . . . 86 6.3.5 Functional chains . . . . . . . . . . . . . . . . . . . . . . . 87 6.4

  7.1 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90 7.1.1 Circuit semantics of Esterel . . . . . . . . . . . . . . . . . 90 7.1.2 Symbolic Transition System . . . . . . . . . . . . . . . . . 91 7.1.3 Symbolic Model-checking . . . . . . . . . . . . . . . . . . 92 7.2 Translating PSYC to Symbolic Transition Systems . . . . . . . . 93 7.2.1 Extending PSYC agents with verification signals . . . . . . 93 7.2.2 Translation principle . . . . . . . . . . . . . . . . . . . . . 93 7.2.3 Sources and clocks . . . . . . . . . . . . . . . . . . . . . . 94 7.2.4 Statements . . . . . . . . . . . . . . . . . . . . . . . . . . 94 7.2.5 Agents . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 7.2.6 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . 98 7.3 Experiments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99 7.3.1 Implementation . . . . . . . . . . . . . . . . . . . . . . . . 100 7.3.2 Benchmarks . . . . . . . . . . . . . . . . . . . . . . . . . . 100 7.3.3 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . 101 7.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103

  Definition 7.1.2 (STS Reachability). Let's consider a program M, M Init, M T rans and a property P, P Init, P T rans . A bad state is never reachable if and only if ∀n ∈ N * Init 0 ∧ T rans 1 ∧ T rans 2 ∧ ... ∧ T rans n |= OK n

	where:

  8.1 Problem statement . . . . . . . . . . . . . . . . . . . . . . . . . . 105 8.2 A temporal optimization approach . . . . . . . . . . . . . . . . . 107 8.2.1 Symbolic Transition System with durations . . . . . . . . . 107 8.2.2 Symbolic abstraction of durations . . . . . . . . . . . . . . 108 8.3 Experiments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108 8.3.1 Back to GNC task . . . . . . . . . . . . . . . . . . . . . . 108 8.3.2 The Landing Gear System use-case . . . . . . . . . . . . . 110 8.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111

  table below shows state space variations of task GN C -without mode handling -considering different choice of task period.

	106		CHAPTER 8 -Verification: Mono-Source Case
	GNC period 1 s 10 s 100 s 1000 s
	#State vars	37	37	37	37
	#States	42 402 4002 40002
	Diameter	20 200 2000 20000

  We show now the STS of the scheduler for a list of agent ag 1 , ag 2 , . . . , ag n : {∆, duration 1 , duration 2 , . . . duration n , state 1 , state 2 , . . . state n , clock 1 , clock 2 , . . . clock n

	8.3 -Experiments	109
	V =
	8.3 Experiments
	8.3.1 Back to GNC task

  table below. Hence, this methodology works in terms of state space size.

	Source period 100 ms 10 ms 1 ms 100 us
	#State vars	43	43	43	43
	#States	4	4	4	4
	Diameter	4	4	4	4

Résumé

  Les systèmes temps-réel critiques doivent respecter des contraintes temporelles strictes qui doivent être considérées tout au long du cycle logiciel. Cependant, du fait que les temps d'exécution exacts ne sont généralement pas connus lors de la conception, le temps logique fournit un moyen d'abstraire les contraintes temporelles et les exécutions du temps physique, dépendant de la plateforme. Dans cette thèse, nous nous concentrons sur deux formalismes basés sur le temps logique. L'approche Synchrone-Réactive abstrait totalement le temps physique en utilisant des bases de temps discrète sur lesquelles les calculs sont déclenchés. L'approche de Temps d'Exécution Logique utilise des bases de temps logique pour représenter non seulement les instants de déclenchement, mais aussi les durées des calculs élémentaires. Dans notre travail, nous commençons par définir une unification des approches Synchrone-Réactives et de Temps d'Exécution Logique, fournissant un cadre formel naturel pour définir la sémantique de PSYC, un langage temps-réel industriel expressif. Nous définissons deux sémantiques pour celui-ci : une sémantique native à grands pas, préservant les durées logiques des intervalles de temps, définie par des règles structurelles opérationnelles ; et une sémantique synchrone à petits pas définie par traduction vers un langage Synchrone-Réactif étendant les durées des intervalles de temps à une succession de transitions atomiques. Nous montrons que les deux sémantiques sont équivalentes. Cette formalisation de la sémantique de PSYC nous permet de définir une méthodologie de vérification formelle pour PSYC basée sur du model-checking symbolique. Pour réduire l'espace d'état pendant le model checking, nous définissons une technique d'optimisation inspirée du model-checking temporisé. Enfin, nous spécifions les exigences temporelles que nous voulons vérifier via un langage de spécification de contrainte d'horloge -CCSLqui sont ensuite traduites en observateurs synchrones.

Mots-clés : Systèmes Temps-Réel, Temps d'Exécution Logique, Langages Synchrone-Réactifs, Vérification Formelle.

Remerciements

CHAPTER 5

Formal Semantics of PSYC

temporal <type> <variable_name> with <clock>; Listing 4.12 -PSYC temporal variable declaration Where <clock> corresponds to the sampling clock.

From the producer side, the agent has to declare the temporal variables that it is going to write on. It is defined as following: Listing 4.14 -PSYC temporal variable assignment statement From the consumer's side, the agent has also to specify the temporal variables that it is going to read from as well as the number of past samples to read with respect to the temporal variable's clock. Syntaxically, it is defined as following:

Equivalence Criterion Proof

In this appendix, we demonstrate the equivalence between both semantics, namely native (i.e. bigstep) and synchronous (i.e. small-step). We show the proof only for a subpart of the syntax for various reasons: firstly, it makes the proof simpler with less technical details; secondly, it allows to focus on the important part which is actually what should be retained from this criteria and could be applied to other languages.

A Syntax

We show in this section the simplified syntax for both PSYC and ESTEREL.

p, q ::= nothing 1, the grammars are highly simplified; only the part used in the translation scheme is kept. In this PSYC syntax, we don't show the body/endbody mechanism to avoid the trap/exit ESTEREL statements in the proof. However, body without endbody can be rewritten using an next_body variable and a global if statement to start the correct body accordingly as shown below.

B ESTEREL Semantics

In this section, we give the ESTEREL semantics rules of the subset that we consider. Let's first recall the definition of the semantics transition rule. Definition B.1 (Esterel semantics). Given a constructive ESTEREL program P and a set of data, the semantics of its transition is given by the following relation:

P, data

Eo k ------

where E i and E o are respectively the input and output signal set active on the current reaction, and k, a boolean denoting the termination status (i.e., if it takes time or not) Then, we give the main semantics rules of ESTEREL. The rules are given with a structure very similar to the ones from PSYC to ease the proof procedure.