Julien Forget

Frédéric Boniol

David Lesens

Claire Pagetti

Implementing Multi-Periodic Critical Systems: from Design to Code Generation ⋆

This article presents a complete scheme for the development of Critical Embedded Systems with Multiple Real-Time Constraints. The system is programmed with a language that extends the synchronous approach with high-level real-time primitives. It enables to assemble in a modular and hierarchical manner several locally mono-periodic synchronous systems into a globally multi-periodic synchronous system. It also allows to specify flow latency constraints. A program is translated into a set of real-time tasks. The generated code (C code) can be executed on a simple real-time platform with a dynamic-priority scheduler (EDF). The compilation process (each algorithm of the process, not the compiler itself) is formally proved correct, meaning that the generated code respects the real-time semantics of the original program (respect of periods, deadlines, release dates and precedences) as well as its functional semantics (respect of variable consumption).

Introduction

Embedded systems have successfully been implemented with synchronous languages in the past. In particular, data-flow synchronous languages (Lustre/ Scade [START_REF] Halbwachs | The synchronous data-flow programming language LUSTRE[END_REF], Signal [START_REF] Benveniste | Synchronous programming with events and relations: the Signal language and its semantics[END_REF]) are well adapted for describing precisely the data flow between the communicating processes of the system. In [START_REF] Forget | A multi-periodic synchronous data-flow language[END_REF] we proposed an extension of synchronous languages to design multi-periodic systems efficiently, by assembling several synchronous nodes into a multi-periodic synchronous program. Such an approach allows to describe the real-time aspects and the functional aspects of a system in the same framework. The purpose of the paper is to give an overview of the language capabilities and to describe the compilation chain through the programming of a case study. The generated code is targeted for a simple real-time platform with the earliest-deadline-first (EDF) scheduling policy [START_REF] Liu | Scheduling algorithms for multiprogramming in a hard-real-time environment[END_REF]. We present the whole compilation chain but we do not get into the details of the proofs, which can be found in [START_REF] Forget | Programming and implementing Control-Command systems[END_REF]. We focus more particularly on the generated code, which gives a concrete illustration of the compilation and summarizes our contribution.

Motivation

The development of an industrial critical system may involve several teams, which separately define the different functions of the system. The functions are then assembled by the integrator, who implements the communications between the functions. Currently, this integration process lacks a formal language to ease the design process and to ensure the correctness of the global system.

We consider the simplified Flight Control System of Fig. 1 as a case study. This system controls the attitude, the trajectory and the speed of an airplane in auto-pilot mode. It consists of three communicating sub-systems. Each subsystem consists of several operations (represented by boxes in the figure ) and executes repeatedly at a periodic rate. The fastest sub-system executes at 10ms, it acquires the state of the system (angles, position, acceleration) and computes the feedback law of the system. The intermediate sub-system is the piloting loop, it executes at 40ms and manages the flight control surfaces of the airplane. The slowest sub-system is the navigation loop, it executes at 120ms and determines the acceleration to apply. The required position of the airplane is acquired at the slow rate. The three sub-systems are first defined separately by different teams. The integrator then assembles them in the global system and specifies how they communicate. The language focuses on this assembly level.

Contribution

The main novelties of our approach are: first the integrator can develop the complete system in a unified formal framework (a high-level formal language) and second the language along with its compiler covers the development of the system from its design to its implementation, through automated code generation.

This relies on two different research domains. On the one hand, scheduling theory focuses mainly on satisfying system real-time constraints but usually disregards system functional behaviour. This ensures the correctness of the temporal properties of the system, but makes it hard to verify the functional correctness of the system. In the case of multi-periodic systems, this often leads to non-deterministic process communications. On the other hand, synchronous languages focus on the correctness of the functional behaviour of the system and ensure that it is deterministic. However, classic synchronous languages abstract from real-time (except some recent extensions discussed in Sect. 7), which makes them ill-adapted to the implementation of multi-periodic systems.

Our work combines scheduling theory and synchronous languages to ensure both the functional and the temporal correctness of multi-periodic systems. This is particularly suitable for the implementation of critical systems. The integrator programs the system with the language introduced in [START_REF] Forget | A multi-periodic synchronous data-flow language[END_REF], which extends synchronous languages with high-level real-time primitives. The compiler then generates the set of real-time tasks corresponding to this program. Tasks are then translated into C threads, each one containing the functional code of a task completed with a deterministic data-exchange protocol that does not require synchronization primitives (such as semaphores). The threads are scheduled concurrently with the EDF policy. They can be preempted by the scheduler during their execution but preemptions do not jeopardize the functional correctness of the system. The use of an EDF scheduler departs from the classic compilation scheme of synchronous languages, which translates a program into a "single-loop" sequential code [START_REF] Halbwachs | Generating efficient code from data-flow programs[END_REF]. The single-loop scheme relies on a static-priority non-preemptive scheduling policy, which makes it ill-adapted for implementing multi-periodic processes. A dynamic-priority preemptive policy like EDF allows to achieve better processor utilization (to execute more timeconsuming processes). The complete compilation process has been implemented in OCaml and is about 3000 code lines long. It generates C code with calls to the real-time primitives defined in the real-time extensions of POSIX [START_REF][END_REF].

Paper Outline

Sect. 2 gives an overview of the language for specifying multi-periodic systems and shows how the case study can be programmed. We then detail the compilation process. The correctness of the system is first verified by a series of static analyses (Sect. 3). We then translate the program into a set of real-time tasks (Sect. 4). The preservation of the synchronous semantics during inter-task communications is ensured by a buffering protocol described in Sect. 5. We can then translate the tasks into C code for a simple real-time platform (Sect. 6). A comparison with related works is given in Sect. 7.

A Synchronous Real-Time Language

Informal Presentation

We present the language through the programming of the Flight Control System of Fig. 1. The different operations of the Flight Control System are first declared as imported nodes, named after the initials of the operations (for instance, PA stands for "Position Acquisition"):

imported node PA( i : i n t ) returns ( o : i n t ) wcet 1 ; imported node AA( i : i n t ) returns ( o : i n t ) wcet 1 ; . . . The declaration of an imported node specifies the inputs and outputs of the node with their types and the worst case execution time (wcet) of the node. For instance, the node PA has one input i of type int, one output o of type int and its wcet is 1.

