Hamza Bourbouh

Pierre-Loïc Garoche

Thomas Loquen

Eric Noulard

Claire Pagetti

CoCoSim, a code generation framework for control/command applications

We present CoCoSim, a framework to support the design, code generation and analysis of discrete dataflow model expressed in Simulink. In this work, we specifically focus on the analysis and code generation of multi-periodic systems. For that CoCoSim provides two complementary approaches: the first amounts to encode the multiperiodic semantics in a pure-synchronous one -à la Lustre-, enabling the use of model checker for verifying properties. The second provides a faithful code generation into multiple communicating (mono)synchronous components -à la Preludethat can be then simulated or embedded in the final platform with any real-time scheduler. These approaches have been experimented in various settings.

Introduction

Context

Safety-critical systems design requires a thorough development process including formal verification and correct by construction behaviour. In that area, Model-Based Design has been widely used for software development. Such an approach offers the refinement of a system from High Level Requirements down to the embedded code while having an executable model at different stages. Matlab/Simulink 1 from MathWorks, is a de facto model-based design standard in industry, offering verification and code generation means.

Nonetheless, other development frameworks are used in addition in some industries, such as aeronautic, railways or space. Indeed, control/command applications have received a particular attention over the years and several synchronous programming languages such as Esterel [START_REF] Berry | The Esterel synchronous programming language: design, semantics, implementation[END_REF], Lustre 1 https://www.mathworks.com/products/simulink.html [START_REF] Caspi | Lustre: A Declarative Language for Programming Synchronous Systems[END_REF] or Signal [START_REF]Synchronous programming with events and relations: the SIGNAL language and its semantics[END_REF] have been defined to help their design. Scade [START_REF] Colaço | SCADE 6: A formal language for embedded critical software development (invited paper)[END_REF] is an industrial and DO 178C qualified Lustre-based framework that provides strong guarantees and proofs well appreciated, in particular for certification.

Offering frameworks linking Simulink and synchronous approaches is thus appealing. CoCoSim belongs to this category as it is an open source tool that translates Simulink specification in Lustre while preserving semantics and providing many associated traceability or test capabilities. In this paper, we describe an extension of CoCoSim to allow the safe translation and verification from multiperiodic systems to Lustre/Prelude programs.

Contributions

The CoCoSim approach to deal with multiperiodic systems is highlighted in the Fig. 1. First, we need to define precisely the semantics of multi-periodic systems in Simulink and connect it to the one of synchronous programming. In synchronous languages, execution time is neglected while each computation is performed repetitively, e.g., every ts seconds. In Simulink, most discrete subsets of blocks are fitted with a synchronous se-mantics, but the case of multi-periodic systems is more complex and requires an analysis of the internal semantics.

Multi-periodic system in

Once the semantics has been defined, the second contribution is the extension of CoCoSim current Lustre translation in order to encode the multi-periodic communication with classical Lustre over-and sub-sample operators (left hand side of Fig. 1). This amounts to express the whole system on a base clock. This Lustre model is then used to perform formal analysis using SMT-based model-checking. While required to properly analyze the full system, this encoding is not efficient for execution.

Once the verification is valid, the last step is the efficient code generation (right hand side of Fig. 1). Each synchronous component is translated as a Lustre model which will eventually be compiled into C code, while aggregating nodes, mixing different clocks or execution rates are expressed as Prelude programs. Prelude [START_REF] Pagetti | Multi-task Implementation of Multi-periodic Synchronous Programs[END_REF] is a synchronous language that has been defined to program multiperiodic applications. From a Prelude program, the compiler generates a set of classical real-time tasks and many predictable implementations have been proposed for multi-and many-core architectures [START_REF] Puffitsch | Off-line Mapping of Multi-rate Dependent Task Sets to Many-core Platforms[END_REF].

Outline

We start by presenting an overview of CoCoSim framework (Section 2) for mono-periodic discrete Simulink models. We then define the specification of multi-periodic applications with Simulink (Section 3). We detail the multi-periodic extension of CoCoSim (Section 4). Last, Section 5 presents some experiments settings and two detailed use cases.

Overview of mono-periodic CoCoSim

CoCoSim is a highly automated framework for verification and code generation of Simulink/Stateflow models. It consists of an open architecture, allowing the integration of different analyses. CoCoSim is structured as a compiler, sequencing a series of translation steps leading, eventually to either the production of source code, or to the call to a verification tool. By design, each phase is highly parametrizable through an API and could then be used for different purposes depending on the customization. The Figure 2 outlines the different steps. CoCoSim starts first by simplifying some complex blocks into a set of basic blocks. Then an internal representation of the model is generated containing all information needed for code generation. Based on the work of Caspi et al. [START_REF] Caspi | Translating Discrete-Time Simulink to Lustre[END_REF], Gene-Auto [START_REF] Rugina | Gene-Auto: Automatic Software Code Generation for Real-Time Embedded Systems[END_REF][START_REF] Toom | Gene-Auto: an Automatic Code Generator for a safe subset of Simulink/Stateflow and Scicos[END_REF] CoCoSim is customizable and configurable. Indeed, it supports most of frequently used Simulink blocks libraries (around 100 blocks) and new blocks can be easily supported.

Supported analyses

Once a formal representation of Simulink model is generated, CoCoSim is connected to a set of external tools to provide code generation, formal verification or test case generation. The toolchain is highly automated as all the steps of verification or code generation are automated.

The goal of the CoCoSim framework is to ease the application of formal methods and analysis of Simulink-based systems. The external tools are introduced and linked to the platform in a very generic way. While CoCoSim is built mainly around a specified set of tools, additional ones can be easily locally linked or even distributed as extensions. A set of Matlab functions libraries are pro-vided by CoCoSim to ease the integration of tools analysis results. Eg. displaying the counterexample at the Simulink level, importing test harness as a Signal builder or create a new test-harness model, generating HTML reports or other helpful support functions.

All CoCoSim analyses are performed on the compiled artifact and the results are expressed back at Simulink level thanks to traceability information. We sketch here the features of the connected tools. At the current moment all tools are opensource and freely available. It scales well with large models, therefore various verification techniques and compositional reasoning can be used.

Formal Verification: SMT-based model checking

Once requirements have been expressed using Co-CoSim library and attached to the Simulink model, different tools can perform SMT-based model checking and check their validity. In case the property supplied is falsified, CoCoSim provides means to simulate the counterexample trace in the Simulink environment. Currently, CoCoSim is connected to three verifiers. First, Kind2 [START_REF] Champion | The Kind 2 Model Checker[END_REF] is a powerful tool that implement multiple algorithms including k-induction [START_REF] Sheeran | Checking Safety Properties Using Induction and a SAT-Solver[END_REF] and IC3/PDR [START_REF] Bradley | IC3 and beyond: Incremental, Inductive Verification[END_REF] as well as on-the-fly invariant generation. All of these can be performed with various SMT solvers: CVC4, Z3, Yices.

Second, Zustre [START_REF] Garoche | Zustre[END_REF] relies on the LustreC [20] modular compiler. The input Lustre model is compiled in a Horn encoding [START_REF] Garoche | Hierarchical State Machines as Modular Horn Clauses[END_REF][START_REF] Garoche | Synthesizing Modular Invariants for Synchronous Code[END_REF] describing the transition relation. The hierarchy of the input model is preserved: each Lustre is associated to a local Horn description of the computation. This transition system along with a similar expression of its requirements is analyzed with Spacer [START_REF] Komuravelli | SMT-based model checking for recursive programs[END_REF][START_REF] Komuravelli | Automatic Abstraction in SMT-Based Unbounded Software Model Checking[END_REF], a PDR algorithm integrated in Z3. Thanks to the modular encoding at Horn level and to Spacer, a valid property will produce witnesses as node-local invariants. These invariants are expressed in the feedback to CoCoSim and can be re-introduced in the original Simulink model as fresh annotations.

Third, JKind [START_REF] Gacek | The JKind Model Checker[END_REF], a similar model checker, developed at Rockwell Collins, is also integrated.

Code generation:

Some of CoCoSim backends provide code generation. Eg. LustreC [START_REF] Garoche | LustreC[END_REF] is an implementation of the modular compilation scheme [START_REF] Biernacki | Clock-directed modular code generation for synchronous data-flow languages[END_REF] used in Scade. It preserves the hierarchy of the initial model, easing the checking of traceability between Lustre and generated C code. LustreC targets mainly C code but extends the general compilation of Lustre to CoCoSpec [START_REF] Champion | CoCoSpec: A Mode-Aware Contract Language for Reactive Systems[END_REF][START_REF] Davy | Ensuring functional correctness of cyber-physical system controllers: from model to code analyses[END_REF]. LustreC also provides modular compilation with multiple source files, call to external C libraries or externally defined C functions.

Kind2 [START_REF] Champion | The Kind 2 Model Checker[END_REF] is, first of all, a model checker but it is capable of producing Rust code from the provided models.

Test cases generation:

LustreT [START_REF] Garoche | Testing-Based Compiler Validation for Synchronous Languages[END_REF] is based on some compilation stages of LustreC [START_REF] Garoche | LustreC[END_REF]. It provides two different methods to perform test case generation [START_REF] Garoche | Testing-Based Compiler Validation for Synchronous Languages[END_REF].

