D Müller

Accelerated Simply Periodic Task Sets for RM Scheduling

Keywords: rate-monotonic scheduling, partitioned multiprocessor scheduling, sufficient schedulability test, Sr, DCT

. They have already shown the advantage of Sr and DCT over the Liu/Layland (LL) and the Burchard (Bu) bound in terms of sensitivity. First, the article compares Sr and DCT as well with other uniprocessor scheduling criteria, both theoretically and empirically. Next, these tests are applied to MP scheduling. Theory is followed by a case study and an empirical investigation with randomised task sets. Related approaches are thoroughly examined and summarised in a scheme where the central role of ASPTSs becomes obvious.

The article shows that Sr and DCT provide a very good trade-off between maximizing the scheduling test sensitivity (no unnecessary hardware) and minimizing the test's computational complexity (towards real-time decisions on schedulability).

Introduction

Scheduling in computing deals with assigning jobs to processors. Often, equal jobs have to be executed periodically, especially in embedded real-time systems. Then, the periodic task model applies, where jobs are instances of a task. Each task is specified by a period, a (relative) deadline, an execution time and a phase. Jobs are released periodically in accordance to their task's period. All jobs must be completed no later than the respective absolute deadline which is the release time plus the relative deadline. In the most typical case, the (relative) deadline equals the period and the phase is zero. Then, only two parameters characterizing each task remain: period and execution time. A necessary condition for schedulability is that the utilization, the sum of the ratios between execution time and period of all tasks, is not greater than the number of processors. Often it is much more difficult to provide sufficient or even necessary and sufficient conditions for schedulability. The goal of scheduling is to assign as many tasks as possible to the available processors, or, closer to praxis, to minimise the number of necessary processors for a given task set. So, the economic objective is to minimise necessary CPU resources, and, thus, to minimise hardware costs. Rate-monotonic scheduling (RMS) is a widely applied scheduling policy for the periodic task model on uniprocessor systems. It enables the scheduling of real-time tasks with a processor utilization of at least 0.69. Often, much higher utilizations of 0.88 [START_REF] Lehoczky | The rate monotonic scheduling algorithm: Exact characterization and average case behavior[END_REF] or even above 0.90 are possible. RMS is the optimal static-priority scheduling scheme where task priorities are assigned fixedly over the entire scheduling. The rule of RMS is the shorter the task's period the higher the task's priority. Schedulability analysis deals with necessary, sufficient, or necessary and sufficient criteria for the determination whether a task set is schedulable or not. The only known necessary and sufficient criteria are simulation along the entire hyperperiod of the task set and Time Demand Analysis (TDA) [START_REF] Lehoczky | The rate monotonic scheduling algorithm: Exact characterization and average case behavior[END_REF]. Both methods involve a computational complexity beyond O n 2  which is too expensive in many situations. Thus, sufficient criteria have been developed in order to obtain partial results much more quickly. The best-known procedure is the Liu/Layland criterion with only linear complexity but a bad performance. Frequently, a false negative answer is given using such a simple test. In that, the Liu/Layland test is a much too pessimistic one ignoring most of the data provided by the respective task set. Later on, improved linear computational complexity criteria like the Hyperbolic Bound [START_REF] Bini | A hyperbolic bound for the rate monotonic algorithm[END_REF] or the Burchard criterion [START_REF] Burchard | New strategies for assigning real-time tasks to multiprocessor systems[END_REF] have been developed. At the other end of the scale, quadratic computational complexity criteria like Critical Task Sets [START_REF] Chen | Utilization bound revisited[END_REF] and the Pillai/Shin criterion [START_REF] Pillai | Realtime dynamic voltage scaling for low-power embedded operating systems[END_REF][START_REF] Krishna | Real-Time Systems[END_REF] evolved which are sufficient ones, too. The advantage of them is that they provide high performance and, thus, are good approximations of a TDA in many situations. In 1997, Han and Tyan [START_REF] Han | A better polynomialtime schedulability test for real-time fixed-priority scheduling algorithms[END_REF] presented criteria Sr and DCT with complexities O n log n and O n 2  with very good performance (sensitivity or true positive rate). They are underrepresented in literature and deserve a thorough investigation. This will be provided by extensive comparisons (tables and charts) both of theoretical and practical (empirical) nature. Finally, a multiprocessor RM scheduling case study will be delivered.

It will be shown that DCT is the best known O n 2  sufficient criterion for RM schedulability on a uniprocessor. Sr behaves slightly worse, but has the advantage of an only linear-logarithmic complexity.

Hence both procedures are cost-effective. It turns out that DCT as a greedy algorithm to find an accelerated simply periodic task set with a utilization not greater than one is better on the average, while the non-greedy algorithm Sr can outperform DCT in rare cases. Such an example is discussed.

Next, amazing interrelationships between different uniprocessor schedulability criteria will be uncovered. This systematization will stress the central role of ASPTSs in this context. It will be thoroughly explained why using transformations of task sets is the method of choice for a decision on schedulability.

In most cases, the used transformation is an acceleration, i.e., to shorten the periods while maintaining the execution times of the individual tasks, respectively. Here, besides simply periodic task sets, roots and fundamental frequencies of the periods of the task play an important role and serve as transformation goals. Partitioned RM multiprocessor scheduling 1 is strongly based on heuristics since an exhaustive search turns out to be infeasible even for a small number of tasks. A combinatorial explosion is the reason. The approach is characterised by a suitable combination of a Bin Packing heuristic and a uniprocessor schedulability test. A combination of First Fit with Sr or DCT will turn out to be superior to other known RM MP scheduling heuristics in terms of minimizing the number of processors required to schedule a given task set. This is both performed with a task set from a problem posed by Jane Liu as exercise 9.3 in [START_REF] Liu | Real-Time Systems[END_REF], p. 390 and randomly generated task sets. The adequate generation of random task sets is crucial for the informational value of performance ratios. So it would be wrong to take only chains of multiples as periods since this is a very special configuration and not general enough. Thus, special care will be devoted to the random generation of task sets.

As an outlook on future research, the combination of different uniprocessor schedulability tests and the investigation of runtime behaviour of the compared criteria will be suggested. The latter one is important since a purely theoretical comparison of the complexities may not be appropriate to praxis. Here, behaviour with a lower number of tasks and the operations necessary to execute per step are important, too, for runtime evaluations. This goes up to worstcase execution time (WCET) analysis which is a cornerstone of real-time analysis.

1 The alternative is global scheduling. Here, the optimal algorithms PFAIR and LLREF are better in theory (worst case), ignoring runtime overhead [START_REF] Cho | An Optimal Real-Time Scheduling Algorithm for Multiprocessors[END_REF][START_REF] Baker | Comparison of empirical success rates of global vs. partitioned fixed-priority and EDF scheduling for hard real time[END_REF][START_REF] Kato | Semipartitioned Scheduling of Sporadic Task Systems on Multiprocessors ECRTS '09[END_REF].

Methodology

System model

There are given n pre-emptive, independent, period- ic real-time tasks T ={T 1 , T 2 , .. , T n } with T i = p i ,e i  where p i is the period and e i is the execution time. The deadline is assumed to be equal to the period, i.e., ∀ i : p i =d i . Additionally, ∀ i : 0e i ≤ p i should hold. The individual utiliza- tions u i =e i / p i sum up to the total utilization u= ∑ i=1 n u i . The challenge is to schedule these tasks on a set of m identical processors P={P 1 , P 2 , .. , P m } . The task priorities, denoted by Prio i , shall be assigned statically and in a rate- monotonic way, the shorter the period the higher the priority. Equal period ties are broken arbitrarily, but fixed 2 . Further, we restrict our considerations to the simplest case of partitioned schemes which doesn't allow any migration. The last two restrictions imply that we consider a (1,1)-restricted MP scheduling according to the terminology introduced in [START_REF] Carpenter | A categorization of real-time multiprocessor scheduling problems and algorithms[END_REF]. The remaining problem is to map tasks to processors where they can be scheduled following the ratemonotonic uniprocessor scheduling, respectively. We will consider only off-line algorithms where all task parameters are initially known. There are two approaches concerning the number of processors. First, this number m can be fixed, and we obtain a decision or feasibility problem whether the task set can be feasibly scheduled. On the other hand, the minimization problem with the objective m  min for a given set of n tasks could be raised. We will focus on the minimization problem.

Two scheduling elements

A strict distinction between the allocation algorithm and the uniprocessor schedulability condition is suggested. Both of them contribute to the performance as well as to the complexity of the heuristics. In general, a trade-off between the complexity and the performance can be expected.