For each sub-system, we define an intermediate node that groups the operations of the sub-system. Node definitions are modular and hierarchical. There are several ways to decompose the Flight Control System into nodes and it is also possible to program the whole system as a single node. However, the different decompositions produce the same behaviour as intermediate nodes are flattened during the compilation (see Sect. 4.1). We choose to group operations by sub-systems (and by rates) for better readability. In the following, the suffix _o stands for "observed", _r for "required" and _i for "intermediate". The node for the acquisition loop is defined as follows: node a c q u i s i t i o n ( a n g l e , pos , a c c ) returns ( p o s i , a c c i , a n g l e r ) l e t p o s i = PA( pos ) ; a c c i = AA( a c c ) ; a n g l e r = FL( a n g l e ) ; t e l This node has three inputs and three outputs, the types of which are left unspecified and will be inferred by the type-checker of the language (see Sect. 3). The body of the node (the let ... tel block) is a set of equations that define how the outputs of the node are computed from its inputs. All the variables and expressions of a program are flows. For example, the constant value 0 stands for an infinite constant sequence. Nodes are applied point-wisely to their arguments. So, for instance, at each repetition of node acquisition, the output pos_i is obtained by applying node PA to input pos.

Similarly, we define a node for the piloting loop and for the navigation loop: So far, each node could be defined with the existing Lustre language as each sub-system is mono-periodic. For the main node FCS however, we use new primitives to handle rate transitions (when operations of different rates communicate) and to specify the real-time constraints of the different operations: o r d e r = p i l o t i n g ( a n g l e r / ˆ4 , a c c i / ˆ4 , ( 0 fby a c c r ) * ˆ3 ) ; ( p o s i , a c c i , a n g l e r ) = a c q u i s i t i o n ( a n g l e , pos , a c c ) ; t e l When a faster node consumes a flow produced by a slower node, we undersample the flow using operator /ˆ. e/ˆk only keeps the first value out of each k successive values of e. For instance flow acc_i is under-sampled by factor 4 as its consumer (piloting) is 4 times slower than its producer (acquisition).

For communications from slow to fast operations, we first delay the flow with operator fby. The operator fby inserts a unitary delay: expression cst fby e produces the value cst at its first iteration and then the previous values of e (ie e delayed by the period of e). We then over-sample the delayed flow with operator * ˆ. e * ˆk over-samples e by a factor k. Each value of e is duplicated k times in the result. For instance the flow acc_r is delayed and then over-sampled by a factor 3 as its consumer (piloting) is 3 times faster than its producer (navigation). We use a delay before over-sampling the flow to avoid reducing the deadline for the production of the flow. In the case of flow acc_r for instance, without a delay the deadline for NL would be lower than 40.

For now, we have only described the ratio between the execution rates of the nodes. The declaration of the node inputs simply specifies that pos_r has clock (120, 0) (ie that it has period 120 and phase 0) and all the different rates of the system are deduced from this information by the clock calculus (see Sect. 3). The declaration of output order, imposes a deadline constraint (due 15), which requires it to be produced less than 15ms after the beginning of its period, to respect some external environment constraint. Its period is left unspecified (its inferred value is 40ms). The behaviour of the new operators is illustrated in Fig. 2, in which we give the value of each expression at each repetition of the system.

Formal Definition: Strictly Periodic Clocks

In the synchronous approach, the computations performed by the system are split into a succession of instants, where each instant corresponds to one repetition of the system. The synchronous assumption requires that for each instant, computations end before the end of the instant. Computations can be activated or deactivated at different instants using clocks. Clocks define the temporal behaviour of the program on the logical time scale of instants.