In the first case a coverage criteria such as MC-DC is expressed as a reachability problem. For example, an atom of a boolean predicate has to be true at some point. Then we check the validity of the negation of that property. Model checker such as Kind2 or Zustre will then perform bounded-model checking or, possibly, exhibit a counter-example; that is, a test case activating that specific criteria. A MC-DC criteria will then be mapped to a large set of such predicates. The test generation process will populate a set of test cases activating each of these conditions.

The second approach relies on the notion of mutants. Usually, mutants are used to evaluate the quality of a test suite. We generate a set of mutant programs and apply different test suites. A good test suite distinguishes valid program from mutants. Here the approach is different. After generating mutants, we use the same bounded-model checking tools to build a test case that will distinguish them. This does not always succeed since some mutations may be invisible, or in dead code. But considering the large set of mutants, this approach is efficient at building test cases.

3 Multi-periodic in Simulink

Reminder on Simulink

Simulink is a graphical, dataflow programming environment for modeling and simulating dynamical systems. Roughly speaking, in a Simulink model, the user can use blocks, signals and annotations. Each Simulink block implements a given mathematical function or a stateful system specification and has a specific number of inputs and outputs connected with other blocks using Simulink signals. These blocks are either basic blocks from Simulink library (e.g., Sum, UnitDelay, Gain) or a grouping of several blocks into a Subsystem block. Simulink diagrams are hierarchical and graphically organized using Subsystems. There are two types of Subsystems, Virtual Subsystem that is flatten during Simulation and only used to organize the model at design time and Atomic Subsystem that is executed as an atomic unit in the final code.

A discrete Simulink model runs on a fixed time step defined with a period π and initial offset θ. A Simulink model can be mono-periodic where all blocks runs with the same period, or multi-periodic where blocks can run on different periods. A block is executed and its outputs are updated only when certain execution conditions are satisfied. If these conditions are not met, the block is not executed and its output signals hold their values. Matlab/Simulink defines three types of execution conditions and block:

• Unconditional blocks or subsystems: The block is set with a sample time D = (π i , θ i ) with period π i and initial offset θ i and it is updated only at times kπ i + θ i for k ∈ N, whereas, it remains constant during the intervals

[kπ i + θ i , (k + 1)π i + θ i ).
• Conditionally executed subsystems: such as enabled/triggered subsystems, are subsystems that are conditionally executable when a certain guard condition over certain variables, called control-inputs, holds. Furthermore, the data of the system-block may be reset when the guard condition holds, and the outputs may be reset when the guard condition is violated.

• Logically-executed subsystems: the subsystem is executed one or more times at the current time step when it is enabled by a signal from a control block. An example of logicallyexecuted subsystems are if Action Subsystem, Switch Case Action Subsystem and For Each Subsystem.

Multi-periodic blocks

From now on, we only consider unconditional blocks and systems. The output of the model is incremented by In1 every 2 seconds because of the UnitDelay block updates its outputs every two seconds and because Sum is a stateless block that adds its inputs values at the same time step. The behaviour can be represented as:

t 0 1 2 3 4 5 In1 1 1 1 1 1 1 Out1 0 0 1 1 2 2
Since UnitDelay block is running on a different period than the Sum block, an implicit data transfer block (Rate Transition) is introduced by Simulink to ensure all input signals runs on the same period. The user can force Simulink to reject models with unspecified data transfers between different rates. In the case of the Simulink example in Figure 3, we get the following error when we set "Multi-task (or Single task) rate transition" to "error":

The sample time 1 of 'Sum' at input port 2 is different from the sample time 2 of 'Unit Delay' at output port 1.

Explicit clock transition

The model described in Fig. 3 will be rejected by CoCoSim. Instead, the user must specify explicitly the right data transfers block type. In Figure 4 we introduced two Rate Transition blocks to ensure Sum block and UnitDelay block have their inputs running on the same period as the block itself. Thanks to these introduced Rate Transition blocks, the boundaries between blocks that run on different period become explicit and makes the reasoning about clocks to be limited to these data transfers blocks. The Rate Transition block (RTB) has two block parameters that control its execution: Ensure data integrity and Ensure deterministic data transfer. When the first parameter is checked, it ensures data integrity when the block transfers data. A problem of data integrity exists when the input to a block changes during the execution of that block. For instance, a faster block supplies the input to a slower block. In a protected data transfer, the output of the faster block is held until the slower block finishes executing. The second parameter enforces a deterministic data transfer where the timing of the data transfer is completely predictable, as determined by the sample rates of the blocks. The timing of a nondeterministic data transfer depends on the availability of data, the sample rates of the blocks, and the time at which the receiving block begins to execute relative to the driving block.

CoCoSim only allows rate transition blocks that ensure data integrity and determinism. With this restriction, there exist two main types of data transfer:

• ZOH: the Zero-Order-Hold is a deterministic RTB that implements direct communications from fast to slow blocks at harmonic periods. ∃n ∈ N, inTs = outTs/n and inTsOffset = outTsOffset = 0.

• 1/Z: Acts as a unit delay that implements delayed communications from slow to fast block at harmonic periods. ∃n ∈ N, inTs = outTs * n and inTsOffset = outTsOffset = 0.

Common base clock identification

In Simulink, each period π i and offset θ i of a block is defined by a floating point number. In the following, we will encode the semantics of the whole system over a base symbolic clock either using counters (in Lustre) or using rational numbers (in Prelude) to describe the individual local period and offset.

To characterize such common clock, we can express periods and offsets without loss of generality as rational numbers p/q ∈ Q where p ∧ q = 1. Let us consider n unconditional blocks, each associated to the period and offset π

i , θ i ∈ Q. Let π n i , π d i , θ n i , θ d i ∈ N be such that π i = π n i /π d i and θ i = θ n i /θ d i .
We can define the common base clock as π = (π n /π d , 0) where

π d = lcm {π d i , θ d i } i and π n = gcd {π i × π d , θ n i × π d } i .
Let us remark that since π d is defined as the least common multiplier of all denominators of periods and offsets, the terms in the gcd expression of π n are all integers.

Example 1 In Figure 5, In1 is defined on D1 = (1/1s, 0/1s) and UnitDelay, Sum, Out1 on D2 = (2/1s, 0/1s). Thus, the common base clock is D = (1s, 0s) since 1 = lcm(1) and 1 = gcd(1, 2).

We can now express each period π i and offset θ i with respect to the base period, as positive integers, respectively πi = π i ×π and θi = θ i ×π. This gives a symbolic and denumerable characterization of each period and offset as a multiple of the base clock.

Example 2 In Figure 5, D1 is defined as (1, 0) and D2 is defined as (2, 0) relatively to the base clock (1s, 0s).

Multi-periodic CoCoSim

We present here the extension of CoCoSim to address multi-periodic Simulink models. It uses Lustre as an intermediate formal language for verification since many external model checkers take Lustre model as an input (e.g., Kind2, Zustre, Jkind). It relies on Prelude for code generation.

Lustre

Lustre code consists of a set of nodes transforming infinite streams of input flows into streams of output flows. A notion of symbolic abstract universal clock (also referred as the basic clock) is used to model system progress. In Lustre, a node is defined as a set, i. Clocks. Another specific construct is the definition of clocks and clocked expressions. Clocks are defined as enumerated types, the simplest ones being Boolean clocks. Expressions can then be clocked with respect to such clock values: e when c where c is a Boolean clock. In this case, the expression is only defined when variable c is positive. Clocked expressions can be gathered using merge operator: Expressions have to be clocked appropriately. The clocking phase of the compiler allows to check the consistency of clocks definitions and their uses.

Translation in Lustre

The first CoCoSim multi-periodic translation technique [START_REF] Tripakis | Translating discrete-time simulink to lustre[END_REF] produces a pure Lustre specification. The first question is to translate the sample time in Lustre as sub-sampled clock of the common base clock. The idea is to compute the common base clock as explained in section 3.4 and express each couple (period, offset) relatively to it. For the example in Fig. 5, one solution to encode D1 and D2 could be:

D1 = true ; D2 = true → not pre ( D2 ) ;
D1 was exactly equal to the common base clock whereas D2 was twice slower. Then, alternating true and false in the flow D2 will indeed lead to true every two times. However, when the clocks become complex, the intrication of pre will become unsustainable. Instead, we will use some counters and will have a similar approach as the one in Prelude.

D1 = make_clock (1 ,0) ; D2 = make_clock (2 ,0) ;
Where make_clock is a Lustre node that generates a Boolean clock that is true at the logical instants k * period + offset with k ∈ N and false otherwise.

node make_clock ( period , offset : int ) returns ( clk : bool ) var count : int ; let count = (( period -offset ) -> ( pre ( count ) + 1) ) mod period ; clk = ( count = 0) ; tel

The second question is how to combine different sample times. The idea is to bring back a flow on the common base clock and to sub-sample. Let us detail the translation for the two rate transition blocks, ZOH and 1/z, supported by CoCoSim. Let (inTs, inTsOffset) (resp. (outTs, outTsOffset)) be the sample time of RTB input port called RTB_U (resp. output port called RTB_Y) relatively to the common base clock. We thus have:

0 0 0 0 1 1 2 2
Prelude: Y = (0.0 f by Counter) * ˆ2;

0 0 0 0 1 1 2 2
Table 1: Translation to Lustre and Prelude of different settings of block RTB in Fig. 6.

Translation in Prelude

Prelude [START_REF] Pagetti | Multi-task Implementation of Multi-periodic Synchronous Programs[END_REF] is a synchronous language that has been defined to program multi-periodic applications. The language considers imported nodes that can be programmed in C or Lustre. An example is given below where a node Sum has two inputs, one output and a worst case execution time (WCET) of 1 logical time.

imported node Sum ( v1 , v2 : real ) returns ( v : real ) wcet 1;

In the CoCoSim framework, the code generated from Simulink will be composed of Lustre nodes for mono-periodic (sub-) systems and Prelude when several rates are handled. Thus in that case, Lustre nodes are assembled together in a Prelude program, which details the real-time constraints of the system and the semantics of the communications between the Lustre nodes. This assembly is not done directly in Lustre because communications relate nodes executing at different periodic rates and Prelude is better suited to the specification and efficient compilation. The example corresponds to the Fig. 5. The assembly node has one input In1 with a clock (10, 0) meaning that In1 has a period of 10 and an offset of 0. It is up to the user to link the logical clock with the physical one. Since In1 is running at D1=(1s,0s), the logical clock is at 100ms.

The imported node Sum consumes the flows In1 /^2 and 0.0 fby UnitDelay_1_1. Nodes are synchronous, thus the two inputs and the output must have the same clock. As the clock of In1 is (10, 0) by definition, the flow In1/^2 has (20, 0) as clock. The operator ^2 is a deceleration by 2.

The operator *^2 is an acceleration that will divide the period by 2. It is used for the 1/z block as shown in table 1.

Experiments

In this section, we will present two use cases that will be experimented with CoCoSim. The controller is composed of 8 functions (depicted by boxes) that run at different periods and exchange data (depicted by arrows). A series of filters (named X_filter ) consolidate the data measured on the aircraft and two controllers manage the airspeed (va_control ) and the vertical speed (vz_control and altitude_hold ). Data-dependencies are causal, for instance, the function vz_filter produces the variable vz_f, which is consumed by functions vz_control and va_control. The controller receives two inputs from the cockpit, which are the orders requested by the pilot on the altitude h c and on the vertical air speed V a c . The Aircraft receives the orders δ ec and δ thc computed by the controller.

We have translated Rosace in Lustre/Prelude and executed it on many architectures. We have now a Lustre version on which we could make some verification.

Attitude Control of the Space Shuttle

The second use case is the Attitude and Orbital Control System (AOCS) of the famous Space Shuttle [START_REF] Cohen | Space Shuttle Attitude and Orbital Control System[END_REF]. Fig. 7a presents the different modes in which the Simplified Digital Autopilot (SDAP) of the Space Shuttle can operate. Each of them is modeled as a Simulink component. The most complex one being the AUTO MANEUVER sub-mode within the AUTO mode. Its architecture is depicted in Fig. 7b: The SDAP executive will command and execute the software logic at a frequency of 12.5 Hz. The Auto Maneuver module is processed at 1.04 Hz, it is called every 12 th DAP pass whenever SDAP is in the auto mode.

After collecting the current state from the IMUs (current attitude), the DAP, depending on the switches values entered by the crew, will send appropriate commands to the actuators (jets) to bring about a desired state. The crew can set the behavior they desire via keyboard, and by push-buttons modding discrete, such as the choices between primary/vernier jets and automatic/manual attitude control mode.

We identified and labeled in the Space Shuttle report numerous sentences that could act as requirements.

Each of these requirements is then expressed as a Lustre CoCoSpec contract and can then be expressed in the Simulink model.

A list of 49 identified requirements can be found in https://coco-team.github.io/ spaceshuttle/requirements.html. Table 2 represents some of the identified requirements and their verification results.

We have now a Lustre/Prelude version that we will port on multi-and many-core architectures.

Req. ID

Simulink

Related Works

Model-based development has been adopted widely in the design of cyber-physical system. Simulink and Scade are the reference and the most successfully used toolkits in the development of such systems. Both Simulink and Scade have code generators and some means of applying formal verification on safety requirements to find bugs early on the development process. Simulink Design Verifier (SLDV) [START_REF]Simulink Design Verifier (SLDV)[END_REF] and Scade Design Verifier [START_REF]SCADE Suite Design Verifier | Esterel Technologies[END_REF] are both commercial tools and they have their own limitations. For instance, SLDV does not support all Simulink blocks and suffers from state space exmplosion.

The objective of the CoCoSim framework is to provide an open source tool for code generation and an integration hub for others to contribute with different techniques of formal verification and code generation capable of scaling on real-case systems.

In order to perform any type of analysis on the Simulink/Stateflow models, a formal specification needs to be defined. Since the semantic of Simulink/Stateflow2 is informal, many efforts have been made to define a formal semantic of a subset of Simulink/Stateflow in many formal languages for code generation as well as for formal verification. In its PhD, Cédric Klikpo [START_REF] Cédric | Méthode de conception de systèmes temps réels embarqués multi-coeurs en milieu automobile. (Methodology of designing embedded real-time multi-core systems in automotive)[END_REF] has proposed a clear explanation of rate transition blocks. Discrete subset of Simulink has been translated to various input languages of formal verification such as NuSMV model [START_REF] Meenakshi | Tool for Translating Simulink Models into Input Language of a Model Checker[END_REF], Lustre language [START_REF] Tripakis | Translating discrete-time simulink to lustre[END_REF], SDF (Synchronous Data Flow) [START_REF] Cédric | Méthode de conception de systèmes temps réels embarqués multi-coeurs en milieu automobile. (Methodology of designing embedded real-time multi-core systems in automotive)[END_REF] or hybrid automata [START_REF] Silva | Formal verification of hybrid systems using CheckMate: a case study[END_REF]. All of the previous works are either closed source or not maintained or does not work with new Simulink version as their transla-tor parses the model in its textual format. We addressed those two challenges: it is open source and is based on Simulink API to get and compute all model information needed for translation, therefore any new Simulink release does not affect badly the translator.

Expressing multi-periodic systems with synchronous languages has been proposed in previous works. In [START_REF] Camus | A verifiable architecture for multitask, multirate synchronous software[END_REF], Scade was used to describe multiperiodic systems with harmonic period. In [START_REF] Forget | Programming Languages For Hard Real-Time Embedded Systems[END_REF], we made a state of the art of the question for the works before 2008. Some approach, similar to Prelude, was proposed in [START_REF] Alras | Model-Based Design of Embedded Control Systems by Means of a Synchronous Intermediate Model[END_REF]. More recently, Didier et al. [START_REF] Didier | Correct-by-Construction Parallelization of Hard Real-Time Avionics Applications on Off-the-Shelf Predictable Hardware[END_REF] have defined an extension of Heptagon and Hili and al. have extended ForeC [START_REF] Girault | A Multi-Rate Precision Timed Programming Language for Multi-Cores[END_REF], a C-based synchronous programming language.

Regarding code generation, there exist other works on implementation of synchronous multiperiodic systems. For code generation, [START_REF] Cédric Klikpo | Modeling Multi-Periodic Simulink Systems by Synchronous Dataflow Graphs[END_REF] presents an approach to formally define the synchronous semantic of multi-periodic Simulink system using Synchronous Dataflow Graph. In their work, they focus only on the semantic-preserving implementation of the interactions between tasks. [START_REF] Sfyrla | Compositional Translation of Simulink Models into Synchronous BIP[END_REF] presents another translation of a discrete-time Simulink into the synchronous subset of the BIP language to compare runtime performances with Simulink code generation tool.

Conclusion

We presented an overview of CoCoSim framework, a modular framework to support the analysis and the code generation of discrete Simulink models. We focused on two CoCoSim backends addressing the analysis and code generation of multi-periodic Simulink models. The first backend is addressing the V&V of multi-periodic systems by encoding them into a pure Lustre models to properly analyze the full system. The second backend is dedicated to code generation based on Prelude. We presented two use cases, the first is demonstrating the capabilities of Prelude, whereas, the second use case we demonstrated the V&V capabilities of CoCoSim.

Figure 1 :

 1 Figure 1: CoCoSim overview

Figure 2 :

 2 Figure 2: CoCoSim framework

  and P [4] projects, CoCoSim translates modularly the pre-processed mono-periodic Simulink model into an equivalent Lustre model. The translator is developed using a visitor pattern, each Simulink Subsystem is translated into a Lustre node, each instance of a Subsystem is translated into a Lustre node call and each Simulink atomic block is represented by a local Lustre equation defining the semantic of the block. The generated Lustre model has the same hierarchy as the original Simulink model and preserves the initial semantic.

Figure 3 :

 3 Figure 3: Example of a Simulink model.

Figure 3

 3 Figure 3 is a simple example of Simulink blocks running on different sample times D1 = (1s, 0s) and D2 = (2s, 0s). The Inport In1 is running on D1. The Sum block is adding two signals running on different periods D1 and D2. The Unit Delay is delaying its input signal by one step but updating its output every 2 seconds (sample time D2).