Allocation algorithm

The problem is related to the Bin Packing Problem.

Here, the task is to find an m -partition of a set of n items so that the sum of item sizes in each bin is bounded by a constant. The decision problem, cf. [START_REF] Lehoczky | The rate monotonic scheduling algorithm: Exact characterization and average case behavior[END_REF] is beside simulation the only necessary and sufficient condition for RM schedulability. One has to check for a fixed point of the iteration of processing time demand which must be not greater than the deadline of the task (1), a computationally beneficial iterative method given by Audsley et al. [START_REF] Audsley | Applying new scheduling theory to static priority pre-emptive scheduling[END_REF]. Of course, this has to be done for all tasks as the example { 5, 2  , 7, 4

t i l 1 =e i  ∑ j : Prio j  Prio i ⌈ t j l p j ⌉ e j t i 0 =e i ∀ i ∃l :t i l1 =t i l ≤ p i =d i (1)
TDA has a pseudo-polynomial time complexity. More precisely, it can be given as O rn 2  where r =max p i / min p i ( [START_REF] Liu | Real-Time Systems[END_REF], p. 137).

Pillai/Shin criterion (PS): Pillai and Shin [START_REF] Pillai | Realtime dynamic voltage scaling for low-power embedded operating systems[END_REF][START_REF] Krishna | Real-Time Systems[END_REF] suggest to adapt TDA to obtain a lower-complexity, only sufficient condition. The iteration (1) considers the entire interval [0 ; d i = p i ] for each task as it looks for the fixed point which is the (worst case) processing time demand of the task. As a pessimistic approach we consider the maximum number of preemptions by a higher priority task. This is the period ratio rounded up. Multiplying it with the execution time of the particular higher priority task and summing up over all such tasks gives (2).

∀ i : e i  ∑ j : Prio j Prio i ⌈ p i p j ⌉ e j ≤ p i =d i (2) Computational complexity is O n 2  .
Liu/Layland criterion (LL): Liu and Layland gave in their classical paper [START_REF] Liu | Scheduling algorithms for multiprogramming in a hard-real-time environment[END_REF] a sufficient upper bound of RM schedulability depending only on the number of tasks to schedule [START_REF] Burchard | New strategies for assigning real-time tasks to multiprocessor systems[END_REF].

u≤n  n  2-1= L n  (3)
Two minor mistakes in the proof were detected and corrected by Devillers and Goossens [START_REF] Devillers | Liu and layland's schedulability test revisited[END_REF]. Time complexity is linear since utilization has to be summed up over all tasks. Liu/Layland limit criterion (LLconst): In order to make this a constant as it is required for a complete analogy to the Bin Packing Problem, cf. 2.3, the infimum

limit of L(n) is considered (4). u≤ln  2 (4)
Again, time complexity is linear. Hyperbolic Bound (HB): Instead of considering only the total utilization u , it might be a good idea to in- clude the individual utilizations u i [START_REF] Bini | A hyperbolic bound for the rate monotonic algorithm[END_REF]. This approach resulted in condition (5), which is better than LL. The more heterogeneous the utilizations are distributed, the better is the sensitivity of the criterion.

∏ i=1 n u i 1≤2 (5)
Computational complexity is linear. Burchard criterion (Bu): Following [START_REF] Burchard | New strategies for assigning real-time tasks to multiprocessor systems[END_REF], we define

S i =log 2 p i -⌊ log 2 p i ⌋
for each task and build

=max S i -min S i If 1-1/ n the condition is u≤n-12  n-1 -12 1- -1=B n ,  (6)
else, i.e., ≥1-1/ n , the condition is just (3).

It has been shown that B n , ≥ L  n always holds. In that way, Bu is better than LL. Time complexity is linear. RBound: In 2003, Lauzac et al. [START_REF] Sylvain Lauzac | An improved rate-monotonic admission control and its applications[END_REF] proposed a new criterion. In order to apply it, the task set has to be transformed first using an algorithm called ScaleTaskSet which transforms T into T0 by stretching each period and execution time by an appropriate power of 2. The goal is to have all new periods between half the maximum period and the maximum period. ScaleTaskSet includes a sorting by periods in non-decreasing order, but this step is not necessary for the criterion itself. Then, we define

r =max p ' i -min p ' i ( 7
)
The condition is then u≤n-1r

1 n-1 -1 2 r -1 (8)
Time complexity is linear and not log-linear as stated in [START_REF] Sylvain Lauzac | An improved rate-monotonic admission control and its applications[END_REF] since the sorting in the original algorithm can be substituted by a min-max search loop. Only these values are evaluated in the further algorithm and the definition of r .

Critical Task Sets (CTS): Chen et al. [START_REF] Chen | Utilization bound revisited[END_REF] proposed a transformation of the periods to a critical task set following the ideas of Liu and Layland in their proof of the LL bound [START_REF] Liu | Scheduling algorithms for multiprogramming in a hard-real-time environment[END_REF]. First, the periods are sorted in non-decreasing order. Next, incremental subsets starting from 2 up to n periods are considered. Such a subset is then transformed according to

p ' j = p j ⌊ p i p j ⌋ (9)
with i as the outer loop index and j as the inner loop index. This results in a maximum period ratio no larger than 2 . Then, the construction of a critical task set based on [START_REF] Liu | Scheduling algorithms for multiprogramming in a hard-real-time environment[END_REF] with a calculation of the improved utilization bound is possible.

(10) The utilization must be no larger than the minimum of the critical task set utilizations of the incremental subsets and (from the necessary condition)

1 . Com- putational complexity is O n 2  .
Summary and Anticipation: In order to give a summary we provide a comparison of the different uniprocessor schedulability conditions in Table 1 including an anticipation (printed in italics) of our proposed conditions introduced later in Section 3.

Special task sets

Accelerated task sets

A task set T ={T

O rn 2  (all)
Table 1: RMS uniprocessor schedulability conditions, r defined in ( 7)

u≤min  {  ∑ j =1 i-1 p' j1 -p ' j p ' j   2p ' 1 -p' i p ' i |i=2..n } ∪{1}  ∀ i , j ∃c i , j∈ℕ: max { p i , p j } min { p i , p j } =c (11)
The intention behind extracting such special task sets is to fit every task completely into all tasks which have a larger period. Note that, e.g., the task set {3, 1 , 6, 1 , 9, 1} is not simply periodic although there is a great regularity in the periods. Obviously, 9 is not an integer mul- tiple of 6 . The pattern behind with a step-wise in- crease by the minimal period is only appropriate for task sets of size 2 . We can repair the fault and ob- tain {3, 1 , 6, 1 , 12, 1} as a valid example for a simply periodic task set. On the other hand, one could be tempted to restrict the pattern to { a⋅b i , e i } with b∈ℕ . It is obvious that a =1.5 and b=2 in the previous valid example.

In general, a ratio c i , j=b

|i-j| must be an integer following that construction. Considering a task set like {3, 1 , 15, 1 , 30, 1} which doesn't fit into the above given pattern clarifies that the approach was too restrictive. Relaxing the condition we can state the following lemma: Lemma 1 (Characterization of simply periodic task sets)

A task set T ={T 1 , T 2 , .

. , T n } is simply periodic if and only if an (index-dependent) integer ratio exists for all direct neighbours in the non-decreasingly ordered list of task periods.

A proof in forward direction is easy since the ratio is directly given by definition [START_REF] Holte | The pinwheel: a real-time scheduling problem[END_REF]. Assuming a non-integer ratio between two task periods leads immediately to contradiction to definition [START_REF] Holte | The pinwheel: a real-time scheduling problem[END_REF]. In backward direction, we have to construct the period ratio between two arbitrary periods and to show that this ratio is always an integer. The ratio is the product of all neighbour ratios along the unique path from minimum to maximum period. Since ℕ is closed under multiplication, it is indeed a non-negative integer. A test based on Lemma 1 is O n log n . Sorting is the dominating step, the check for integer ratios is only of linear complexity. It turns out that the pattern {a⋅b i , e i } can be re- garded as a special case with a constant neighbouring period ratio of b . The misleading thought in the first attempt was the assumption that there should be a constant integer-additive relationship between neighbouring periods, but it has to be a variable integer-multiplicative one. The second approach is -in that terminology -a constant integer-multiplicative one and too specific.

Intuitively, it might be clear that the zero cut-off property mentioned in the beginning of this subsection enables for a rate-monotonic scheduling without idle processor time which lifts it to the same performance as EDF scheduling under maintenance of its simplicity. This fact is expressed in the following theorem.

Theorem 2 (RMS on a simply periodic task set)

A system consisting of a single simply periodic task set is schedulable by RMS if and only if u≤1 .

A proof sketch is given in [START_REF] Liu | Real-Time Systems[END_REF], p. 129f.

ASPTSs: Sr and DCT

As the naming already suggests, an ASPTS has to be conform to both conditions (3.1 and 3.2) at the same time. Such a s ways exists to a given task set, but is not unique. Lemma 2 (Accelerated simply periodic task set)

For an arbitrarily given task set T ={T 1 , T 2 , .. , T n }

, there always exists an ASPTS. It is not unique. This can be shown easily by construction.

T '={T ' 1 , T ' 2 , .. , T ' n } with ∀ i : p' i =inf i { p i }
fulfils the conditions since all periods are not increased and a common period means an integer ratio of 1 for all possible pairs. A straightforward step is it to combine Theorems 1 and 2 to our main theorem: Theorem 3 (RM schedulability of ASPTSs)

In order to show RM schedulability of a given task set T , it is sufficient to show that there is an acceler- ated simply periodic task set T ' with u ' ≤1 .

A proof is given in [START_REF] Han | A better polynomialtime schedulability test for real-time fixed-priority scheduling algorithms[END_REF]. Theorem 3 as a sufficient condition offers a new way to prove RM schedulability as suggested by [START_REF] Han | A better polynomialtime schedulability test for real-time fixed-priority scheduling algorithms[END_REF][START_REF] Han | Distance-constrained scheduling and its applications to real-time systems[END_REF]. It suffices to look for ASPTSs and to minimise the total utilization. The new test is then given by [START_REF] Xiaobo (sharon | Fast performance prediction for periodic task systems[END_REF].

∃T ' ={T ' 1 ,T ' 2 ,.. , T ' n }: ∑

i=1 n e ' i p ' i ≤1

subject to ∀ i : p ' i ≤ p i ∀ i : e ' i =e i and (11) [START_REF] Xiaobo (sharon | Fast performance prediction for periodic task systems[END_REF] Note that the test can be cancelled as soon as a transformed task set with a feasible utilization is found. If there is such a u ' ≤1 , the original task set is schedulable by RM, if not we cannot make a claim on schedulability by RM 3 . For the purpose of finding candidate ASPTSs with low utilizations, two algorithms coined Sr and DCT 4 were proposed in [START_REF] Han | A better polynomialtime schedulability test for real-time fixed-priority scheduling algorithms[END_REF][START_REF] Han | Distance-constrained scheduling and its applications to real-time systems[END_REF]. Sr is a specialization described as well in [START_REF] Liu | Real-Time Systems[END_REF], p. 414ff. and has its origin in pinwheel scheduling [START_REF] Holte | The pinwheel: a real-time scheduling problem[END_REF]. While Sr accelerates to a task sets obeying the pattern {a⋅b

i , e i } with b=2 (discussed in 3.2), DCT

3 Of course, this can be checked by TDA or a scheduling simulation both of which are exact (necessary and sufficient) tests. 4 Sr means Specialization with respect to r which is further explained in [START_REF] Han | Distance-constrained scheduling and its applications to real-time systems[END_REF]. DCT probably means Distance-Constrained Tasks. Definitely, it has nothing to do with the Discrete Cosine Transform known from signal and image processing.

uses individual ratios according to p ' j = p i / ⌈ p i p j ⌉ and p ' i = ⌊ p i p j ⌋ p j for p i  p j which are the locally optimal transformations. This greedy approach will be discussed in 3.4. The computational complexity of tests based on these two algorithms is O n log n and O n 2  . Sr uses a sorting 5 and precalculation of partial sums which enables for an iterative calculation of utilizations avoiding a double loop with complexity O n 2  . This is further explained in [START_REF] Han | A better polynomialtime schedulability test for real-time fixed-priority scheduling algorithms[END_REF] and [START_REF] Han | Distance-constrained scheduling and its applications to real-time systems[END_REF]. For a better understanding of the two algorithms, see example in Table 2. The best results can be obtained using a combination of both algorithms. A task set is marked RM schedulable if one of both algorithms Sr and DCT is able to find a task set T ' with u ' ≤1 . The complexity of this approach, coined Sr ∨ DCT , is O n 2  .

Theoretical Performance of Sr and DCT

Theorem 4 (Theoretical Performance Sr/DCT)

A test based on Sr is better than LL and better than Bu since each task found to be RM schedulable by LL or by Bu can also be found to be schedulable by Sr [START_REF] Han | A better polynomialtime schedulability test for real-time fixed-priority scheduling algorithms[END_REF][START_REF] Han | Distance-constrained scheduling and its applications to real-time systems[END_REF]. DCT is necessary and sufficient for the case of n=2 [START_REF] Han | A better polynomialtime schedulability test for real-time fixed-priority scheduling algorithms[END_REF].

There are task sets not passing LL or Bu tests but Sr as will turn out by example in Section 4, so the first part describes a proper relationship. The second part of the theorem makes DCT equivalent to TDA in the case of n=2 . Note that this results in another ad- vantage over the compound algorithm Rate Monotonic Tasks (RMGT) [START_REF] Burchard | New strategies for assigning real-time tasks to multiprocessor systems[END_REF] which uses Rate Monotonic Small Tasks (RMST) [START_REF] Burchard | New strategies for assigning real-time tasks to multiprocessor systems[END_REF] based on a simplification of Bu for small tasks and TDA for large tasks. Such a quite complicated heterogeneity in testing is no longer necessary by using DCT. It can be shown that DCT is equivalent to the necessary and sufficient test given as Theorem 32.9 in [START_REF] Sudarshan | Approximation algorithms for scheduling time-critical jobs on multiprocessor systems[END_REF]. The condition for schedulability with n=2 and p 1 ≤ p 2 is given there as

e 2 ≤ ⌊ p 2 P 1 ⌋  p 1 -e 1 max { 0, p 2 -⌊ p 2 P 1 ⌋ p 1 -e 1 } (13
) This interrelationship stresses the prime importance of the given approach. As an example, we test the schedulability of task sets of the kind {5,e 1  , 7, e 2 } . The possible pairs of e 1 and e 2 resulting in a schedulable task set can be visualised graphically, see Figure 1.

5 Sorting is O n log n .
The filled region denotes the solution set. The linear function e 2 =5-e 1 represents the utilization limit if the second task is accelerated to a period of 5 . Second, the first task could be accelerated to a period of 3.5 resulting in an acceleration limit of e 2 =7-2 e 1 . Since the existence of one ASPTS suffices according to Theorem 3, a union of both triangles gives the solution set. Note further that the PS bound (2) only considers e 2 ≤7-2 e 1 as con- straint omitting the other possibility e 2 ≤5-e 1 in the OR term. Thus, the dark grey region represents task sets detected schedulable by DCT but not by PS, characterizing DCT superior to PS. For n=2 , DCT is always equal to or better than PS since the PS constraint is relaxed by an additional OR term. Finally, we want to point out that DCT pursues a greedy strategy when constructing the accelerated task sets. It will turn out that this approach is (in the average case) superior to the more restricted one only using the simply periodic task pattern { a⋅b i , e i } introduced in 3.2 where, additionally, b=2 , which corresponds to Sr. Anyway, there are rare cases where the greedy DCT is worse than Sr. An example is the task set {2,1 , 11,2 , 17,4 } , see Table 2

Case study

As a first test, we want to apply the suggested approach to a problem raised as exercise 9.3 in [START_REF] Liu | Real-Time Systems[END_REF], p. 390. Ten asks with parameters given in Table 3 shall be scheduled on a multiprocessor system. The obvious question is for the minimal number of processors necessary. Following the sub-tasks given by [START_REF] Liu | Real-Time Systems[END_REF], p. 390 both with FF-LL and RMST, a number of processors of m=4 is obtained. This is not the optimal number of m=3 . Clearly, with a total utilization of u≈2.47 , a schedule with only two processors is impossible. By running the heuristics, it turns out that only FF-TDA, FF-DCT, FF-PS, FF-CTS and FF-Bu 7 achieve the optimal number of 3. All other approaches find the sub-optimal solution of m=4 .

Here, the border line runs almost exactly between the O n and the higher complexity methods. Only the more complex criteria and Bu are able to obtain the optimal value of m=3 . This suggests strongly 6 We can also consider other bases than b=2 for the specialization. The average performance becomes worse [START_REF] Sudarshan | Approximation algorithms for scheduling time-critical jobs on multiprocessor systems[END_REF], but in rare cases, they can be better. Note that, e.g., { Further investigations shall consider the number of partitions leading to a schedulable configuration found by the different heuristics. The most general approach giving exactly the possible partitions and so the optimal number of processors, too, is to combine the exact methods of both scheduling elements, cf. 2.2. Thus, a brute-force search with TDA will be the reference. The number of cases to consider is the 10th Bell number which is 115975 , cf. 2.3. This is possible with a today's computer in a reasonable amount of time. Anyway, we want to limit the search space and then compare the performance of the different algorithms in the specified parts of the search space. Since we already know that the optimal value is m=3 , this part close to the border of impossibility to schedule is the most interesting one. There are still S 10,3=9330 possibilities, cf. 2.3. Among them, we want to consider three combinations of numbers of tasks assigned to each of the three processors: 4-3-3 , 4-4-2 and 5-3-2 . They contain 2100 , 1575 and 2520 cases, respectively.

In Table 4, a comparison of the different uniprocessor schedulability conditions in relationship to TDA as the reference is given. Performance has to be seen as sensitivity or true positive rate.

Table 4: Performance of different uniprocessor schedulability conditions on a set of ten tasks

Clearly, the conditions Sr ∨ DCT , DCT, Sr, CTS and PS outperform all other conditions significantly. Among them, the combination of Sr and DCT, which requires the highest effort, delivers the best performance in the most typical 4-3-3 case. But the ad- vantage is only marginal, so using DCT might be sufficient. In the exotic cases 4-4-2 and 5-3-2 , CTS and PS outperform the suggested approaches. This is interesting, but should not be overvalued since the sample size is very small. Remarkable is the breakdown of almost all known only sufficient conditions in the particularly difficult case 5-3-2 . An exception is PS which detects 7 of 9 correct partitions. It can be seen as an outlier. Results in Section 5 will deliver more evidence.

Simulation with randomised task sets

In the following, we will present two simulation results, one for uniprocessor scheduling and one for multiprocessor scheduling. An important step in both cases is the generation of random task sets. The core of such a function is pseudo random number generation. In order to obtain a uniform distribution it is wrong to use a modulo operator since this operation restricts the result to only the lower value bits. Instead, scaling by division should be used.

Uniprocessor

Tasks are randomly given an integer execution time in [1,10] (uniform). The period results from adding an integer uniform distribution in [1,100] to the execution time. The target is n=10 and u=0.70..0.96 . So, the total utilization is incremented in steps of 0.02 . If the target utilization is reached or sur- passed with less than 10 tasks this set will be omit- ted. Otherwise, the execution time of the 10th task is reduced in order to reach the respective target utilization exactly. 10,000 task sets exactly meeting the requirements for n and u are checked for each u , where for u=0.96 only 100 task sets are checked. The reason is that it is much more unlikely that they are RM schedulable. The results can be seen in Figure 2.

We can see that higher utilization task sets are more difficult to recognise as schedulable. This is true for all investigated uniprocessor schedulability conditions. The slight increase from 0.94 to 0.96 is not significant since the sample size of 100 , see above, is not convincing. Note that LL breaks down already right above u=0.70 since the limit 10 2 1, compared to LL. So, for low utilizations PS is worse than the linear complexity LL condition. On the other hand, CTS includes a guarantee, but exhibits worse behaviour compared to DCT or Sr. Sr shows a good performance related to its computational complexity of O  n log n .

Multiprocessor

For the multiprocessor case, the target utilization is 2.5 . In order to enable this, the period results here from adding an integer uniform distribution in [1,30] to the execution time. For all criteria, FF was used as allocation algorithm. In the cases of Bu and RBound, a processing of the task set has been conducted before applying FF. For Bu, tasks are sorted by the S values, cf. 2.4.6, in non-decreasing order. For RBound, the procedure ScaleTaskSet, cf. 2.4.7, including a sorting of the transformed set with non-decreasing periods is applied. Such a preprocessing further improves the performance of the algorithms being opponents to the new ones, and, thus, makes the competition even harder. The value m is the result of the minimization prob- lem. 100,000 task sets have been checked by each heuristic, respectively. Figure 3 shows the results.

Note that the m value of 5 occurs so rarely that it is almost invisible in the bars CTS, PS, HB and LL. Clearly, again the three new heuristics based on the new criteria outperform the established ones significantly. While they peak, together with the exact uniprocessor schedulability condition, at m=3 , the oth- er ones peak at m=4 . This means that they would waste an entire processor in most cases. Again, Sr ∨ DCT has no great advantage compared to DCT itself. Thus, we recommend to use DCT.

Related Work

Sr and DCT are underrepresented in literature. While the article by Zapata and Alvarez [START_REF] Zapata | EDF and RM multiprocessor scheduling algorithms: Survey and performance evaluation[END_REF] not even mentions the great work of Han and Tyan, Lauzac et al. [START_REF] Sylvain Lauzac | An improved rate-monotonic admission control and its applications[END_REF] shortly discuss their approach, but claim that "[..]SRFF is always between that of RMFF and RBound[..]" [START_REF] Sylvain Lauzac | An improved rate-monotonic admission control and its applications[END_REF] and then no further consider it. Zapata et al. came in [START_REF] Zapata | Comparative analysis of real-time scheduling algorithms on one processor under rate monotonic[END_REF] to the result that DCT and Sr yield the best performance among all sufficient tests they investigated.

In [START_REF] Kuo | Efficient online schedulability tests for realtime systems[END_REF], Kuo et al. claim to have found a polynomialtime schedulability test with higher performance and efficiency. The idea is to use the number of roots instead of the number of tasks in the LL formula. A task is called a root if there is no other process with a larger period that is an integer multiple of the original period. There are task sets for which their so called Root-Based test recognises schedulability where all other tests collapse. But the problem is that this is only possible for very artificial task sets as they have been used in their "simulations". Only in case of task sets with a single root the bound becomes 1.0 . In all other cases, it is almost as bad as LL since the most typical number of roots is close to the number of tasks itself. E.g., for the task set given in Section 4, there are 9 roots. Thus, the Root- Based test with O n 2  complexity [15] is in the aver- age case much worse than the proposed tests. An illustrative example is the task set 〚5,2 , 7,4  ,35,1〛 . At first, it seems to be RM schedulable since there is one root and utilization is exactly one. The problem is that the precondition in Theorem 4 in [START_REF] Kuo | Efficient online schedulability tests for realtime systems[END_REF] is not fulfilled. The algorithm has to be done in an iterative or recursive manner. In the example, the middle priority task doesn't meet its deadline. On the other hand, this property makes the approach suitable for on-line schedulability [START_REF] Kuo | Efficient online schedulability tests for realtime systems[END_REF]. Similarly, Kuo and Mok [START_REF] Kuo | Load adjustment in adaptive real-time systems[END_REF] suggested a schedulability condition based on the number of fundamental frequencies. In the division graph, which is the Hasse diagram induced by the half order relationship p i |p j , it coincides with the number of fundamental chains. Again, this number is then put into the LL formula. An algorithm finding the number of fundamental frequencies with a complexity of O n 5/2  is given in [START_REF] Kuo | Load adjustment in adaptive real-time systems[END_REF] provement to O n 2  complexity in [START_REF] Chen | Utilization bound revisited[END_REF] with the additional advantage that their Algorithm 2 can obtain a smaller k value if a root is smaller than a leaf. The problem is that these algorithms result in a high sensitivity only for sets with just one fundamental frequency. Note that this means a simply periodic task set which corresponds to a very restricted part of the parameter space. The common problem of the criteria based on the number of roots or the number of fundamental frequencies [START_REF] Kuo | Load adjustment in adaptive real-time systems[END_REF][START_REF] Kuo | Efficient online schedulability tests for realtime systems[END_REF] is that they do not transform the task set and so remain too specific. Thus, they are not able to reach good average sensitivity on random task sets. The argument of the authors that harmonic rates are typical e.g. for multimedia processes [START_REF] Kuo | Efficient online schedulability tests for realtime systems[END_REF] trivialises the problem. A configuration with just one harmonic chain can be detected without any advanced algorithm in most cases. As a consequence, it might be a good idea to combine the basic idea of the Root-Based test with a transformation to accelerated task sets. But it turns out that in case of assuming only one root, which is then the task with the longest period, such a "test" would not be sufficient. The reason is that deadline violations in RMS can not only occur in the lowest priority task. Instead, all tasks 8 have to be checked for possible deadline violations in the accelerated task set with only one root. This leads directly to PS, see T i corresponds to a root task. The denom- inator p i / ⌈ p i p j ⌉ is the reduced period of the appro- priate accelerated task T j and is closely related to the term used in DCT for shorter period tasks. The difference is that in DCT, the shortening is applied iteratively while here, it is applied related to the root task. This becomes apparent by again considering the task set {2,1 , 11,2 , 17,4 } given in 3.4. It will be accelerated to {17/ 9,1 , 8.5,2 ,17,4}

with a utilization of exactly 1 and, thus, T 3 experi- ences no deadline violation. Here, T 2 is not distorted by T 1 since it can be accelerated to {11/6,1 , 11,2 } with a utilization less than 1 . Thus, not only Sr, see 3.4, but also PS is able to detect {2,1 , 11,2 , 17,4 } as RM schedulable. So, PS is closely related to DCT which highlights the central role of ASPTSs.

8 The only exception is the highest priority task which always will be scheduled at the beginning of its period.

∀ i :e i  ∑ j : Prio j  Prio i e j p i

⌈ p i p j ⌉ ≤1 ⇔ ∀ i : e i  ∑ j : Prio j Prio i ⌈ p i p j ⌉ e j ≤ p i =d i (14)
The so called Algorithm 3 by Chen et al. in [START_REF] Chen | Utilization bound revisited[END_REF] with a complexity of O n 3  is an improvement of CTS. As a preprocessing, periods which are integer divisors of other periods and other ones fulfilling an advanced condition are eliminated. According to [START_REF] Zapata | Comparative analysis of real-time scheduling algorithms on one processor under rate monotonic[END_REF], the performance of this algorithm is in the range of DCT and Sr, but it can outperform them only in case of small maximum task utilizations ≤0.5 . A serious draw- back is the high complexity. Often, a TDA will be preferable. Similar to CTS, Park et al. [START_REF] Park | A generalized utilization bound test for fixed-priority real-time scheduling[END_REF] gave a linear programming (LP) approach in order to obtain a task set specific utilization bound, too. A total utilization below the LP bound means that at least one of the constraints must be violated. Hence, for a single decision on schedulability, it is sufficient to test all given constraints. A sole violation entails schedulability of the task set. By not finding such a violation, nothing can be said on feasibility. The criterion is sufficient but not necessary. The approach is closely related to PS. The set of constraints could be reduced by Hu and Quan [START_REF] Xiaobo (sharon | Fast performance prediction for periodic task systems[END_REF]. They claim that their best algorithm

Figure 4: Relationships between different uniprocessor scheduling criteria

can outperform DCT for larger values of n . But they have to admit that DCT is much better in terms of running time, ca. one order of magnitude in their tests. Their constraints correspond to a generalization of PS. Instead of only checking with the period p i of the incremental lowest priority task, acceler- ated periods ⌊ p i p j ⌋ p j are tested, too. Finally, all oth- er tasks are accelerated related to the accelerated lowest priority task. The idea of the Root-Based test is exploited as done in PS. Since PS is O n 2  and the extension is an additional loop over tasks, this approach has a computational complexity of O n 3  , and is, thus, not a direct competitor of DCT or Sr. E.g., the schedulability of the task set {2,1 , 11,2 , 17,4 } given in 3.4 can be detected with their LP approach. It accelerates the set to {2,1 , 8,2 , 16,4 } as Sr does. Thus, the approach seems to be conceptually interesting and reaches a very good performance at the price of much higher complexity and running times than Sr/DCT. In the case of n=2 , it turns out to be equivalent to DCT and, thus, to be a necessary and sufficient criterion. LP can be seen as filling a gap between PS and TDA. Summing up, see Figure 4.

Conclusions

We came to the result that DCT is the best known O n 2  sufficient criterion for RM schedulability on a uniprocessor. Our simulations suggest that multiprocessor scheduling heuristics based on Sr or DCT outperform all other heuristics under investigation. With a computational complexity of O n log n and O n 2  , the criteria are less complex than TDA which is pseudo-polynomial. On the other hand, they are more complex than classical criteria with linear complexity. A serious competitor is the Critical Task Set test. Anyway, it turned out to be worse than Sr and worse than DCT. The Pillai/Shin test with a complexity of O n 2  like DCT provides no guarantees at all and exhibits in most cases a worse sensitivity than DCT. In a concrete run-time comparison, DCT is often faster than the linear complexity criteria RBound or the Burchard criterion since they include several loop cycles, making the constant belonging to O n high, and use expensive operations like power and logarithm extensively. This is also true for Sr. Thorough investigation of runtime behaviour could be dealt with in future research. Interrelationships between ASPTSs and the concepts of the Root-Based test and the Pillai/Shin test have been pointed out. The connection between the LP approach of Hu and Quan, DCT, and the Root-Based test has been given explicitly. An extensive study of related work has shown that a lot of approaches are closely related to ASPTSs.

DCT delivers an outstanding performance at a reasonable practical run-time. Additionally, DCT provides a necessary and sufficient criterion for task sets of size n=2 making it as powerful as TDA in this particular case. Last but not least, the principle behind DCT, taking one period as a pivot and constructing a harmonic set by shortening (if necessary) all other periods, is well understandable and can be applied even by humans and not only by computers for smaller values of n . Its elegance strongly sug- gests a higher influence on teaching.

A further improvement can be achieved by combining different tests. Here, Sr ∨ DCT lead to only very little´gain, not paying off the increased effort. The combinations PS ∨ DCT (similar to the LP approach by Hu and Quan [START_REF] Xiaobo (sharon | Fast performance prediction for periodic task systems[END_REF]) and CTS ∨ DCT might be more promising since the concepts behind are less similar. This could be a matter of future research.

A combination of the new tests with the FF policy leads to new powerful MP scheduling heuristics. They can reach results close to the optimum. This suggests that the algorithms Sr and DCT are still better suitable for multiprocessor scheduling.

Acknowledgement

The author acknowledges the contribution of his colleagues to this work.

  2,1 ,  20,2 , 55,20} can be detected schedulable by Sr with b=3 , but neither by Sr nor by DCT. So, consecutive tests with different bases can improve the result. On the other hand, the gain might be low and not worth the effort in most cases. 7 Note that FF-Bu is an improved version of RMST since it uses the Bu criterion in its original form instead of the simplified one used by RMST.

	that it is worth not only to use linear complexity
	heuristics in MP scheduling.
	i 1 2 3 4 5 6	7	8	9	10
	p i 7 21 29 49 64 66 160 235 260 450
	e i 2 3 9 15 20 16 32 72 25 120

Table 3 :

 3 Parameters of 10 periodic tasks for multiprocessor scheduling

  Best sensitivity delivers Sr ∨ DCT . But the improvement compared to pure DCT is marginal and doesn't pay off the higher effort. So, DCT turns out to be the condition of choice. Note that both CTS and PS as the other conditions with O n 2  complexity besides DCT reach medium sensitivity. Anyway, a serious drawback of PS is its lack of a guarantee, cf. Table

	cases.
		100,00%	Sr+DCT
		90,00%	DCT
		80,00%	Sr CTS
		70,00%	PS Bu
	sensitivity	40,00% 50,00% 60,00%	RBound HB LL
		30,00%
		20,00%
		10,00%
		0,00%
		0.70 0.72 0.74 0.76 0.78 0.80 0.82 0.84 0.86 0.88 0.90 0.92 0.94 0.96
		utilization

1/10 -1 is between 0.70 and 0.72 . All three newly proposed conditions are better than the established ones in all

Figure 2: Performance of different uniprocessor schedulability conditions on randomised sets of ten tasks; 10,000 simulations per u value; Sr + DCT curve is only slightly above the DCT curve

  by Kuo and Mok. Chen et al. gave an im-

	100%
	90%
	80%
	70%
	60%
	50%
	40%
	30%
	20%
	10%
	0% 5 4 3	TDA	Sr+DCT	DCT	Sr	CTS	RBound	Bu	PS	HB	LL
	Figure 3: Results of the MP scheduling minim-
	ization problem (value of m) for randomised
	task sets with u = 2.5 and n = 10 using FF with
	different uniprocessor schedulability condi-
	tions; Bu and RBound apply a preprocessing
	concerning the order of the tasks

Glossary

ASPTS: Accelerated Simply Periodic Task Set BF:

Best Fit Bu:

Burchard (criterion) CTS:

Critical Task Sets DCT:

Distance-Constrained Tasks FF:

First Fit HB:

Hyperbolic Bound LL:

Liu/Layland (criterion) LLconst: Liu/Layland limit criterion LP Linear Programming MP:

Multiprocessor NF:

Next Fit PS:

Pillai/Shin (criterion) RBound RBound criterion RM(S): Rate-monotonic (scheduling) RMFF Rate Monotonic First Fit RMGT Rate Monotonic General Tasks RMST Rate Monotonic Small Tasks Sr:

Specialization with respect to r TDA: Time Demand Analysis WCET: Worst Case Execution Time WF:

Worst Fit


R Adeline

J Cardoso

P Darfeuil

S Humbert
email: sophie.humbert@turbomeca.fr

C Seguin

Toward a validation process for model based safety analysis

Keywords: Model Based Safety Analysis, validation, formal model, AltaRica

Today, Model Based Safety Analysis processes become more and more widespread to achieve the safety analysis of a system. However and at our knowledge, there is no formal testing approach to ensure that the formal model is compliant with the real system. In the paper, we choose to study AltaRica model. We present a general process to well construct and validate an AltaRica formal model. The focus is made on this validation phase, i.e. verifying the compliance between the model and the real system. For it, the proposed process recommends to build a specification for the AltaRica model. Then, the validation process is transformed to a classical verification problem between an implementation and a specification. We present the first phase of a method to verify the compliance between the model and the specification.

Introduction

Model-Driven Engineering (MDE) is a methodology which aims to base the development of a system on the creation, the refinement and the integration of models. MDE was created to increase productivity by, for example, simplifying the design or promoting communication between the different teams working on a same project. If at the beginning, MDE was focused on the development of software systems, its applications are nowadays more spread and deal for example with the achievement of safety analyses. Thus, where MDE is generally focused on the automatic generation of code (e.g. C, C++), Model Based Safety Analysis (MBSA) aims to provide a model to automatically perform classical safety analyses such as Fault Tree Analysis (FTA) or Failures Modes and Effects Analysis (FMEA) ( [START_REF] Villemeur | Reliability Availability Maintainability and Safety Assessment[END_REF]). Concerning this MBSA, several works ( [START_REF] Joshi | Model-based safety analysis final report[END_REF]) propose to assess the safety of systems by allowing simulation, the automatic generation of fault trees or searching automatically failure scenarios leading to undesired events. Amongst all the languages, we have chosen to use AltaRica which was designed to formally describe the functional and dysfunctional behaviour of a system. In a general way, the process to study the behaviour of a model can be divided into three main parts: • Modelling activity. System components and their behaviours are described in an adapted formal language. Methodologies and guidelines can be written to give rules and best practices. These guidelines aim at both helping the model design and encouraging the reusability of models (by , for example, standardizing information implemented in the model);

• Validation of the model. This step ensures that the model is a valid abstraction of the real system (correct hypotheses and same behaviours). Without this step, the next one can be useless; • Verification of the specification. We check that the model holds the system's specifications.

In this paper, we deal with the second point. Indeed, although the problem of validation of AltaRica models is not well address in the literature, this validation seems to be essential in order to check if safety analyses are generated from erroneous or incomplete models.

The paper introduces the first steps of a validation process for AltaRica models. Section 2 presents an overview of the classical safety analysis process.

With showing some limits of this kind of analyses, we present the motivation for the use of MBSA. Then, the AltaRica language is described in section 3. Sections 4 to 7 are devoted to the presentation of the validation process for AltaRica models. In the sections 6 and 7, the work is focused on the unit validation, i.e. the validation of the AltaRica component library. Finally, last section presents a conclusion of our work and futures works.

From classical safety analysis to MBSA

Definitions

Before describing the classical safety analyses, some definitions, strongly inspired from [START_REF]ARP4754: Certification considerations for highly integrated or complex aircraft systems[END_REF], are introduced.

• Failure: the inability of an item to perform its intended function. • Failure condition: Condition with an effect on the system and its users, caused by one or several failures. It depends on both operational and environmental conditions. • Failure mode: the way in which the failure of an item occurs.

Classical safety analyses

Safety engineering ensures that the safety requirements (extracted from international standards) are held by the system considering all potential failure modes of each component. In this purpose, safety studies aim to define the safety requirements and then ensure that the system fulfils its required properties. In industrial practice, we can distinguish the following types of safety analyses.

• Assessment of qualitative requirements. The objective is to demonstrate that no combination of events with less than N individual failures leads to the failure condition (N depends on the severity of the failure condition). • Assessment of quantitative requirements. The objective is to compute the occurrence probability of failure condition.

To perform the safety analyses, safety engineers traditionally use the Failure Modes and Effects Analysis (FMEA) and the Fault Tree Analysis (FTA) ( [START_REF] Villemeur | Reliability Availability Maintainability and Safety Assessment[END_REF]). Building a FMEA consists in identifying all the potential failure modes of each system component and analysing their local and global effects on the system.

A FTA is a top down approach which illustrates the way in which low level component failures or events contribute to the global system failure condition. Thus, an FTA begins with a defined failure condition and breaks it down into basic failure modes identified in the FMEA. One strong advantage of the FTA is its simple formalism. After doing the breaking down, the FTA become a logic gate network. In this network, the failure condition is described by a logic equation from which we can extract failure scenarios. From this logic equation, it is even possible to compute the occurrence probability of the failure condition during the considered mission.

Toward Model Based Safety Assessment

Although FMEA and FTA are classical methods, several limits can be seen.

• The size and the complexity of current industrial systems grow. They become highly reconfigurable and performing the identification of failure scenarios without model can be error prone;

• Because a fault tree describes only one failure condition, it can be heavy to build all fault trees for all failure conditions; • In case of modification of the system, several fault trees would have to be updated; • Even if the formalism of fault trees allows an easy computation of qualitative and quantitative results, this formalism is different from the representation of the system. The fault trees can be difficult to read for someone outside the safety domain, especially when the number of terminal events is important. We think these limits can be overcome by performing the safety analysis activities on formal model of the system under development. Instead of building one fault tree for each failure condition, we provide a formal model describing both the nominal system behaviour and the dysfunctional behaviour of the system. On this model, several failure conditions can be studied. The failure scenarios as well as the FTA could be automatically generated.

Figure 1 : The two approaches 2.4 Toward a rigorous process for MBSA So, MBSA can help to tackle several limits shown by the classical approach. But, today, the modelling process of these formal models is based, as for the classical approach, on informal sources. Indeed, FMEA and FTA are based on informal sources such as regulations (for the identification of failure conditions and requirements), design documents and field experience. Thus, they are highly dependant on the skill and also on the interpretation of safety engineers in charge of the analysis. Moreover, the validation process of FMEA and FTA is mainly based on 1) the verification by experts that no failure mode is forgotten in the FMEA, 2) that the effect of the failure modes are well described and 3) that all failure scenarios are considered in the FTA. Thus, validation process remains a mere proofreading and is all but formal.