To define formally the real-time operators presented in the previous section, we introduce a new class of clocks called strictly periodic clocks. Given a set of values V, a flow is a sequence of pairs (v i , t i ) i∈N where v i is a value in V and t i is a tag in N, such that for all i, t i < t i+1 . The clock of a flow is its projection on N. A tag represents an amount of time elapsed since the beginning of the execution of the program. Each value of a flow must be computed before its next activation: v i must be produced during the time interval [t i , t i+1 [. After precedence encoding, the deadline may actually be less than t i+1 , this will be detailed in Sect. 4.3.

Definition 1. ( Strictly periodic clock).

A clock h = (t i ) i∈N , t i ∈ N, is strictly periodic if and only if: ∃n ∈ N * , ∀i ∈ N, t i+1 -t i = n.
n is the period of h, denoted π(h) and t 0 is the phase of h, denoted ϕ(h).

Definition 2. The term (n, p) ∈ N * × Q + denotes the strictly periodic clock α such that π(α) = n and ϕ(α) = π(α) * p
A strictly periodic clock defines the real-time rate of a flow and is uniquely characterized by its phase and by its period. Strictly periodic clocks relate logical time (instants) to real-time. Locally, each flow has its own notion of instant (it must end before its next activation), and globally we can compare flows that do not share the same notion of instants by relating instants to real-time. We introduce periodic clock transformations to formalize such rate transitions: Definition 3. Let α be a strictly periodic clock, operations / . , * . and → . are periodic clock transformations, that produce new strictly periodic clocks satisfying the following properties:

-π(α/ . k) = k * π(α), ϕ(α/ . k) = ϕ(α), k ∈ N * -π(α * . k) = π(α)/k, ϕ(α * . k) = ϕ(α), k ∈ N * -π(α → . q) = π(α), ϕ(α → . q) = ϕ(α) + q * π(α), q ∈ Q
Rate transition operators apply periodic clock transformations to flows. If e has clock α, then e/ˆk has clock α/ . k, e * ˆk has clock α * . k and e ∼> q has clock α → . q.

Syntax

The syntax of the language is close to Lustre. It is extended with real-time primitives based on strictly periodic clocks. The grammar of the language is given in Fig. 3. A program consists of a list of node declarations (nd). Nodes can either be defined in the program (node) or implemented outside (imported node), for instance by a C function. Node durations must be provided for each imported node, more precisely an upper bound on worst case execution times (wcet). The external code provided for imported nodes can itself be generated by a standard synchronous language compiler (like Lustre), in case developers want to program the whole system using synchronous languages. The clock of input/output parameters (in/out) of a node can be declared strictly periodic (x : rate(n, p), x then has clock (n, p)) or unspecified (x). A deadline constraint can be imposed on outputs (x : rate(n, p) due n ′ , the deadline is n ′ ). The body of a node consists of an optional list of local variables (var) and a list of equations (eq). Each equation defines the value of one or several variables using an expression on flows (var = e). Expressions may be immediate constants (cst), variables (x), pairs ((e, e)), initialised delays (cst fby e), applications (N (e)) or expressions using strictly periodic clocks (epck). Values k, n, n ′ , q must be statically evaluable. Value q must be an element of Q + .

Static Analyses

Synchronous languages are targeted for critical systems. Therefore, the compilation process puts strong emphasis on the verification of the correctness of the programs to compile. This consists of a series of static analyses of the program, which are performed before code generation. The first analysis performed by the compiler is the type-checking. The language is a strongly typed language, in the sense that the execution of a program cannot produce a run-time type error. Each flow has a single, well-defined type and only flows of the same type can be combined. The type-checking of the language is fairly standard [START_REF] Pierce | Types and programming languages[END_REF]. For the example of the Flight Control System, the type-checker produces the flowing type for node FCS: (int*int*int*int)->int. This means that the node takes four integer inputs and produces one integer output. This type is inferred from the types of the imported nodes.

The causality check verifies that the program does not contain cyclic definitions: a variable cannot instantaneously depend on itself (i.e. not without a fby in the dependencies). For instance, the equation x=x+1; is incorrect, it is similar to a deadlock since we need to evaluate x+1 to evaluate x and we need to evaluate x to evaluate x+1.

The clock calculus (defined in [START_REF] Forget | A multi-periodic synchronous data-flow language[END_REF]) verifies that a program only combines flows that have the same clock. When two flows have the same clock, they are synchronous as they are always present at the same instants. Combining non-synchronous flows leads to non-deterministic programs as we access to undefined values. For instance we can only compute the sum of two synchronous flow, because the value of the sum is ill-defined when only one of the two flows is absent (when the two flows are absent the sum flow is simply absent, which is well-defined). The clock calculus ensures that a synchronous program will never access to undefined values. For the example of the Flight Control System, the clock-calculus produces the following clock for node FCS: ((120,0)*(10,0)*(10,0)*(10,0))->(40,0). This means that inputs angle, acc, position have period 10, while input position_r has period 120. The output order has period 40 (though its deadline is 10). These static analyses ensure that a program accepted by the compiler has a deterministic behaviour.

Translation into Real-Time Tasks

This section details how the compilation process translates the input program into a set of real-time tasks. We first extract a task graph from the program, where tasks are related by precedence constraints. We then encode task precedences in task real-time attributes to obtain a set of independent tasks.

Task Graph Extraction

Tasks A synchronous program consists of a hierarchy of nodes, the leaves of which are predefined or imported nodes. The task graph generation process first inlines intermediate nodes appearing in the main node recursively, replacing each intermediate node call by its set of equations. For instance, the program of the Flight Control System of Sect. 2.1 is translated into a single node (the main node FCS) containing one node call to each imported node, PA, AA, FL, PF, PL, NF, NL, one node call to operator * ˆ, one node call to operator fby and three node calls to operator /ˆ.

This "flattened" main node is then translated into a task graph. Each imported node call is translated into a task. Each variable of the node and predefined operator call is also translated into a vertex but will later be reduced to simplify the graph (see Sect. 4.1). The clustering of several nodes into the same task to reduce the number of generated tasks is beyond the scope of this paper. We could probably reuse existing strategies, for instance those suggested in [START_REF] Curic | Implementing Lustre Programs on Distributed Platforms with Real-Time Constraints[END_REF].

Task Precedences In order to respect the synchronous semantics, for each data-dependency there must be a precedence from the task producing the data to the task consuming it. Task precedences are deduced from data dependencies between expressions of the program. Similarly to [START_REF] Halbwachs | Generating efficient code from data-flow programs[END_REF], we say that an expression e ′ precedes an expression e when e syntactically depends on e ′ . This occurs either when e ′ appears in e or when x appears in e and we have an equation x = e. Let g = (V, E) denote a task graph, where V is the set of tasks of the graph and E is the set of task precedences of the graph (a subset of V × V ). For instance, the flattened Flight Control program contains the two equations pos_o=NF(pos_i/^12); pos_i=PA(pos);. These equations produce the following graph: ({NF,PA,/^12,pos,pos_i,pos_o}, {pos→ PA, PA→ pos_i, pos_i→ /^12, /^12→ NF, NF → pos_o}).

Task Graph Reduction

We then simplify the intermediate graph structure. First, each input of the main node is translated into a (sensor) task and each output of the main node is translated into a (actuator) task. Second, we remove variables from the graph, replacing recursively each pair of precedence N → x → M , where x is a local variable, by a single precedence N → M .

We finally translate predefined nodes into precedence annotations. A precedence τ i ops → τ j represents an extended precedence, where ops is a list of precedence annotations op, with op ∈ { * ˆk, /ˆk, ∼> q, fby}. op.ops denotes the list whose head is op and whose tail is ops and ǫ denotes the empty list. For instance, the precedences PA→ pos_i, pos_i→ /^12, /^12→ NF are simplified into a single extended precedence PA /ˆ12 → NF. When the rewriting terminates, every task of the graph corresponds to either an imported node or a sensor or an actuator. The reduced task graph of the Flight Control System is given in Fig. 4.

Real-Time Characteristics Extraction

Each task τ i of the graph is characterized by its real-time attributes (T i , C i , r i , d i ). τ i is instantiated periodically with period T i . It cannot start its execution before all its predecessors, defined by the precedence constraints, complete their execution. C i is the (worst case) execution time of the task. r i is the release date of the first instance of the task. The subsequent release dates are r i + T i , r i + 2T i , etc. d i is the relative deadline of the task. The absolute deadline D i [j] of the instance j of a task τ i is the release date R i [j] of this instance plus the relative deadline of the task: D i [j] = R i [j] + d i . Task real-time characteristics are extracted as follows:

-Periods: The period of a task is obtained from its clock ck i . We have T i = π(ck i ). -Deadlines: By default, the deadline of a task is its period (d i = T i ). Deadline constraints can also be specified on the production of a node output (o: due n). -Release Dates: The initial release date of a task is the phase of its clock:

r i = ϕ(ck i ).
-Execution Times: The execution time C i of a task is directly specified by the wcet of the imported node declaration. For simplification, we consider that the run-time overhead due to task preemptions is negligible.

Precedence Encoding

Simple Precedences Encoding [START_REF] Chetto | Dynamic scheduling of real-time tasks under precedence constraints[END_REF] showed that a set of dependent tasks (task related by precedence constraints) can be reduced to a set of independent ones (without precedences) obtaining an equivalent problem under the EDF policy, by adjusting task release dates and deadlines such that precedences are encoded in the adjusted real-time characteristics. The adjusted absolute deadline D * i of a task is:

D * i = min τj ∈succ(τi) (D i , min(D * j -C j )
). If we want to perform a schedulability test, the adjusted release date of a task is:

R * i = max τj ∈pred(τi) (R i , max(R * j + C j )
). If we only want to schedule the program correctly, the adjusted release date of a task R * ′ i is: R

* ′ i = max τj ∈pred(τi) (R i , max(R * ′ j )
). For simplification, we only consider the second encoding in the following.

Extended Precedences Encoding Fig. 5, shows that we can unfold extended precedences between tasks into simple precedences between task instances. The precedence encoding technique can then be applied to the "unfolded" graph.

τ i ops → τ j ⇒ ∀n, τ i [n] → τ j [g ops (n)]
, with g ops defined as follows:

g * ˆk.ops (n) = g ops (kn) g /ˆk.ops (n) = g ops (⌈n/k⌉) g ∼>q.ops (n) = g ops (n) g fby.ops (n) = g ops (n + 1) g ǫ (n) = n
The precedence relation is an over-approximation of the data-dependency relation. Indeed, there is a data dependency between τ i [n] and τ j [n ′ ], meaning that τ j [n ′ ] consumes the data produced by

τ i [n], if and only if τ i ops → τ j ∧ n ′ = g ops (n) ∧ g ops (n) = g ops (n + 1).
We can then adapt the encoding to our context. For each precedence τ i ops → τ j , we must adjust the release dates and deadlines of each instance

τ i [n] such that R * i [n] ≤ R * j [g ops (n)] and D * i [n] ≤ D * j [g ops (n)] -C j .
Concerning release dates, we can easily prove that thanks to the synchronous semantics we already have

R i [n] ≤ R j [g ops (n)]
, so release dates do not need to be adjusted. Concerning deadlines, we need to transpose the formulae to relative deadlines to fit our task model. From the definition of relative deadlines:

D * i [n] ≤ D * j [g ops (n)] -C j ⇔ d i [n] ≤ d j [g ops (n)] + r j + g ops (n)T j -r i -nT i -C j .
Deadline Calculus In practice we do not need to unfold extended precedences to perform their encoding. Instead, we represent the sequence of deadlines of the instances of a task as a finite repetitive pattern called deadline word. A unitary deadline specifies the relative deadline for the computation of a single instance of a task. It is simply an integer value d. A deadline word defines the sequence of unitary deadlines for each instance of a task. The set of deadline words is defined by the following grammar: w ::= (u) ω u ::= d | d.u. Term (u) ω denotes the infinite repetition of word u. In the following, w[n] denotes the n th unitary deadline of deadline word w (n ∈ N).

Let w i denote the deadline word of task τ i . A precedence τ i ops → τ j is encoded by a constraint relating w i to w j of the form:

w i ≤ W ops (w j ) + ∆ ops (T i , T j ) -C j + r j -r i
where, for all n, W ops (w j )

[n] = w j [g ops (n)] and ∆ ops (T i , T j )[n] = g ops (n)T j -nT i . Let ψ ops (τ j ) = W ops (w j ) + ∆ ops (T i , T j ) -C j + r j -r i .
Property 1. ∆ ops (T i , T j ) is periodic and can be represented as a deadline word. The set of deadline words is closed under operation W ops and under deadline words addition. As a consequence, ψ ops (τ j ) is a deadline word.

Proof. By induction. For instance, for the Flight Control System program, we take

C P A = 1, C AA = 1, C F L = 3, C P F = 4, C P L = 6, C N L = 20, C N F = 5.
To simplify, we take null durations for sensors and actuators. The result of the deadline calculus is: w P A = (10) ω , w AA = (5.10.10.10) ω , w F L = (9.10.10.10) ω , w P F = (9) ω , w P L = (15) ω , w N L = (120) ω , w N F = (100) ω . The deadline words of tasks AA and PA state that, each first repetition out of four successive repetitions the two tasks have a shorter deadline as PF and PL execute. Notice that if we set deadline 5 for all the instances of AA (instead of a deadline word), this example is not schedulable.

As task precedences are encoded in task deadlines, inter-task communications do note require synchronization primitives (like semaphores for instance). Indeed, as long as tasks respect their deadlines, data is produced before being consumed, so tasks simply read from and write to some communication buffers allocated in a global shared memory when they execute. However, to respect the synchronous semantics, the input of a task must not change during its execution. Therefore, we propose a communication scheme, which ensures that the input of a task remains available until its deadline.

For a precedence τ i ops → τ j , data produced by τ i [n] may be consumed by τ j [g ops (n)] after τ i [n + 1] has started. This is illustrated in Fig. 6, which shows the schedule of two tasks related by extended precedences. Vertical lines on the time axis represent task periods and marks represent task preemptions. An arrow from A at date t to B at date t ′ means that task B may read at time t ′ from the value produced by A at time t. In Fig. 6(a), 6(c) and 6(d), when A [START_REF] Benveniste | Synchronous programming with events and relations: the Signal language and its semantics[END_REF] executes, it must not overwrite the data produced by A[0] because it is consumed by B[0] and B[0] is not complete yet. Therefore, we need a buffer to keep the value of A[n] after A[n + 1] has started. In Fig. 6(b), the same data is consumed several times but A [START_REF] Benveniste | Synchronous programming with events and relations: the Signal language and its semantics[END_REF] can freely overwrite the data produced by A[0], so no specific communication scheme is required.

A A B B (a) A /ˆ2 → B A A B B B B (b) A * ˆ2 → B A A B B (c) A fby → B A A B B B CC C C C C (d) A ∼>1/2 → B, A * ˆ4 → C
Fig. 6. Communications for extended precedences

The communication protocol allocates a buffer for each extended precedence of the graph. The producer of the data writes to the buffer only if g ops (n) = g ops (n + 1) (see the definition of data-dependencies in Sect. 4.3). The consumer simply reads from this buffer each time it executes. We allocate a double-buffer when the precedence contains a fby or a ∼>, to keep the previous and the current value of the data. This communication scheme is illustrated in more details in Sect. 6.1. It is of course not optimal because in many cases when we consider a set of precedences from a single task τ i to several tasks τ j we can use the same communication buffer for some of the tasks τ j . Optimization will be treated in future work, we could for instance adapt the communication scheme proposed by [START_REF] Tripakis | Translating discrete-time Simulink to Lustre[END_REF] to our language.

Code Generation

The compiler generates C code with calls to the real-time primitives defined in the real-time extensions of the POSIX standard (POSIX.13 [START_REF][END_REF]). The code generation can easily be adapted to any real-time operating system that provides dynamic priority scheduling. Each task is translated into a thread and the threads are executed concurrently by an EDF scheduler modified to handle deadline words.

Task Code Generation

The generated code consists of a single C file. The file starts with the declaration of one global variable for each communication buffer. For instance, for the communication from PF to PL (acc_o before graph expansion), we have the declaration: int PF_o_PL_i1 (named after the output of the producer and the input of the consumer). For the communication from PL to FL, we have the declaration: int PL_o_FL_i2 [START_REF] Chetto | Dynamic scheduling of real-time tasks under precedence constraints[END_REF], as there is a delay between the two tasks.

The file then contains a function for each task of the task set. The function mainly consists of an infinite loop, that wraps the function of the corresponding imported node with the code of the communication protocol. One step of the loop corresponds to the execution of one instance of the task. Once buffer updates are complete, the function signals to the scheduler that the current task instance completed its execution so that it can schedule another task.

For instance, the function for task PL is given in Fig. 7. The value returned by the external function PL is a single integer so we can directly assign its return value to an integer variable. When the external function returns a tuple, the output value is returned as a struct pointer in the parameters of the function. The variable NL_o_PL_i3 is the communication buffer for precedence N L fby . * ˆ3 → P L. It is an array of size 2 as the precedence contains a delay. The delay is initialised at the beginning of the function. PL alternatively reads from value 1 and from value 0 of the array, starting with value 1 (NL_o_PL_i3[(instance+1)%2]). PL then copies its output value to the communication buffer PL_o_order for precedence P L → order. Instruction invoke_scheduler(0) signals the completion of the task instance. The main function then creates one thread for each task, initializes the EDF scheduler and attaches the threads to it. For instance, the thread for task PL is created by the following function call: pthread_create(&tPL,&attrPL,PL_fun, NULL). tPL is the thread created for this task. attrPL contains the real-time attributes of the task. PL_fun is the function executed by the thread. The last parameter NULL stands for the arguments of PL_fun.

Implementing EDF with Variable Deadlines

We choose to prototype the scheduler using MaRTE Operating System [START_REF] Rivas | POSIX-Compatible Application-Defined Scheduling in MaRTE OS[END_REF], which was designed specifically to ease the implementation of application-specific schedulers while remaining close to the POSIX model. We modify the EDF scheduler provided with the OS to support deadline words. To summarize, the EDF scheduler is defined as a high-priority thread created by the main function of the file. The scheduler thread is itself scheduled by the kernel of the OS. It becomes active only when scheduling actions must be taken, which is when the following scheduling events (implemented by means of signals) occur: the current instance of a task completes its execution or a new task instance is released. The scheduler then computes the most urgent task among the ready tasks (tasks released and not complete yet), resumes the execution of the corresponding thread where it stopped and suspends the execution of the currently executing thread, if any. The scheduler thread then becomes inactive until the next scheduling event.

The support of deadline words requires very few modifications. We define deadline words and modify the structure describing task real-time attributes as shown in Fig. 9. Then, we modify the function that programs the next instance of a task when the current instance completes. For a task τ i , the attributes of which are described by the value t_data, the release date and the deadline of its new instance are computed as described in Fig. 10 (D i

[n] = R i [n] + d i [n]).
The function incr_timespec(t1,t2) increments t1 by t2 and the function (t1,t2,t3) sets t1 to t2+t3.

We can see that the overhead due to the support of deadline words remains very reasonable. Altogether, we modified about 20 lines of code of the original EDF scheduler, which is 300 lines of code long. We compiled and executed the C code generated for the Flight Control System and it behaved as expected.

Related Works

The language used in this article relies on a specific class of clocks to handle the multi-periodic aspects of a system. Real-time periodic clocks have also been introduced in [START_REF] Curic | Implementing Lustre Programs on Distributed Platforms with Real-Time Constraints[END_REF], but they do not include clock transformations to efficiently handle rate transitions. Our rate-transition operators are also very similar to the rate transition blocks of Simulink [START_REF]Simulink: User's Guide[END_REF]. Yet, as far as we know, for models using such blocks, the code generation tool (Real-Time Workshop) relies on a Rate-Monotonic scheduler [START_REF] Liu | Scheduling algorithms for multiprogramming in a hard-real-time environment[END_REF] used with semaphores to handle task communications, which is not an optimal scheduling policy for this scheduling problem.

The scheduling of multi-rate Synchronous Data Flow (SDF) is a well studied problem (see for instance [START_REF] Lee | Static scheduling of synchronous dataflow programs for digital signal processing[END_REF][START_REF] Ziegenbein | Dynamic response time optimization for SDF graphs[END_REF][START_REF] Oh | Memory optimal single appearance schedule with dynamic loop count for synchronous dataflow graphs[END_REF]). In particular [START_REF] Ziegenbein | Dynamic response time optimization for SDF graphs[END_REF] studies the implementation of SDF with a dynamic scheduler using preemption. However, though multi-rate systems are at the chore of SDF graphs, SDF operations are not periodic, they are not released periodically and their relative deadline is not their period. As a consequence, these results do not apply to our problem.

[15] deals with the execution of a set of synchronous tasks, the semantics of which is very close to our task sets, with a dynamic scheduler. However, the authors do not detail how the synchronous task set is obtained, for instance how it is translated from a synchronous language, and task precedences are not specified in the task set.

A simple solution to the problem of scheduling tasks related by extended precedences is to unfold the extended precedence graph on the hyperperiod of the tasks and use [START_REF] Chetto | Dynamic scheduling of real-time tasks under precedence constraints[END_REF] to encode the simple precedences of the unfolded graph. This solution replaces each task τ i by HP/T i duplicates (where HP is the hyperperiod of the tasks) in the unfolded graph. This can lead to important computation overhead at execution as the scheduler needs to make its decisions according to a task set that will contain many tasks. Our solution does not duplicate any task, so the scheduler takes less time to make its decisions.

We proposed a language for programming critical systems with multiple real-time constraints, along with its compiler, which automatically translates a program into a set of independent real-time tasks programmed in C with POSIX.13 realtime extensions. The generated code is schedulable optimally by a slightly modified EDF scheduler and requires no synchronization primitives. Though tasks are scheduled concurrently and preemptions are allowed, the generated program respects the real-time and the functional semantics of the original program.

Fig. 1 .

 1 Fig. 1. Flight control system

  node p i l o t i n g ( a n g l e r , a c c i , a c c r ) returns ( o r d e r ) var a c c o ; l e t a c c o = PF( a c c i ) ; o r d e r = PL ( a n g l e r , a c c o , a c c r ) ; t e l node n a v i g a t i o n ( p o s i , p o s r ) returns ( a c c r ) var p o s o ; l e t p o s o = NF( p o s i ) ; a c c r = NL( p o s o , p o s r ) ; t e l

  node FCS ( p o s r : r a t e ( 1 2 0 , 0 ) ; a n g l e , pos , a c c ) returns ( o r d e r : due 1 5 ) var a c c i , a c c r , a n g l e r , p o s i ; l e t a c c r = n a v i g a t i o n ( p o s i / ˆ1 2 , p o s r ) ;

  acc_r)*^3 0 0 0 ac0 ac0 . . .

Fig. 2 .

 2 Fig. 2. Behaviour of real-time operators

Fig. 3 .

 3 Fig. 3. Language grammar

Fig. 4 .

 4 Fig. 4. Reduced task graph for the Flight Control System program

Fig. 5 .

 5 Fig. 5. Encoding extended precedences

Property 2 .

 2 The deadline words of a task graph g = (V, E) can be computed with complexity O(|V | + |E| * |w max |), where w max denotes the deadline word which has the longest size in the task graph. Proof. A reduced task graph is a DAG (when we do not consider delayed precedences), so we can compute the deadline words of the graph by performing a topological sort working backwards (starting from the end of the graph). As the complexity of a topological sort is O(|V | + |E|), the complexity of the algorithm is O(|V | + |E| * |w max |) where w max denotes the longest deadline word in the task graph.

Fig. 7 .Fig. 8 .

 78 Fig. 7. Code generated for task PL The functions for tasks FL and NL, which produce data used by PL are given in Fig. 8. Variable FL_o_PL_i1 is the communication buffer for precedence F L /ˆ4 → P L. It is updated once every 4 iterations, (update_FL_o_PL_i1[instance%4]). For precedence N L fby . * ˆ3→ P L, NL alternatively copies its output value to the value 0 and to the value 1 of the buffer NL_o_PL_i3.

Fig. 8 .

 8 Fig. 8. Code generated for tasks FL and NL

Fig. 9 .Fig. 10 .

 910 Fig. 9. Data type representing task real-time attributes d w o r d t dw = t d a t a ->dword ; t d a t a ->i n s t a n c e ++; i n c r t i m e s p e c (& t d a t a ->n e x t r e l e a s e ,& t d a t a ->p e r i o d ) ; a d d t i m e s p e c (& t d a t a ->n e x t d e a d l i n e ,& t d a t a ->n e x t r e l e a s e , &(dw . dds [ t d a t a ->i n s t a n c e%dw . w s i z e ] ) ) ; Fig. 10. Releasing a new task instance

  typedef s t r u c t dword { s t r u c t t i m e s p e c * dds ; i n t w s i z e ; } d w o r d t ; typedef s t r u c t t h r e a d d a t a {

	s t r u c t t i m e s p e c p e r i o d ;
	s t r u c t t i m e s p e c i n i t i a l r e l e a s e ;
	d w o r d t dword ;
	s t r u c t t i m e s p e c n e x t d e a d l i n e ;
	s t r u c t t i m e s p e c n e x t r e l e a s e ;
	i n t i n s t a n c e ;
	} t h r e a d d a t a t ;

⋆ This work was funded by EADS Astrium Space Transportation


Imen Tounsi
email: imen.tounsi@redcad.org

Zied Hrichi
email: dsi.zied.hrichi@gmail.com

Mohamed Hadj Kacem
email: mohamed.hadjkacem@redcad.org

Ahmed Hadj Kacem
email: ahmed.hadjkacem@fsegs.rnu.tn

Khalil Drira
email: khalil@lass.fr

Using SoaML Models and Event-B Specifications for Modeling SOA Design Patterns

Keywords: SOA Design patterns: SoaML modeling: Formal methods: Event-B method: Tool support EVENT Sending_Req partition(MessageType, Transformation Rules 2.Transformation partition(MessageType, RequestMessage}, {ResponseMessage}

Although design patterns have become increasingly popular, most of them are presented in an informal way. Patterns, proposed by the SOA design pattern community, are described with a proprietary informal notation, which can raise ambiguity and may lead to their incorrect usage. Modeling SOA design patterns with a standard formal notation avoids misunderstanding by software architects and helps endow design methods. In this paper, we present an approach that aims, first, to model message-oriented SOA design patterns with the SoaML language, and second to transform them to Event-B specifications. These two steps are performed before undertaking the effective coding of a design pattern providing correct by construction pattern-based software architectures. Our approach is enhanced with a tool supporting it. Specification results are imported under the Rodin platform which we use to prove model consistency.

INTRODUCTION

The dominant architectural style for many systems is the Service-oriented architecture (SOA), a style that is essentially based on the message exchange. This architecture offers a model and an opportunity to solve problems related to the communication and the integration between heterogeneous and distributed applications [Erl, 2009]. However these architectures are subject to some quality attribute failures (e.g., availability, reliability, and performance problems). Design patterns, as tested solutions to common design problems within a context, have been widely used to solve these weaknesses.

Patterns, proposed by the SOA design pattern community, are described with a proprietary informal notation [Erl, 2009], which can raise ambiguity and may lead to their incorrect usage. So they require modeling with a standard notation and then formalization. The intent of our approach is to model and formalize message-oriented SOA design patterns. These steps are performed before undertaking the effective coding of a design pattern, so that the pattern in question will be correct by construction. Our approach allows to reuse correct SOA design patterns, hence we can save effort on proving pattern correctness.

In this paper, we propose an approach for modeling and transforming message oriented SOA design patterns. The key idea is to model these patterns with the semi-formal Service oriented architecture Modeling Language (SoaML) and to transform them into Event-B specifications. We proceed by proposing the SOA design patterns metamodel conformed to the SoaML language. This modeling step is proposed in order to attribute a standard notation to SOA design patterns. Then we propose the transformation of design pattern models, according to transformation rules, into Event-B specifications. We import the generated specifications under the Rodin platform which we use to prove model consistency. We provide structural features of SOA design patterns in the modeling phase as well as in the specification phase. Structural features of a design pattern are generally specified by assertions on the existence of types of components in the pattern. The configuration of the elements is also described, in terms of the static relationships between them. We illustrate our approach through a pattern example "Event-Driven Messaging", proposed by the SOA design pattern community. We also present a tool supporting our approach.

The paper is structured as follows. Section 2 gives background information of some concepts used in this paper. Section 3 gives an overview of our approach. Section 4 describes our tool supporting our approach. Section 5 discusses related work. Section 6 concludes and gives future works.

BACKGROUND

In this section, we provide some background information on patterns, SoaML modeling language and Event-B method.

Design Patterns

In the field of information systems, a pattern is defined as a model that provides a proven solution to a common problem individually documented in a consistent format and usually as part of a larger collection [Erl, 2009]. Patterns can be classified relatively to their level of abstraction into three categories: architectural patterns (or architectural styles) that provide the skeleton or template for the overall shape and the structure of software applications at a high-level design [Gomaa, 2004], design patterns that encode a proven solution to a recurring design common problem of automated systems [START_REF] Ramirez | Developing and applying design patterns for dynamically adaptive systems[END_REF], and implementation patterns that provide a solution to a given problem in programming [Beck, 2007]. It is used to generate code.

SoaML

SoaML4 (Service oriented architecture Modeling Language) [START_REF] Omg | Service oriented architecture Modeling Language (SoaML) Specification[END_REF] is a specification developed by the OMG that provides a standard way to architect and model SOA solutions. It consists of a UML profile and a metamodel that extends the UML 2.0 (Unified Modeling Language).

XSLT

XSLT5 (eXtensible Styles Language Transformation) is a W3C standard that supports the XML standard. The objective of this specification is to transform XML documents into another document format. XSL is decomposed into two languages, a transformation language and a formatting language. The first one can transform an XML document into another document, while the second one can use predefined tags to represent the visual aspect of an XML document. XSLT apply the transformation written by XSL stylesheet to an XML document. In our approach, we use the XSLT language to transform SoaML diagrams into Event-B specifications.

Event-B

Event-B [Abrial, 2010] is a formal method for developing systems via stepwise refinement, based on first-order logic. The method is enhanced by its supporting Rodin Platform [START_REF] Abrial | Rodin: An Open Toolset for Modelling and Reasoning in Event-B[END_REF] for analyzing and reasoning rigorously about Event-B models. The basic concept in the Event-B development is the model which is made of two types of components: contexts and machines. A context describes the static part of a model, whereas a machine describes the dynamic behavior of a model. Each context has a name and other clauses like "Constants" to declare constants, "Sets" to declare a new data type and "Axioms" that denotes the type of the constants and the various predicates which the constants obey. It is a predicate that is assumed to be true in the rest of the model.

APPROACH OVERVIEW

The main goal of our approach is the modeling of message-oriented SOA design patterns with the semi-formal SoaML standard language, the automatic transformation of pattern diagrams to Event-B specifications and the formal verification of their correctness. Figure 3 depicts the overall approach.

After modeling design patterns, the graphical editor generates an XML file. The plug-in transforms this XML file, according to transformation rules expressed with the XSLT language, into Event-B specifications. These specifications will then be imported under the Rodin theorem prover that supports the generation of Proof Obligations belonging to Event-B models. The Rodin Platform is also used in order to check the syntax of SOA design pattern specifications as well as their correctness.

SOA Design Patterns Modeling

We provide a modeling solution for describing SOA design patterns using a visual notation based on the graphical SoaML language. Three main reasons lead to use SoaML. First, it is a standard modeling language defined by OMG. Second, it is used to describe service oriented architectures. Third, diagrams used in SoaML, allow to represent structural features as well as behavioral features of design patterns.

The SoaML metamodel extends the UML metamodel to support an explicit service modeling in distributed environments. This extension is perfectly applied to SOA design patterns modeling. We Entities, that make up the architecture of an SOA design pattern, can be either Participants or Agents . A Participant represents a subclass of Component that provides and/or consumes services. Agents extend Participants with the ability to be active (their needs and capabilities may change over time). Entities can have Ports that constitute interaction points with their environment. These Ports are related to one or more provided or required Interf aces and their types can be either Service or Request . ServiceInterfaces are used to describe provided and required operations to complete services functionality, they can be used as protocols for a service port or a request port. The communication path between Services and Requests within an architecture is called ServiceChannel , it extends the metaclass Connector.

The MessageType is used to specify information exchanged between services, it extends the metaclass DataT ype. An Attachment is a part of a message that is attached to it, it extends the metaclass P roperty. The stereotype Property extends the metaclass P roperty with the ability to be distinguished as an identifying property ("primary key" for messages).

A Capability is the ability to act and produce an outcome that achieves a result, it extends the metaclass Class. A Participant can realize zero or several capabilities with the link CapabilityRealization .

In some SOA design patterns entities are organized in various ways across many orthogonal dimensions, for example they can be organized by service layers or by physical boundaries. Catalogs provide a means of classifying and organizing elements by Categories for any purpose, they extends the metaclass P ackage and specializes the stereotype NodeDescriptor . Categories are related to Catalogs with the relation Belons to . A collection of related entities are characterized by a Category . Applying a Category to an entity by using a Categorization places that entity in the Catalog .

In this paper, we model as example the Event Driven M essaging pattern6 [Erl, 2009]. It is an SOA design pattern for inter-service message exchange. It resolves the problem of inefficient pollingbased interactions for service consumer, generated in order to obtain information about events occurrence. The solution proposed by this pattern is to introduce an event manager allowing the service consumer to set itself up as a subscriber to events associated with a service that assumes the role of publisher. So that service consumers are automatically notified of runtime service events. We specify entities of the pattern and their dependencies (connections) in the Participant diagram (Figure 3) and we specify their interfaces and exchanged messages in the ServiceInterface and MessageType diagrams respectively (Figure 4).

The Subscriber, the P ublisher and the Event-M anager are defined as participants because they provide and use services. As shown in Figure 3, the P ublisher provides an event used by the Subscriber. When the event occurs, the P ublisher automatically sends the event details to the Event-M anager, which then broadcasts the event notification to the Subscriber. Both the P ublisher and the Subscriber have a port typed with "Event". the P ublisher is the provider of the service and has a Service port. The Subscriber is a consumer of the service and uses a Request port. In this diagram, ServiceChannels are explicitly represented, they enables communication between the different participants.

« Participant » Publisher « Participant » Event_Manager «ServiceChannel» PushEM_P « Participant » Subscriber «ServiceChannel» PushS_EM « Service » : Event_Notif «ServiceChannel» « Service » : Event « Request » : ~ Event «ServiceChannel» PushP_EM «ServiceChannel» PushEM_S Fig. 3. Participant diagram
In the MessageType diagram (Figure 4) three MessageTypes are used to define information exchanged between the P ublisher, the Subscriber and the Event-M anager. These messages are "SubsReq", "SubsResp" and "EventInfo", they are used as types for operation parameters of the service interfaces. As shown in Figure 4, the P ublisher's port type is the UML interface "ProviderEvent" that has the operation "publishEvent". This operation has a message style parameter typed "EventInfo". The Subscriber expresses its request for the "Event" using its request port. The type of this request port is the UML interface "SubscriberEvent". This interface has an operation "subscribeEvent" with a parameter typed "SubsReq". The type of the Event-M anager's port is the UML interface "Notification" that has two operations "eventNotif" and "subsNotif". These operations have two message style parameters where the type of the parameters are the Mes-sageTypes "SubsResp" and "EventInfo".

R1. Architecture Entities Transformation Rule

This rule transforms entity types into new Event-B entity types. Participant names and agent names are transformed to constants. The set Entity is composed of the set of all P articipants and the set of all Agents. This is specified by using a partition in the AXIOMS clause (Entity partition).

The following algorithm shows how to transform the architecture entities. The SOA design patterns diagram editor is a tool where diagrams can be created to model patterns. Figure 5 shows the diagram editor of the SOA design patterns with an illustration of the pattern example "Event-Driven Messaging". After modeling a design pattern, the plug-in generates an XML specification describing it. The generated XML specification corresponding to the participant diagram presented in Figure 3, is depicted in follows.

Algorithm Architecture entities transformation rule

<!--=======Entities======= --> <Participant ParticipantName="Subscriber"> <Port> <RequestPort Name=": ~Event"/> </Port> </Participant> ... <!--=======Connexions======= --> <RequireInterface Origine="..." Destinataire="//@Assemblage.0"/> <RequireInterface Origine=".../@Port.0" Destinataire="..."/> ... The plug-in transforms the generated XML file, according to transformation rules expressed with the XSLT language, into Event-B specifications. These specifications can be imported under the Rodin platform to verify their correctness. Transformation rules described in section 3.2 are expressed with the XSLT language. For reasons of space, we only present the following XSLT fragment for transforming the architecture entities.

By applying transformations rules on the generated XML specifications, we obtain Event-B specifications presented in Figure 6.

CONTEXT EventDrivenM

SETS

Entity MessageType

CONSTANTS

RELATED WORK

In the literature most proposed patterns are described with a combination of textual description and a graphical presentation [START_REF] Gamma | Design Patterns: Elements of Reusable Object-Oriented Software[END_REF], some times using proprietary notations [Gregor Hohpe, 2003,Erl, 2009], in order to make them easy to read and understand. However, using these descriptions makes patterns ambiguous and may lack details. There have been many research that specify patterns using formal techniques [START_REF] Zhu | [END_REF]Bayley, 2010,Blazy et al., 2003] but research that model design patterns with semi-formal languages are few [START_REF] Mapelsden | Design pattern modelling and instantiation using DPML[END_REF].

In our research work we are interested in SOA design patterns defined by Erl [Erl, 2009]. For these patterns, there are no work that model or formally specify them. Erl presents his patterns with an informal proprietary notation because there is no standard modeling notation for SOA, but now OMG announces the publication of the SoaML language [START_REF] Omg | Service oriented architecture Modeling Language (SoaML) Specification[END_REF], it is a specification for the UML profile and a metamodel for services. So, in our work, we propose to model SOA design patterns with the SoaML standard language. After the modeling step, we propose to specify these patterns formally. Similar to [START_REF] Zhu | [END_REF]Bayley, 2010,Kim and[START_REF] Kim | [END_REF] we specify design patterns using First Order Logic, but we use a different formal method which is Event-B.

After the OMG publication of the SoaML language, some works that provide SoaML support appeared. Delegado et al. [START_REF] Delgado | SoaML Eclipse plug-in para modelado de servicios[END_REF] developed an Eclipse plug-in based on EMF and GMF that implements the SoaML standard. Modeling with this plug-in is quite heavy and we can not model a provided/required connection with SoaML. Other tools that allow modeling service oriented architectures according to the OMG standard exists like Modeliosoft [Modeliosoft, 2011] and modelDriven [ModelDriven, 2009] however, these tools do not use transformation techniques for generating formal specifications.

In this context, we proposed a tool for modeling SOA design patterns, that is not only easy to use, specific for our diagrams, and adaptable with Rodin environment but also it allows importing and exporting XML files of model that will be subsequently converted to Event-B specifications. Moreover, we use the XSLT language for the automatic transformation of our model to Event-B language.

CONCLUSIONS

In this paper, we presented an architecture-centric approach supporting the modeling and the transformation of message-oriented SOA design patterns to formal specifications. The modeling phase allows to describe SOA design patterns with a graphical standard notation using the SoaML language. The transformation phase allows to formally specify structural features of these patterns at a high level of abstraction. We proposed an Eclipse plug-in that supports our approach. More precisely, it allows the modeling of SOA design patterns and then generating the corresponding XML file. Each XML file is transformed according to transformation rules expressed with the XSLT language into Event-B specifications. These specifications are then imported under the Rodin platform. We illustrated our approach through a pattern example ("Event Driven M essaging"). In this paper, we presented structural features of design patterns, behavioral features are presented in the modeling phase with sequence diagram which are then transformed to machines in the Event-B method. Currently, we are working on defining transformation rules in order automate this phase.

Fig. 1 .

 1 Fig. 1. The overall approach

  model structural features of design patterns with Participant diagram, ServiceInterface diagram, MessageType diagram. To model these diagrams, we use the part of the SoaML metamodel presented in Figure 2. Gray classes represent abstract metaclasses and white classes represent stereotypes. In follows, we only present the base concepts that we use in the pattern modeling.

Fig. 2 .

 2 Fig. 2. SOA design patterns Metamodel

Fig. 4 .

 4 Fig. 4. ServiceInterface and MessageType diagrams

Fig. 5 .

 5 Fig. 5. SOA design patterns plug-in

http ://www.omg.org/spec/SoaML/

http ://www.w3.org/TR/xslt

http ://soapatterns.org/patterns/event driven messaging

Proof Obligations

27:

for each Participant do 28:

Write (Participant.Name) 29:

end for 30: end if 31: if exist Agent then 32:

Write('Agent partition (Agent,') 33:

for each Agent do 34:

Write (Agent.Name) 35:

end for 36: end if 37: end

R2. Connections Transformation Rule

In the SoaML modeling, a ServiceChannel is a connection between two architecture entities. This rule define the graphical connection with an Event-B relation between two entities (ServiceChannel) and transforms ServiceChannels name into constants in the CONSTANTS clause. The set of Ser-viceChannels is composed of all ServiceChannel's name. This is transformed formally to a partition (ServiceChannel partition). This rule also generates Domain and Range axioms for each service channel to define its source and its target. The following algorithm shows how to transform a service channel.

Algorithm Connections transformation rule

TOOL SUPPORT

Our approach is enhanced by an Eclipse plug-in based on its development on the Frameworks; GMF (Graphical M odeling F ramework) [START_REF] Eclipse | Graphical Modeling Framework[END_REF], EMF (Eclipse M odeling F ramework) [START_REF] Steinberg | EMF: Eclipse Modeling Framework 2.0[END_REF] and GEF (Graphical Editing F ramework) [Eclipse, 2010a]. It is a graphical modeling tool that ensures an easy and efficient modeling way of SOA design patterns. Several diagrams are available in the plug-in; we can model P articipant diagram, Service Interf ace diagram, and M essage T ype diagram.