Figure 4 :

 4 Figure 4: Introducing explicit Rate Transition block in the Simulink model of Fig. 3.

Figure 5 :

 5 Figure 5: Second clock explicit solution of Fig. 3

  e. unordered, of stream equations, with possible local variables denoting internal flows. Regular arithmetic and comparison operators are lifted to sequences and are evaluated at each time step. Ifthen-else constructs are functional and should be well typed: they build values instead of sequencing imperative statements. For instance, a valid flow equation could be x = 3 + (if y > 0 then 4 else y); Stateful constructs. Temporal operator pre, for previous, enables a limited form of memory, allowing to read the value of a stream at the previous instant. It corresponds to the unit delay block in Simulink. The arrow operator, known as follow-by, allows to build a stream x0 → e as the expression e while specifying the first value x0 at time zero. A flow defined as x0 → pre u will then correspond in Simulink to a Unit Delay over flow u with initial value x0.

  x = merge c ( e1 when c ) ( e2 when not c ) ;

  C_in = make_clock ( inTs , inTsOffset ) ; C_out = make_clock ( outTs , outTsOffset ) ; From Fast to slow: outTs > inTs, ZOH block The communication is direct and the output port RTB_Y simply takes the value of the input port RTB_U on its sample time: :ON; Integrity:ON; Sample time [4s,0] => type ZOH Simulink: = make_clock(4, 0); true false false false true false false false Counter = Counter_SS(); :ON; Integrity:ON; Sample time [1s,0] => type 1/z Simulink: = make_clock(2, 0); true false true false true false true false Counter = Counter_SS(); C_2_0 (0.0 → pre Counter) ((0.0 → pre Y ) when not C_2_0);

Figure 6 :

 6 Figure 6: Sampled counter

Figure 7 :Figure 8 :

 78 Figure 7: SDAP Architecture

Table 2 :

 2 controller is deflected in any axis, the SDAP automatically switches to manual mode Req_p19_5 Auto Manual Maneuver When the maneuver mode is changed from manual to auto, if the bypass flag is ON, it is set to OFF and the auto maneuver initialization flag is set to ON. CoCoSim is detailed as compilation time to Lustre and actual verification. SLDV is the model-checking tool provided by MathWorks. Selection of requirements and verification results

			Component	Text
	Req_p63_1	Call Jet Select		The two types of thrusters may not be used simultaneously
	Req_p19_1 If the hand Req_p27_1 Auto Manual Maneuver Auto Maneuver tests the rotation angle rota-Auto Manual Switch
					tion_angle_delta_theta against two numerical cri-
					teria.	If rotation_angle_delta_theta is larger than
					y = SCALARBIAS + 2 * Deadband, the module places
					itself in the maneuver mode; if rotation_angle_delta_theta
					is less than x = SCALARBIAS + Deadband, the hold
					mode results.
	Req. ID	Simulink Com-#blocks	SLDV Result	SLDV Time	CoCoSim Result	Total Time	Lustre Gen. Time	Verification Time
		po-
		nent
	Req_p63_1 Call	34	Valid	27s	Valid	21s	19s	2s
		Jet
		Select
	Req_p19_1 Auto	8	Valid	7s	Valid	12s	10s	2s
		Man-
		ual
		Switch
	Req_p19_5 Auto	589	Valid	23s	Valid	34s	30	4s
		Man-
		ual
		Ma-
		neu-
		ver
	Req_p27_1
	Note that total time reported for

https://www.mathworks.com/help/pdf_doc/simulink/slref.pdf

RTB_tmp =

merge C_in RTB_U (( dft -> pre RTB_tmp ) when not C_in ) ; RTB_Y = RTB_tmp when C_out ;

From slow to fast: outTs < inTs, 1/z block The block behaves as a Unit Delay. We first compute the previous value of the input signal, then compute the values in the base clock by keeping the previous values when it is undefined and finally sample the signal to the output clock. In Table . 1 we give few different settings of RTB block and their translation in Lustre and Prelude. We set the Counter Subsystem with a Simulink clock of (2s, 0s) that is the counter is incremented by 1 every 2 seconds. The common base clock is (1s, 0s).


Frédéric Boniol

Claire Pagetti

Nathanaël Sensfelder

Identification of multi-core interference

Keywords: Multi-core, certification, timing interference

Introduction

The last decade has seen the emergence of multi-core processors, i.e. chips integrating several cores linked by a shared interconnect. Although these architectures have been shown to provide huge gains in performance, they have severe lapses in time predictability [START_REF] Wilhelm | The worst-case executiontime problem -overview of methods and survey of tools[END_REF][START_REF] Wilhelm | Embedded systems: Many cores -many problems[END_REF], one of the key elements of certification expectations.

Identification of potential interference

Aeronautic certification authorities, in association with industrial manufacturers, have published the Multi-Core Certification Review Item (MCP-CRI) [START_REF]The Use of Multi-Core Processors in Safety-Critical Applications -CRI[END_REF] (also published as the CAST-32A position paper [7]), in order to provide a set of guidances for software planning and verification on multi-core chips.

Due to resource sharing, couplings exist at the platform level. These can cause interference between applications, which, in turn, may lead to unexpected delays, and even the alteration or loss of data. These three issues are not acceptable in the aeronautics domain and must thus be avoided. In terms of certification, this entails a four steps process: First, the applicant must identify all interference channels. In the CAST-32A terminology, an interference channel is a platform property that may cause interference between independent applications. Second, the applicant must classify the interference as either acceptable, tolerable, or unacceptable. Third, for each unacceptable interference, they must provide a mean of mitigation to prevent the system from having catastrophic behaviors. In that context, mitigation signifies that some mechanisms have been proposed to forbid unacceptable interference or reduce their effect to acceptable or tolerable levels. For example, if a resource being accessed in parallel by more than two requesters would lead to a non-acceptable delay, mitigation could take the form of a run-time mechanism that sequentializes the access. Fourth and final, the applicant must argue why the means of mitigation are adequate and why unacceptable interference will never occur during aircraft operations.

This requirement is called resource usage 3 in the CAST-32A. In the sequel, we will only focus on this particular objective and, more precisely, on the identification of interference.

Objectives and contribution

To the best of our knowledge, few works have proposed solutions for resource usage 3. Researchers from Thales have proposed the Initiator-Target Model [START_REF] Brindejonc | Avoidance of dysfunctional behaviour of complex cots used in an aeronautical context[END_REF][START_REF] Jean | Assurance methods for cots multi-cores in avionics[END_REF][START_REF] Mutuel | Investigation of error types associated with failures in multicore processors[END_REF][START_REF] Mutuel | Assurance of Multicore Processors in Airborne Systems[END_REF] to help identify the interference channels on multi-core chips. Their model is very simple, but suffers from a combinatorial explosion.

Phylog is a French project (2016-2020), funded by the French civil aeronautic agency (DGAC), which aims at offering a model-based and software-aided certification framework for aeronautics systems based on multi/many-core architectures. In [START_REF] Bieber | A model-based certification approach for multi/many-core embedded systems[END_REF], we have defined the premises of the Phylog model, presented the notions of interference channels and transactions, and shown an automated process to find the interference channels through the use of Weird [START_REF] Bieber | MIMOSA: Towards a model driven certification process[END_REF].

The objective of this paper is to compare and link the initiator-target and Phylog models. For that purpose, we start with a formal definition of the initiator-target model (see section 2). We then refine and formalize our former definition of interference channels (see section 3). We then show that our representation is more compact than the initiator-target model despite remaining as expressive. Indeed, our interference channels are the representative elements of the equivalence classes of an equivalence relation (see section 4). All our formalization and computation are supported by implementations made in idp [START_REF] Broes De Cat | Predicate logic as a modelling language: The IDP system[END_REF] (see section 5), used as a replacement for Weird [START_REF] Bieber | MIMOSA: Towards a model driven certification process[END_REF].

The initiator-target model

The initiator-target model has been introduced in [START_REF] Brindejonc | Avoidance of dysfunctional behaviour of complex cots used in an aeronautical context[END_REF] and reused in [START_REF] Jean | Assurance methods for cots multi-cores in avionics[END_REF][START_REF] Mutuel | Investigation of error types associated with failures in multicore processors[END_REF], and [START_REF] Mutuel | Assurance of Multicore Processors in Airborne Systems[END_REF]. The goal was to provide a theoretical view for the identification of the interference channels (called performance contentions in [START_REF] Brindejonc | Avoidance of dysfunctional behaviour of complex cots used in an aeronautical context[END_REF]) that can occur in a multi-core processor.

Overview

According to their definition, a multi-core is composed of three types of components: • Target components, i.e. end-components targeted by smart or non smart initiators.

Intermediate components (such as internal buses) between initiators and targets are simply ignored.

Example 1 Let us illustrate the initiator-target model on the simple architecture shown in Figure 1, composed of two smart initiators (the two CPUs), two non smart initiators (the two DMAs), and four targets (the two memory controllers, the PCIe controller, and one L3 cache used as SRAM memory). An interference channel is seen as a combination of single test classes (or single test cases) where an interference occurs. A single test class is a transaction initiated by an initiator and targeting a target (for smart initiators) or two targets (in case of non smart initiators).