Design Documents Safety Interpretation

Classical approach

Today, the same report can be made about the model based approach. To solve this problem, the paper presents a global process for the rigorous AltaRica modelling of a system. The focus is made on the validation of these AltaRica models.

The AltaRica language

Amongst all the languages available in the literature to perform MBSA, we have chosen to use AltaRica [START_REF] Point | Contribution à l'unification des méthodes formelles et de la sûreté de fonctionnement[END_REF], a formal modelling language, developed at LaBRI to describe both functional and dysfunctional behaviour of a system. It allows representing the failure propagations in an industrial system. The language is carried out by the tool Cecilia™ OCAS (for example) which provides a graphical interface to design models and allow analysing them by different ways such as simulation, automatic generation of minimal cuts (i.e. shortest scenarios leading to the failure condition) or sequences (i.e. ordered cuts). AltaRica language is hierarchical and compositional. Each component is described by a mode automaton [START_REF] Rauzy | Mode Automata and their compilation into fault trees[END_REF]. The basic unit to model a system component is called a "node" and is composed with three different parts: 1) the declaration of variables and events; 2) the definition of transitions; 3) the definition of assertions.

Each component has a finite number of flow variables and state variables. Flow variables are the inputs and the outputs of the node: they are the links between the node and its environment. State variables are internal variables which are able to memorize current or previous functioning mode (for example, failure mode). In our models, these variables (flow and state) are either Boolean or enumerated. Then, each node owns also events which modify the value of state variables. These events are phenomenon such as a failure, a human action or a reaction to a change of one input value. The transitions describe how the state variables are modified. They are written such as "G(s,v) |-E ->s_" where G(s,v) is a Boolean condition on state s and input variables v, E is the event and s_ is the effect of the transition on state variables. If the condition G is true, then event E can be triggered and state variables are modified as described in s_. The assertions describe how output variables are constrained by the input and state variables.