Example 2 In the architecture depicted Figure 1, cpu 1 mem 1 , cpu 2 mem 2 , and pcie dma 1 mem 2 are examples of single test classes. The first two may denote either read or write transactions from cpu k to mem k . The last one may denote a data transfer from the PCIe device to the second memory through the dma 1 .

(cpu 1 mem 1 ) (cpu 2 mem 2 ) (pcie dma 1 mem 2 )
is a test class composed of three single test classes running in parallel.

Formalization

Let us now introduce a set-based formalization of the initiator-target model.

card(T C P ∞ ) = (1 + n T ) nSI • (1 + n 2 T ) nNSI -1 (1)
Example 3 Let us once again consider the architecture P 1 shown in Figure 1: n SI = 2, n NSI = 2, n T = 4, →= {(cpu 1 ,bus), (cpu 2 ,bus), (dma 1 , bus), (dma 2 ,bus), (bus,mem 1 ), (bus,mem 2 ), (bus,L3), (bus,pcie)}. Applying equation 1 yields:

card(T C P1 ∞ ) = (1 + 4) 2 • (1 + 4 2 )
2 -1 = 7224 meaning that the interference analysis may need up to 7224 test classes to be analyzed on this architecture. Aeronautic certification standards require the assessment of the worst case execution time (WCET) for the critical software functions running on the cores of the processor. As stated in the introduction, interference may strongly affect this execution time. It is up to the designer to characterize the severity of each interference with respect to the execution time of each software function, and, at the end, to show that all the unacceptable interference (i.e., the ones that induce too high WCETs) are properly mitigated by appropriate means (e.g., arbiters, time-triggered execution schemes, etc.). In the case of the (rather small) architecture P 1 , such an assessment requires the investigation of the 7224 test classes.

Hypotheses

In the seminal paper, there was no specific rule about the reachability of a target by an initiator. Implicitly, the authors assumed that all targets were reachable by all initiators. Moreover, they did not make a distinction on the type of transactions (e.g. read or write). Finally, they assumed a unique path from any given initiator to any given target, which is not the case in many-cores. Most commercial multi-core processors satisfy these two hypotheses. Let us formalize them:

• Hyp1. All targets are reachable by all initiators: ∀i ∈ SI ∪ NSI, ∀t ∈ T, i → * t • Hyp2. There is a unique path from an initiator to any non initiator component:

∀i ∈ SI∪NSI, ∀t ∈ O ∪ T , if i → a 1 → . . . → a n → t and i → b 1 → . . . → b m → t, then n = m and ∀k, a k = b k .
Proposition 2 The reachability relation → satisfying Hyp2 is acyclic and defines a partial order

< P : ∀α, β ∈ SI ∪ NSI ∪ T ∪ O, α < P β ⇔ α → * β.
3 Phylog model

In the Phylog project, we need to tackle the identification of all interference channels as in Brindejonc et al.'s approach.

Overview

We believe that the current initiator-target model is insufficient as is and that it must be enriched.

1. Brindejonc's approach is a black-box approach: it does not consider internal components. Two architectures with different topologies may be characterized by the same test classes, even when their interference differ.

2. Test classes do not necessarily lead to any actual interference between transactions. For instance, in the architecture P 2 depicted Figure 2, the test class (cpu 1 mem 1 ) (pcie dma 1 L3) does not cause any contention as these transactions cross two different buses in parallel without interfering with each other. Many other test classes in P 2 are interference-free as well.

3. Their approach is simple, but suffers from scalability issues: For a T4240 processor, composed of 12 cores (n SI = 12), 3 DMAs (n NSI = 3), 2 memory controllers, 1 PCIe, and 1 L3 cache used as SRAM memory (n T = 4), there are more than 10 12 test cases.

Ideally, the number of test classes to be explored should be as low as possible. We thus propose grouping them according to the interference they cause on the components. In the following, we will consider that the branching operator "+" is commutative. That is,

tr = i • ((b 1 . . . b n ) + (c 1 . . . c m )) = i • ((c 1 . . . c m ) + (b 1 . . . b n )).
Example 4 A single test class is a transaction from an initiator to one or two targets. In P 1 , the single test class cpu 1 mem 1 is the transaction cpu 1 .(bus.mem 1 + ); whereas pcie dma mem 2 is the transaction dma.(bus.mem 2 + bus.pcie).

Definition 6 We define a series of useful functions for a transaction tr

= i • ((a 1 . . . a n • b 1 . . . b m ) + (a 1 . . . a n • c 1 . . . c p )) with for all l, k b l = c k :
• hd(tr) = i (head of the transaction),

• prefix(tr) = a 1 . . . a n (common prefix of the transaction, possibly empty).

• proj 1 (tr) = i • a 1 . . . a n • b 1 . . . b m (first branch of the transaction), • proj 2 (tr) = i • a 1 . . . a n • c 1 . . . c p (second branch),
• lg(tr) = {a 1 , . . . , a n , b 1 , . . . , b m , c 1 , . . . , c m } (language of the transaction, i.e., the set of components involved),

• tl(α 1 . . . α n ) = α n (tail of a word),

• pred(α 1 . . . α n-1 • α n ) = α n-1 (penultimate component of a word).
According to hypothesis Hyp2, each tc is modeled by a unique transaction tr in the Phylog model.

Definition 7 (Transactions associated to a single test class) When (i, t) ∈ SI × T , the associated Phylog transaction is defined as phy(i, t) = tr with hd(tr) = i, tl(proj 1 (tr)) = t and proj 2 (tr)) = .

When (i, t 1 , t 2 ) ∈ NSI × T × T , the associated Phylog transaction is defined as phy(i, t 1 , t 2 ) = tr with hd(tr) = i, tl(proj 1 (tr)) = t 1 and tl(proj 2 (tr)) = t 2 .

m (a) tr = i • ((b 1 . . . bm)+ ). i b 1 c 1 . . . . . . b m c p (b) tr = i • ((b 1 . . . bm) + (c 1 . . . cp)) with ∀l, k, b l = c k . i a 1 . . . a n b 1 c 1 . . . . . . b m c p (c) tr = i • ((a 1 . . . an • b 1 . . . bm) + (a 1 . . . an • c 1 . . . cp)) with ∀l, k, b l = c k .

Test classes revisited -Truncated transactions

A test class, as introduced by definition 3, is a set of single test classes tc 1 , . . . , tc n issued by n different initiators.

Definition 8 Let tc = {(i 1 , t 1 ) . . . (i m , t m , t m )} be a test class, the associated Phylog transactions are phy(tc) = {tr 1 , . . . , tr m } = {phy(i 1 , t 1 ), . . . , phy(i m , t m , t m )}.

The shared components in a set of transactions are then: Definition 9 Let tc = {tr 1 , . . . , tr n } be a set of transactions, the language associated to tc is defined by: lg(tc) = lg(tr 1 ) ∪ . . . ∪ lg(tr n ) and shared(tc) is the set of components involved in all transactions: shared(tc) = lg(tr 1 ) ∩ . . . ∩ lg(tr n )

We define the Phylog test classes as the sets of truncated transactions where the interference-free parts of transactions are translated as the empty word .

such that ∃tc = {(i i , t i ) . . . (i m , t m )(i m+1 , t m+1 , t m+1 ) . . . (i n , t n , t n )} ∈ T C P ∞ with • ∀k, hd(tr k ) = i k ;
• ∀j ≤ m, tr j = trunc(tc, phy(i j , t j )) where trunc(tc, i • (a 1 . . . a n + )) = i • (a 1 . . . a p + ) with p ≤ n and a p ∈ shared(tc);

• ∀m + 1 ≤ j ≤ n, ∃k ≤ 3, tr j = trunc k (tc, phy(i j , t j , t j ))
where Notations 2 When handling truncated transactions generated by smart initiators, we will deliberately remove the second branch which is empty. For instance, cpu 1 .bus stands for cpu 1 .(bus + ). This contraction cannot be applied to truncated transactions generated by non smart initiators, as it would then be impossible to differentiate the prefix part.

trunc 1 (tc, i • (a 1 . . . a n + b 1 . . . b m )) = i • (
Example 5 In P 1 , ptc = {cpu 1 .bus, cpu 2 .bus} ∈ Trans. Indeed, cpu k .bus can be obtained as the truncation of cpu k • (bus.pcie + )).

In architecture P 2 , ptc = {cpu 1 .bus 1 , dma 1 .(bus 1 + )} ∈ Trans. Indeed, let tc = {(cpu 1 , pcie), (dma 1 , pcie, mem 1 )} then cpu 1 .bus 1 = trunc(tc, cpu 1 • (bus 1 .pcie + )) and dma 1 .(bus 1 + ) = trunc 2 (tc, dma 1 .(bus 1 .pcie + bus 2 .mem 1 )).