These concepts are illustrated by the following example. This component has one input and one output variables both ranging over the domain {ok, low, null}, one state variable ST ranging over the domain {ok, degraded, lost} and two events Degradation and Fail. At the initial instant, the node is in state "ok". The event Degradation (respectively Fail) describes a failure which leads the node into the state "degraded" (respectively "lost"). "Degradation" (respectively "Fail") can be triggered only if the node is in state "ok" (respectively in the state "ok" or "degraded"). The assertion means that the output value is equal to the input one if the node is in state "ok". The output value is equal to "low" if the state is "degraded" and the input value is "ok". In every other case, the output value is "null". To build the model of the global model, several nodes are interconnected. Thus, failures are propagated via nodes by their inputs and outputs. Failures can also be propagated by synchronizations which simulate the failure of several components at the same time. Hierarchy of nodes can be used to model complex components and build the model of the global system. Once the global model is obtained, the AltaRica model allows analysing failure condition. Different tools can calculate, for example, minimal cut sets or the occurrence rate of a failure condition.

Validation in literature

Validation of classical safety analyses is mainly based on several proofreadings (by engineers and/or experts). Based on formal models, we believe that the new approach can benefit from a more elaborated validation process. A lot of works aim at ensuring that a formal model meets a given specification ( [START_REF] Bogdanov | Statechart testing method for aircraft control systems[END_REF], [START_REF]Formal methods for test sequence generation[END_REF]). Such a work is used to verify that the real system (pictured by the model) meets its specification and its requirements. But one strong hypothesis under this kind of work is that the model behaviour is in accordance with the behaviour of the real system… which is, according to us, far from obvious! Thus, we believe that it is essential to verify that the two behaviours (model and real system) are coherent before verifying that some properties are hold by the model. Testing compliance between a specification and the model is dependant from both the specification form and the model language. The following of this section presents two techniques extracted from literature to verify the compliance of the model with the real system.

Step-by-step simulation

For the validation of the model, one of the most overwhelmed methods is based on the step-by-step simulation of the model. This method ensures, for tested scenarios, that the model behaves as the real system. Nevertheless, this method is not perfect.

• Due to its nature, this method is not exhaustive.

Indeed, an exhaustive simulation is often not feasible (at human scale) due to the large number of scenarios playable by the model. system. But some difficulties; described above, can be highlighted.

• Properties can be difficult to find and to formalize by engineers and experts; • For a property, the model-checker provides only one counter-example. Typically, the kind of property verified on the formal model is properties that the real system has to hold. For example, we can verify that no single failure leads to the loss of the system. But for our application, we will have to verify properties that the real system holds. So identifying properties needs a great experience and an excellent knowledge of the system and its behaviour. For AltaRica language, previous works have developed a platform between AltaRica and the model checker SMV [START_REF] Kehren | Advanced Multi-System Simulation Capabilities with AltaRica[END_REF].

A validation process

High level view of the process

MBSA is clearly a promising approach to overcome limits shown by classical safety analyses. But, to use MBSA in industrial domain, we believe that it's very important to have a method of validation of the model. For this purpose, we envisage two major phases: 1) guiding the modelling phase to prevent some errors and 2) validating the models to detect and eliminate remaining errors. The first subject is not the point here. Details can be found in [START_REF] Adeline | Toward a methodology for the AltaRica modelling of multi-physical systems[END_REF]. Here, the focus is done on the validation phase of an AltaRica model. According to us, a high level view of the general validation process can be pictured as below.