However, in P 2 , {dma 1 .(bus 1 + ), dma 2 .(bus 1 + )} ∈ Trans. Indeed, dma k .(bus 1 .X 1 + bus 1 .X 2 ) with X j ∈ {pcie, L3} can only be truncated with trunc 1 as dma k .(bus 1 + bus 1 ). And the test case {dma 1 .(bus 1 .X 1 +bus 2 .Y 2 ), dma 2 .(bus 1 .X 2 + bus 2 .Y 2 )} with X j ∈ {pcie, L3} and Y j ∈ {mem 1 , mem 2 } can only be truncated by trunc 3 as dma k . (bus 1 + bus 2 ).

On the contrary, ptc = {cpu 1 .bus 1 , dma 1 .(bus 1 + ), dma 2 .(bus 1 + )} ∈ Trans. Indeed, the completion on the DMAs imposes to reach bus 2 but this component will not be in the shared component as cpu 1 cannot reach it.

Interference channel

We can now formally define the notion of interference channel. We distinguish two kinds of interference channels: the 1-interference channels which involve a single shared component, and the 2-interference channels which involve two shared components.

1-Interference channels

Definition 11 (1-Interference channel) For an architecture P = (C, →), a 1-interference channel is defined as

(c, n T R n 1 )
with c ∈ O ∪ T and

T R n 1 =            {tr 1 , . . . , tr n } ∈ Trans ∀i, tl(proj 1 (tr i )) = c ∧ tl(proj 2 (tr i )) = {c, } ∧ ∀i = j, hd(tr i ) = hd(tr j ) ∧ pred(proj 1 (tr i )) = pred(proj 1 (tr j ))           
An interference channel ends with a shared component c. What happens after is irrelevant, as serialization occurs at that point and the transactions do not interfere with each other later on. We apply the same reasoning as in network calculus [START_REF] Boudec | Network Calculus: A Theory of Deterministic Queuing Systems for the Internet[END_REF] when packets share a common path on several switches. This is known as the pay burst only once rule. Thus, interference only occurs on the first component shared by the n transactions. Note that this could be improved in several ways, such as by considering the component entailing the worst case delay instead of simply taking the first one, or by grouping successive components into a super-component.

Example 6 Let us again consider the P 1 of Figure 1. There is a unique 1-interference channel with 11 combinations of transactions capable of occurring on the bus: bus,

                                   {cpu 1 .
                                  
Example 7 Let us consider P 2 of Figure 2 and let us focus on bus 1 (it is similar for bus 2 ). There are 28 combinations of transactions. The interesting parts are those featuring the dma. Either the second branch of the transaction reaches bus 1 , or it is pruned (and replaced by ). The notation dma 2 .(bus 1 + {bus 1 , }) represents the two transactions dma 2 .(bus 1 + bus 1 ) and dma 2 .(bus 1 + ) in order to reduce the length of the table below.

bus 1 ,                                                    {cpu 1 .
, })}                                                   

2-Interference channels

Focusing on 1-interference channels is unfortunately insufficient because of the double branches of transactions issued by non smart transactions. Indeed, those branches can conflict on two components: one per branch. Thus, two components can be accessed in parallel by all transactions. We must then define 2-interference channels. There is no 3 or more-interference channels because the maximal number of branches per transaction is 2.

Definition 12 (2-Interference channel) For an architecture P = (C, →), a 2-interference channel is defined as

(c 1 , c 2 , n T R n 2 ) with c 1 , c 2 ∈ O ∪ T , c 1 = c 2 and T R n 2 =            {tr 1 , . . . , tr n } ∈ Trans ∀i, (tl(proj 1 (tr i )) = c 1 ∧ tl(proj 2 (tr i )) = c 2 ) ∧∀i = j, hd(tr i ) = hd(tr j ) ∧ pred(proj 1 (tr i )) = pred(proj 1 (tr j )) ∧ pred(proj 2 (tr i )) = pred(proj 2 (tr j ))           
Example 9 In P 2 , depicted in Figure 2, there is a unique 2-interference channel occurring on the buses. Example 10 There is no 2-interference channel in the P 1 architecture. This means that, with our approach, analyzing the severity of the interference caused by the 11 transactions listed in example 6 is sufficient, compared to the 7224 test classes of the initiator target model (see example 3). This reduction comes from a better modeling of the platform and from symmetry properties. The severity of the interference is evaluated with respect to the expected behavior of the software functions hosted by the platform.

bus 1 , bus 2 , {dma 1 • (bus 1 + bus 2 ), dma 2 • (bus 1 + bus 2 )} cpu 1 dma 1 (IO transfer for F 1 ) cpu 2 dma 2 (IO transfer for F 2 ) F 1 pcie ↔ L 3 F 1 pcie ↔ L 3 F 2 pcie ↔ L 3 F 2 pcie ↔ L 3
To illustrate this, let us consider the following time-triggered execution scheme depicted in figure 5: (1) cpu 1 (resp. cpu 2 ) hosts a software function F 1 (resp. F 2 );

(2) memory mem 1 (resp. mem 2 ) is dedicated to F 1 (resp. F 2 ), meaning that F 1 never tries to access mem 2 and, conversely, F 2 never tries to access mem 1 ;

(3) dma 1 (resp. dma 2 ) manages input/output transfers of F 1 (resp. F 2 ); (4) input/output data are stored in L 3 ;

(5) F 1 and F 2 are periodically scheduled in non-overlapping time windows; and (6) dma 1 (resp. dma 2 ) is only activated by F 1 (resp. F 2 ). Then, among the 11 transactions listed in example 6, only the second one ({cpu 1 .bus, dma 1 .(bus + bus)}) and the fifth one ({cpu 2 .bus, dma 2 .(bus + bus)}) can occur. The potential interference caused by the other nine transactions are avoided by the execution scheme. Therefore, to meet the certification requirements it is sufficient to evaluate the WCET of F 1 (resp. F 2 ) and the WCET of the dma 1 (resp. dma 2 ) transfers with the interference caused by the second (resp. fifth) transaction. These interference will be said to be acceptable if these WCETs are smaller than the corresponding time windows planned by the execution model. Otherwise, they will be said to be unacceptable.

Comparison between the initiator-target model and Phylog model

The Phylog model can be seen as the definition of equivalence classes for the initiator-target model.

Definition 13 (Interference-free test classes) Some test classes listed in T C P ∞ do not lead to an interference channel:

1. Single test classes, as they do not generate any conflict, 2. Test classes tc such that phy(tc) = (tr 1 , . . . , tr n ), n > 1 and shared(phy(tc)) = ∅, that is, no component is shared by the n transactions.

Test classes satisfying one of these two rules are said to be interference-free.

Example 11 Let us consider P 2 once again. The test class {(cpu 1 , mem 1 ), (dma 1 , pcie, L3)} is interferencefree: no component is shared by the two transactions (rule 2 of the definition). However, {(cpu 1 , mem 1 ), (dma 2 , pcie, mem 2 )} is not interference-free, since bus 1 is shared by the two transactions.

Let us note that a transaction, as depicted in Figure 3, defines a partial order relation over the language for the transactions:

• if (a 1 . . . a n ) = , then ∀i = 1 . . . n -1, a i < tr a i+1 • if (a 1 . . . a n ) = , then a n < tr b 1 • if (a 1 . . . a n ) = and if (c 1 . . . c p ) = , then a n < tr c 1 • ∀i = 1 . . . m -1, b i < tr b i+1 • if (c 1 . . . c p ) = , then ∀i = 1 . . . p -1, c i < tr c i+1
< tr is the order generated by the oriented paths followed by the transaction.

Proposition 4 Let P = (C, →), < P is the partial order (see proposition 2), tc = {tr 1 , . . . , tr n } a Phylog test class, and S = shared(tc) the set of components shared by all the transactions tr i . Let min(S, < P ) = {α ∈ S | ∀β ∈ S, either α < P β or ¬(β < P α)} be the set of smallest components in S for < P . Then

• either min(S, < P ) = ∅,

• or min(S, < P ) = {α} and ∀tr i , ∀β ∈ S, α < tri β (meaning α is the first component crossed by all tr i ),

• or min(S, < P ) = {α, β} and ∀tr i , ∀γ ∈ S, α < tri γ ∨ β < tri γ (meaning α (resp. β) is the first crossed in some branches in which β (resp. α) is not involved, as b 1 and c 1 in Figure 4).

Proof 2 Let us consider tr

1 = i • ((a 1 . . . a m • b 1 . . . b p ) + (a 1 • a m • c 1 . . . c q )) of tc with b j = c k for all j, k.
Remember that S = shared(tc) = lg(tr 1 ) ∩ . . . ∩ lg(tr n ). Then S ⊂ {a 1 , . . . , a m , b 1 . . . , b p , c 1 , . . . , c q }. Let us consider 5 cases:

• case 1: S = ∅. Then min(S, < P ) = ∅. Meaning tc is interference-free.

• case 2: S ∩ {a 1 , . . . a m } = ∅. Then ∃k, min(S, < tr1 ) = {a k }. Moreover, min(S, < P ) = min(S, < tr1 ) = {a k }.

• case 3: S ⊂ {b 1 , . . . b p }. Then ∃k, min(S, < tr1 ) = {b k }. Then min(S, < P ) = min(S, < tr1 ) = {b k }.