Figure 2 : High level validation process

Validation process proposal

We introduce in this part a general method for the three levels of validation described above (unit, integrated and global). The general strategy of this method is to: Modeling Methodology (Not the focus here)

Validation of the AltaRica unit nodes library

Validation of a unit node integrated in the model

Validation of the global model

• Build a schematic representation of the system under study (this representation will play the role of a specification); • Verify that the AltaRica model is compliant with this representation. Thus, we transform the validation problem of an AltaRica model into a "classical" verification problem between a specification and an implementation. In the following, we call SFPM (Specification of Failure Propagation Model) the specification of the AltaRica model and AIFP (AltaRica Implementation of the Failure Propagation model) the implementation of the AltaRica model. At this moment, the careful and cautious reader won't do any assumptions on the form of the SFPM. Indeed, according to us, the form of the SFPM will be different depending on the level of validation (unit, integrated and global). The proposed process can be divided into two steps: Concerning the SFPM:

• Define the SFPM from informal documents;

• Define the coverage criteria of the SFPM. What do we want to test on the SFPM? (the criteria will differ depending on the form of the SFPM and the goal of the validation); • From both the SFPM and its coverage criteria, we generate test cases which cover these criteria.

Concerning the AIFP: To well understand this process let us explicit two particular points of uncertainty in the process. First the SFPM might not be complete (i.e. it might not contain all of the real system's behaviour). Indeed, this SFPM arises from human work and might not contain all possible execution path of the AIFP. So, giving coverage criteria on the SFPM, generating test cases and playing them on the AIFP give confidence in the methodology but are not sufficient. AIFP can embed more information and more behaviours than the SFPM; some of them are true, some other are wrong behaviour and have to be detected and annihilated. Giving coverage criteria on AIFP prove that the model has been "sufficiently" tested. One other advantage of testing AIFP is that we can possibly complete the SFPM afterwards.

We believe that this general process can be applied and adapted to each kind of validation (unit, integrated and global). Depending on the validation level, parts of the process will change; in particular, the form of the SFPM will be different, different coverage criteria will be defined. In the following, our work has been focused on the unit validation (i.e. the validation of an AltaRica node). In a general way and to justify the existence of SFPM, we consider that building a first representation of the component's behaviour (even if it is incomplete but was validated by the experts) is a prerequisite to build the AltaRica node and help at its validation.

6.1: SFPM Requirements

Before dealing with the form and the chosen formalism for this SFPM, we present three major requirements for this SFPM.

• The SFPM should depict correctly the real component behaviour; • The SFPM has to be understandable by experts;

• The SFPM should be as formal as possible.

Concerning the first point and according to previous section, the SFPM is a critical point for the validation of AltaRica models. Indeed, as a specification, the SFPM is the reference of the AltaRica model, i.e. if the SFPM contains errors, the AltaRica model will contain errors too. Thus, the SFPM should be a correct depiction of the real system behaviour. About the second point and because the SFPM have to be validated by experts, the SFPM needs to be written down in an easily understandable form. About this point, we agree that validating the SFPM by a mere expert proofreading is rather strange. However, we believe that having a schematic representation of the system is a prerequisite to build and validate the AltaRica model. Moreover, the focus is made here on the unit validation, i.e. the validation of a component of the AltaRica model. So, the size of the SFPM will be limited and, for the expert, easier to validate than the global AltaRica model.

The last requirement is that the SFPM has to be as formal as possible. Indeed, SFPM is the starting point for the generation of test cases. To allow a systematic generation of these test cases, having a formal (at least a semi-formal) description of the SFPM will be useful.

Taking into account these three requirements, the following subsection proposed a form for this SFPM.

6.2: SFPM building

To build this SFPM, a variety of methods / formalisms can be found in literature to picture and formalize the behaviour of a system. This includes, for example, decision tables (which output for which inputs?), Petri networks, Markov chains, Finite State Machines, UML diagrams, mode automata. The general purpose of this SFPM is to be a kind of bridge between informal documents (design documents, safety analysis or / and failure analysis documents) and the AltaRica model. For practical reasons and because of the AltaRica language, we choose, a Mode Automata like form. We are conscious that it is irrelevant to ask an analyst for a complete mode automaton. We suppose here that the analyst can write little parts of mode automata and existing tools can compute these parts into a complete mode automaton. To achieve that, we propose to:

• Model the inputs / outputs of the component with a block diagram; • Model the states and transitions with a classical state -transition UML diagram; • Add to this state-transition diagram the assertions, i.e. the value of the outputs depending on the state and the input. The assertions will be written as ITE (If Then Else).

On the Figure 4, (a) is the block diagram describing the inputs, the outputs and their types. On the example, the inputs and the outputs are enumerated.

The figure (b) describes the three states "Ok", "Degraded" and "Lost" of the automaton, the transitions "Fail" and "Degradation", and the value of the output in each state. Two remarks can be made:

• If a guard of a transition depends on the value of one or several inputs, the state -transition diagram will picture input change as transition, • A state of the automaton won't be automatically pictured by one AltaRica state variable. Here, we will use one AltaRica state variable with three values {Ok, Degraded, Lost}. We believe that these kinds of diagrams are sufficiently clear, explicit and comprehensible to be validated by experts. Taking the hypothesis that we can transform these diagrams into a mode automaton, these diagrams will be considered as a reference (i.e. a specification) for both the implementation of the component model (modelling activities) and the validation of the implemented model. Thus, our problem can be considered as a classical problem of verification that an implementation is correct with respect to its specification.

6.3: AIFP building

From the SFPM, the AIFP is manually built. Concerning our example, the SFPM represented on Figure 4 corresponds to the AltaRica model presented in section 3.

Verification of the AIFP

At this stage, we have at our disposal the SFPM and the AIFP. We want now to validate the AIFP according to the process described in section 5.

7.1: SFPM and AIFP coverage criteria

First, we have to define the objectives of the verification. So, we must define what we want to test on both SFPM and AIFP, i.e. the coverage criteria on SFPM and AIFP. SFPM coverage: On the SFPM, the coverage criteria are:

• the coverage of all states;

• the coverage of all transitions;

• the coverage of the assertions. For the assertions and because they are written under "If Then Else" form, we can choose classical coverage criteria of the DO178B [START_REF]B / ED-12: Software considerations in airborne systems and equipment certification[END_REF]. Here, we choose the Condition / Decision coverage.

AIFP coverage: Defining coverage criteria for the AIFP consists in defining criteria for an AltaRica model. Our coverage criterion is to cover the transitions and the assertions of the AltaRica model. About the transitions, let us remind that AltaRica transitions are written under the form "G(s,v) |-E ->s_". We transform this form into "If (G(s,v) and E) then s_". The meaning is identical. But, written under "If Then Else" form, we can apply classical coverage criteria defined in DO178B. We choose the condition / decision coverage:

• Condition coverage: a condition is a simple Boolean expression, i.e. it can not be broken down into a simpler Boolean expression; the condition coverage means that each condition has to be evaluated to both true and false. • Decision coverage (or branch coverage): the entire Boolean expression has to be evaluated to both true and false. The AltaRica assertions are written under "If Then Else" form. So again, we can apply coverage criteria of the DO178B. We choose also the condition / decision coverage.

7.2: Preliminary for AIFP verification

Here, we want to directly measure the effectiveness of the test strategy on the AltaRica model. We present thus a way to measure the coverage of the model by introducing flags into the model.

Measure of the coverage of the AltaRica transitions:

To measure the coverage of the AltaRica transitions, we follow the following step. For it and in the previous subsection (during the simulation of test cases extracted from the SFPM), the analyst has checked for the activation of the flags ST_T_i and ST_A_i. Here, we suppose that the analyst in charge of the verification knows the list of all defined flags, i.e. he knows all defined ST_T_i and ST_A_i. So, our objectives here are the followings:

• Analysing which parts of the AIFP are not tested by the test cases extracted from the SFPM; • Generating test cases to cover these parts. About the first point, the analyst knows the list of all existing flags and the list of already activated flags (by the tests extracted from the SFPM).

So, identifying the list of non-activated flag (the list of untested parts of the AIFP) is trivial. Then, for each non-activated flag, we use the sequence generator tool of Cecilia™ OCAS to identify scenarios which activate these flags (for each flag, we obtain a list of scenario which activates this flag). Then, we choose the minimal list of scenarios which activates all non-activated flags. This minimal list corresponds to the test cases set. Then, for each of these test cases, we play it on the AIFP (i.e. on the AltaRica model) and we observe the output and the state transfer. Here, to know if they are correct, our reference is an expert judgement.

In a general way and all along the process, if an error is detected, we have to check if the error is due to the SFPM or the AIFP. If it is due to the AIFP, we update the AIFP and have to play again the test cases extracted form the SFPM (and following step). If the error is due to the SFPM, the SFPM has to be updated and the total process has to be re-started. According to us, when we have no errors at the end of the process, the validation of our AltaRica node is finished.

Conclusion

In this paper, we outlined several important aspects of the design process of an AltaRica model (and more generally of a formal model). Amongst these aspects, the most important are 1) having a specification model and 2) transform the validation problem into a verification problem between the implementation and the specification. The first point, not presented in details in the paper, consists in transforming a design from an informal description into a detailed and formal (at least semiformal) specification usable for both the modelling and validation activities. The second point, which is the subject of the paper, is to check that the implementation (i.e. the AltaRica model) is consistent with this specification. Coverage criteria are given and a process is described to generate automatically test cases which cover (with respect to the defined coverage criteria) the AltaRica model. However, we argued that validation of AltaRica model is needed but we base this validation on a specification model validated by experts. Works will be described in [START_REF] Adeline | Toward a methodology for the AltaRica modelling of multi-physical systems[END_REF] to present a process for the modelling activities which can be an input for a rigorous building of this specification. Also and for future study, a rigorous way to transform the specification into the implementation could be considered.