• case 4: S ⊂ {c 1 , . . . c q }. Then ∃k, min(S, < tr1 ) = {c k }. Then min(S, < P ) = min(S, < tr1 ) = {c k }.

• case 5: S ⊂ {b 1 , . . . , b p , c 1 , . . . c q } and S∩{b 1 , . . . b p } = ∅ and S∩{c 1 , . . . c q } = ∅. Then ∃k, l, min(S, < tr1

) = {b k , c l } with ¬(b k < tr1 c l ) and ¬(b k < tr1 c l ). Then min(S, < P ) = min(S, < tr1 ) = {b k , c l }.
Example 12 For P 2 and its {(dma 1 , mem 1 , pcie), (dma 2 , mem 2 , pcie)} test class, the associated transactions are Proof 3 ≡ is reflexive. Indeed, let tc be a test class, min(shared (phy(tc)), < P ) is defined in a unique way.

• tr 1 = dma 1 • (bus 1 • pcie + bus 2 • mem 1 ) • tr 2 = dma 2 • (bus 2 • mem 2 + bus 1 • pcie) S =
≡ is symmetric, because we only handle sets. ≡ is transitive: if min(S 1 , < P ) = min(S 2 , < P ) and min(S 1 , < P ) = min(S 3 , < P ) then min(S 2 , < P ) = min(S 3 , < P ). Same for hd(tc i ).

Proposition 6 The Phylog interference channels are a representative of the ≡ relation classes. More precisely, let tc = {(i 1 , t 1 ) . . . (i m , t m , t m )}, let S = shared(phy(tc)).

• if min(S, < P ) = ∅, there is no interference channel in Phylog,

• if min(S, < P ) = {c}, the associated interference channel in Phylog is a 1-interference channel in c, ∪ n T R n 1 , i.

Experiments

In this section, we first illustrate the idp code supporting the interference channels computations. We then provide some experiments with idp. ¦ ¥

Coding the initiator target model

Coding the Phylog model

We compute an intermediate predicate to combine two transactions composed of a single branch each.

Trans2, still for a maximal of 3 components in a path, is defined below.

Code 5 § ¤

// when the shared component is at the end

! x [ Component ]: ! i1 [ Initiator ]: ! i2 [ Initiator ]: ! x1 [ Component ]: ! x2 [ Component ]: ! x3 [ Component ]: ! x4 [ Component ]: Trans2 (x , i1 , x1 , x2 ,x , i2 , x3 , x4 , x ) <- ( Path ( i2 , x3 , x4 , x ) & Path ( i1 , x1 , x2 , x ) & ( i1 < i2 ) & ( x2 ~= x4 )).

¦ ¥

There is one predicate per T R n 1 . For instance, T R

¦ ¥

There is also one predicate per T R n 2 . The code for T R ¦ ¥

Some results

idp computes the predicates of the previous examples in less than a second. Increasing the number of smart initiators, non-smart initiators, targets, or intermediary components does not appear to increase the execution time. Even when modeling a Kalray MPPA [START_REF] Corporation | The MPPA hardware architecture[END_REF] compute cluster, composed of 16 cores, 32 intermediary components, and 16 targets, resolution of those predicates (exposing a total of 1920 interference channels) is still completed in sub-second times.

To ensure their correctness, we have also used idp to compute the ≡ relation classes of the aforementioned examples, and found them to be compliant with the propositions made in this paper.

Related Work

Interference analysis in multi-core processors has received significant attention in recent years. A first class of these works focuses on the impact of shared hardware resource contention on the execution time of software application hosted by the processor. For instance, [START_REF] Dasari | An analysis of the impact of bus contention on the wcet in multicores[END_REF] considers a multi-core architecture composed of a single bus providing access to a shared memory, and it proposes a method to determine an upper bound on the number of bus requests that software tasks can generate in a given time interval. Both [START_REF] Bin | Studying co-running avionic real-time applications on multi-core cots architectures[END_REF] and [START_REF] Sylvain Girbal | Using monitors to predict co-running safety-critical hard real-time benchmark behavior[END_REF] focus on measurement techniques based on dedicated stressing benchmarks and hardware monitors to characterize the architecture and the shared resources that can cause interference between software applications.

A second class of works focuses on methods to avoid interference. For instance, [START_REF] Becker | Contention-free execution of automotive applications on a clustered many-core platform[END_REF] proposes a contention-free execution framework to execute automotive software application on many-core platforms. [START_REF] Perret | Temporal isolation of hard real-time applications on many-core processors[END_REF] proposed a similar approach which relies both on a development work-flow, and the use of an execution model defined as a set of rules to be followed by the designer and asserted through the run-time in order to enforce specific behaviors. Both [START_REF] Becker | Contention-free execution of automotive applications on a clustered many-core platform[END_REF] and [START_REF] Perret | Temporal isolation of hard real-time applications on many-core processors[END_REF] target a TDMA execution model, and use a Constraint Programming formulation to find an optimal time-triggered schedule on each core.

In order to tackle multi-core aeronautics certification-related issues, several projects have been funded. One of the first was MULCORS [START_REF] Jean | MULCORS-Use of Multicore Processors in airborne systems[END_REF], which clearly identified the need to change and adapt the current certification standard. Since then, several attempts at precisely defining such new recommendation have been done, such as the Multi-core Certification Review Item (MCP-CRI) [START_REF]The Use of Multi-Core Processors in Safety-Critical Applications -CRI[END_REF]. In other parts of the MCP-CRI, [START_REF] Jean | White Paper on Issues Associated with Interference Applied to Multicore Processors[END_REF] proposed definitions for interference channels, interference sources, and interference targets, and they proposed a process to reduce the number of interference. A more recent work proposed by [START_REF] Agirre | On the Tailoring of CAST-32A Certification Guidance to Real COTS Multicore Architectures[END_REF] tried to adapt the MCP-CRI certification objectives to COST MCP architectures. For that purpose, they showed that the MCP-CRI objectives can be grouped into three high level principles: (1) determining the final configuration, (2) managing interference channels, and (3) verifying the use of shared resources. They showed, through a particular case study (the Freescale P4080 processor), that the second objective (managing interference channels) highly depends on detailed information about the behavior of the resources. And they showed that predicting interference on a COTS multi-core architecture is a very challenging task because of the amount of required information. A way to help the certification application to master the complexity of the architecture is then to use a formal model of the architecture and a formal analysis method to explore the set of interference channels. Such is the aim of our contribution.

Conclusion

In this paper, we have formally defined the initiator-target model and compared it with the Phylog approach. Our representation requires more details on the internal of the platform but offers a more practical size description. Our work was supported with idp tool.

In the future, we will apply our model to other multi-cores and extend our model to many-core platforms. We will also measure the gains of going deeper in the description of the architecture.

Figure 1 : Architecture P 1 Notations 1

 111 Figure 1: Architecture P 1

2 Figure 2 : Architecture P 2 3. 2

 2222 Figure 2: Architecture P 2

Proposition 3 Proof 1

 31 Let P = (C, →) be an architecture satisfying Hyp1 and Hyp2. Let tr = i • ((b 1 . . . b n ) + (c 1 . . . c m )) be a transaction in P . Then: 1. ∀j = k, b j = b k (a component can appear at most once in the b branch), 2. either (c 1 . . . c m ) = (in the case of a smart initiator) or ∀j = k, c j = c k (same as with the b branch), 3. if there exist j, k such that b j = c k , then j = k and ∀l < k, b l = c l (either the two branches do not share any component, or they share a common prefix). 4. ∀l, l > max{j | b j = c j }, b l = c l (after the common prefix, if it exists, the two branches do not share any component). The first two points come from the acyclic property of the reachable relation →. The third point is a consequence of hypothesis Hyp2. Let us suppose that there exists a common component α in the two branches (∃j, l, α = b j = c l ), then because of the unicity of the path from i to α, we have (b 1 . . . b j ) = (c 1 . . . c l ). Thus, j = l and b k = c k for all k < l. The fourth point then comes immediately.

  b

Figure 3 :

 3 Figure 3: Transaction model According to the proposition 3, a transaction can be graphically represented by the figure 3.Figure 3(a) shows a transaction made by a smart initiator.Figure 3(b) describes a transaction made by a non smart initiator without a common prefix. Figure 3(c) describes a transaction made by a non smart initiator with a common prefix. After the prefix, all the components are different. Note that the transaction Figure 3(b) is a particular case of Figure 3(c) in which the prefix word is empty: (a 1 . . . a n ) = .

Figure 3 (

 3 a) shows a transaction made by a smart initiator.

  Figure 3(b) describes a transaction made by a non smart initiator without a common prefix. Figure 3(c) describes a transaction made by a non smart initiator with a common prefix. After the prefix, all the components are different. Note that the transaction Figure 3(b) is a particular case of Figure 3(c) in which the prefix word is empty: (a 1 . . . a n ) = .

Definition 10 (

 10 Phylog test class) A Phylog test class is a set of n transactions ptc = {tr 1 , . . . , tr n }

  a 1 . . . a p + a 1 . . . a p ) with p ≤ n and a p ∈ shared(tc) and ∀k ≤ p, b k = a k trunc 2 (tc, i • (a 1 . . . a n + b 1 . . . b m )) = i • (a 1 . . . a p + ) with p ≤ n and a p ∈ shared(tc) and b p = a p and ∀k, b k ∈ shared(tc) trunc 3 (tc, i • (a 1 . . . a n + b 1 . . . b m )) = i • (a 1 . . . a p + b 1 . . . b l ) with p, l ≤ n and a p ∈ shared(tc) and b l ∈ shared(tc) We note Trans the set of Phylog test classes.

Example 8 Figure 4 :

 84 Figure 4: Architecture P 3

Figure 5 :

 5 Figure 5: An execution scheme for architecture P 1

Definition 14

 14 For an architecture P = (C, →) and a transaction tr = i•((a 1 . . . a n •b 1 . . . b m )+(a 1 . . . a n • c 1 . . . c p )), let us define the relation < tr over lg(tr) as:

{bus 1 ,Proposition 5

 15 bus 2 , pcie}, and min(S, < P ) = {bus 1 , bus 2 }. Definition 15 (Relation ≡) Let us define the relation ≡ on the Brindejonc et al. test classes. Let tc 1 and tc 2 be two test classes. Let S 1 = shared(phy(tc 1 )) and S 2 = shared(phy(tc 2 )), then tc 1 ≡ tc 2 ⇐⇒ min(S 1 , < P ) = min(S 2 , < P ) ∧ (S 1 = ∅ ∨ hd(tc 1 ) = hd(tc 2 )) The relation ≡ is an equivalence relationship.

Proof 4

 4 e. tr = {tr 1 , . . . , tr m } ∈ T R m 1 with hd(tr) = hd(tc);• if min(S, < P ) = {c 1 , c 2 }, the associated interference channel in Phylog is a 2-interference channel c1, c2, ∪ n T R n 2 ,i.e. tr = {tr 1 , . . . , tr m } ∈ T R m 2 with hd(tr) = hd(tc). Case interference-free channel: all these test classes are associated to the empty set of Phylog. Case min(S, < P ) = {c} (resp. = {c 1 , c 2 }): we apply the truncation of definition 10 where the transactions stop at a p = c (resp. a p = c 1 and b l = c 2 ) and then {tr 1 , . . . , tr m } is in T R m 1 (resp. T R m 2 ).

•

  Smart initiator components, i.e. components which can initiate single transactions through the architecture to target components. Processing cores (CPU) are examples of smart initiator components. They can, for instance, initiate memory access transactions to memory controllers.

• Non smart initiator components, i.e. initiator components which can only initiate dual transactions (i.e., with two targets at the same time). DMA are examples of non smart initiator components.

  Definition 1 (Initiator-target model) In the initiator-target model, an architecture P is defined by P = (C, →) where• C = SI ∪ NSI ∪ T ∪ O withSI being the set of smart initiators, NSI the set of non smart initiators, T the set of targets, and O the set of other components. All those sets are disjoint. In the sequel, we will note n SI = card(SI), n NSI = card(NSI) and n T = card(T ); class for a non smart initiator is a triplet (i, t 1 , t 2 ) ∈ NSI × T × T such that there exist a path in P from i to t 2 and one to t 1 , i.e. i → * t 2 and i → * t 1 . In the sequel, we write indifferently (i, t 1 , t 2 ) or t 1 i t 2 . Let P = (C, →) be an architecture. A test class is a set of n single test classes and disjoint initiators. For instance, a test class t c of size 2 is of form t c = {(i 1 , t 1 ), (i 2 , t 2 )} or t c = {(i 1 , t 1 ), (i 2 , t 2 , t 3 )} or t c = {(t 1 , i 1 , t 2 ), (i 2 , t 3 , t 4 )} with i 1 = i 2 . In the sequel, we write indifferently {(i 1 , t 1 ), (i 2 , t 2 )} or (i 1 t 1 ) (i 2 t 2 ). An interference channel is a test class composed of 2 or more single test classes.

	• →⊆ C × C are the hardware connections between components.
	Definition 2 (Single test class) For an architecture P = (C, →), a single test class for a smart ini-
	tiator is a pair (i, t) ∈ SI × T such that there exists a path in P from i to t, i.e. i → * t. In the sequel, we
	write indifferently (i, t) or i	t.
	A single test Definition 3 (Test classes) Definition 4 Let P = (C, →) be an architecture. Let us note T C P ∞ the set of test classes and T C P n those
	of size n:
		nSI+nNSI
		T C P ∞ =	T C P n
		n=1
	Proposition 1 (Total number of test classes [6]) The number of all possible test classes of P is:

  bus 1 , cpu 2 .bus 1 }, {cpu 1 .bus 1 , dma 1 .(bus1 + bus 1 )}, {cpu 1 .bus 1 , dma 1 .(bus 1 + )}, {cpu 1 .bus 1 , dma 2 .(bus 1 + {bus 1 , })}, {cpu 2 .bus 1 , dma 1 .(bus 1 + {bus 1 , })}, {cpu 2 .bus 1 , dma 2 .(bus 1 + {bus 1 , })}, {dma 1 .(bus 1 + {bus 1 , }), dma 2 .(bus 1 + {bus 1 , })}, {cpu 1 .bus 1 , cpu 2 .bus 1 , dma 1 .(bus 1 + {bus 1 , })}, {cpu 1 .bus 1 , cpu 2 .bus 1 , dma 2 .(bus 1 + {bus 1 , })}, {cpu 1 .bus 1 , dma 1 .(bus 1 + {bus 1 , }), dma 2 .(bus 1 + {bus 1 , })}, {cpu 2 .bus 1 , dma 1 .(bus 1 + {bus 1 , }), dma 2 .(bus 1 + {bus 1 , })}, {cpu 1 .bus 1 , cpu 2 .bus 1 , dma 1 .(bus 1 + {bus 1 , }), dma 2 .(bus 1 + {bus 1

  SI, NSI, T and O are represented as types. → is a predicate with two parameters. Path computes all paths from SI to T . For our modeling, we chose to hard code the maximal length of a path. Thus, if a path is shorter, we use NULL to complete the path. For instance, in P 1 , if the maximal length is 4, the path from CPU 1 to mem 1 is represented as Path(CPU 1 , interconnect, mem 1 , NULL) = true. SingleTestCase computes the single test cases. Again, the length is imposed to 3, because of the non smart initiator. The test case CP U 1 mem 1 is represented as SingleTestCase(CPU 1 , mem 1 , NULL) = true.

	Code 1 § type SInitiator	¤
	type NSInitiator
	type Initiator contains SInitiator , NSInitiator
	type Reactive
	type Target
	type Component contains Reactive , Target , Initiator ¦	¥
	A predicate Code 2 § ! i [ Initiator ]: ! x1 [ Component ]: ! x2 [ Component ]:	¤
	! x3 [ Component ]: Path (i , x1 , x2 , x3 ) <-
	¦	( Edge (i , x1 ) & Edge ( x1 , x2 ) & Edge ( x2 , x3 )).	¥
	A predicate Code 3 § ! i [ NSInitiator ]: ! t1 [ Target ]: ! t2 [ Target ]:	¤
	Singl eTestCa se (i , t1 , t2 ) <-
	Code 4 § ! i1 [ NSInitiator ]: ! t1 [ Target ]: ! t2 [ Target ]:	¤
	! i2 [ NSInitiator ]: ! t3 [ Target ]: ! t4 [ Target ]:
	Coupl eTestCa se ( i1 , t1 , t2 , i2 , t3 , t4 ) <-
		( Sin gleTest Case ( i1 , t1 , t2 ) &
		Singl eTestCa se ( i2 , t3 , t4 ) & ( i1 < i2 )).

? x [ Component ]: ? z [ Component ]: ? v [ Component ]: ? y [ Component ]: ? h [ Component ]: ? l [ Component ]: ( Path (i ,x , t1 , z ) | Path (i ,x ,z , t1 ) | Path (i , t1 ,z , v )) & ( Path (i ,y , t2 , h ) | Path (i ,y ,h , t2 ) | Path (i , t2 ,h , l )).

¦ ¥

Finally, there is one predicate per T C P n . For instance, test cases of size 2 are coded by CoupleTestCase.

  2 2 is given below.

	Code 7 § ! x1 [ Component ]: ! x2 [ Component ]: ! i1 [ NSInitiator ]:	¤
	! i2 [ NSInitiator ]: ! y1 [ Component ]: ! y2 [ Component ]:
	! y3 [ Component ]: ! y4 [ Component ]: ! y5 [ Component ]:
	! y6 [ Component ]: ! z1 [ Component ]: ! z2 [ Component ]:
	! z3 [ Component ]: ! z4 [ Component ]: ! z5 [ Component ]:
	! z6 [ Component ]:
	2 Interf2 ( x1 , x2 , i1 , y1 , y2 , y3 , y4 , y5 , y6 ,
	i2 , z1 , z2 , z3 , z4 , z5 , z6 ) <-
	( Trans2 ( x1 , i1 , y1 , y2 , y3 , i2 , z1 , z2 , z3 )
	& Trans2 ( x2 , i1 , y4 , y5 , y6 , i2 , z4 , z5 , z6 )
	& ( x1 < x2 )).