Figure 3 : A proposal for the validation process 6 .

 36 Figure 3 : A proposal for the validation process6. Construction of the SFPMIn this section, we deal with the definition and the building of the Specification of Failure Propagation

Figure 4 :

 4 Figure 4 : Proposal for the SFPM

  Simulation of the test cases on the AIFP: Once these test cases obtained, we simulate them on the AIFP. It consists in checking if the actual output is the expected one (defined in the SFPM) and if after each transition, the state transfer is correct. To achieve this task, a great help is given by the step-by-step simulation tool of Cecilia™ OCAS. Indeed, thanks to this tool, every state and every output are observable. So checking for correct output and correct state transfer is a very easy task.

	• We add an integer local variable named LOC
	with the same form of the output variable:
	"LOC = case { A: 1,
	B: 2,
	else 3}"	If an error
	• We add to the AltaRica model one boolean state variable ST_A_i per assertion	occurred (wrong output / wrong value of a variable state), the model is updated and tested again. When
	• We initialize them to "false" • We add one transition for each assertion: "LOC=i and ST_A_i=false |-Dirac(0) → ST_A_i=true" where Dirac(0) is an instantaneous event	no error is claimed by the verification, we can go further on the process. Moreover, during the simulation, we check, on the AIFP, for the potential activation of the flag ST_T_i and ST_A_i.
	• We add an observer to the AltaRica model. The observer is true if all ST_A_i are true: that	Verification of the AIFP: AIFP coverage
	means that all assertions have been covered.	Previous subsection has tested the AIFP according
		to SFPM coverage criteria. The objectives were to
	7.3: Verification of the AIFP	discover missing states, transitions or assertions in the AIFP (with respect to the SFPM). Here, our
	The first objective is to verify that the AIFP satisfies	objective is to detect extra states, transitions or
	the properties of the SFPM. According to the SFPM	assertions in the AIFP. Potentially, these extra
	coverage criteria (cf. 7.1); it consists in detecting, in	information can be wrong (i.e. errors in the AIFP), or
	the AIFP, missing states, transitions or assertions	true (i.e. errors in the SFPM).
	presents in the SFPM.	• We transform AIFP transitions according to the
	The second objective is to verify that there is no	condition coverage of the DO178B, i.e.
	unwanted information in the AIFP. According to the	transforming "A or B |-E → s_" into two
	AIFP criteria, it consists in detecting extra	transitions "A |-E → s_" and "B |-E → s_". Thus,
	states, transitions or assertions in the AIFP.	each transition has a unique condition, i.e. the
		guard of each transition can not be broken into a
		simpler Boolean expression;
	Verification of the AIFP: SFPM criteria	• We add to the AltaRica model one Boolean state
	For verifying the properties of the SFPM on the	variable ST_T_i per modified transition;
	AIFP, the first step is to generate a set of test cases that satisfies the SFPM coverage criteria. Then, those test cases are simulated on the AIFP.	• We initialize them to "false"; • We transform transition such as: "A |-E → s_ & ST_T_1:=true"
		"B |-E → s_ & ST_T_2:=true";
	Generation of the test cases: From the SFPM, we generate automatically test cases. Written as mode automata, our approach uses different works of the literature ([4], [5]).	• We add an observer to the AltaRica model. The observer is true if all ST_T_i are true. That means that all transitions have been covered.
	The general principle of our approach is:	Measure of the coverage of the AltaRica assertions:
	• Use the state-transition diagram of the SFPM (of	To measure the effective coverage of the AltaRica assertions, we follow the following step.
	the mode automata) to generate a first set of test cases which cover all states and transitions. • Use the assertion part of the SFPM to complete	• We transform AIFP assertions according to the condition coverage of the DO178B, i.e. transforming:
	the first set of test cases in order to cover the assertions. For it, we can use works about the coverage of imperative code ([7]).	"case { A or B: V1, else V2}" Into
		"case { A: V1,
		B: V1,
		else V2}".

So, in this section, we want to generate test cases to test the AIFP according to AIFP coverage criteria.