Parametric schedulability analysis of a launcher flight control system under reactivity constraints

TL;DR

This paper introduces a parametric schedulability analysis method for space launcher flight control systems, using formal models and synthesis tools to improve scheduling reliability and efficiency.

Contribution

It formalizes launcher flight control scheduling with parametric stopwatch automata and demonstrates the effectiveness of the IMITATOR tool for parameter synthesis.

Findings

Successful formalization of the scheduling problem

Effective parameter synthesis with IMITATOR

Comparison shows advantages over traditional tools

Abstract

The next generation of space systems will have to achieve more and more complex missions. In order to master the development cost and duration of such systems, an alternative to a manual design is to automatically synthesize the main parameters of the system. In this paper, we present an approach on the specific case of the scheduling of the flight control of a space launcher. The approach requires two successive steps: (1) the formalization of the problem to be solved in a parametric formal model and (2) the synthesis of the model parameters with a tool. We first describe the problematic of the scheduling of a launcher flight control, then we show how this problematic can be formalized with parametric stopwatch automata; we then present the results computed by IMITATOR. We compare the results to the ones obtained by other tools classically used in scheduling.

Figures

Tables

Table 1. Table I : Computation times without reactivities

Analysis	Time (s)
No parameter	3.086
Parametric offsets	95.807
Parametric deadlines	17.689

Table 2. Table II : Computation times with reactivities

Analysis	Monolithic (s)	Compositional (s)
No parameter	109.404	40.092
Parametric offsets	2303.975	2278.363
Parametric deadlines	637.169	331.272

Table 3. Table III : Computation times without parameters

Analysis	Without reactivities (s)	With reactivities (s)
Cheddar		N/A
IMITATOR	3.086	109.404
Uppaal	0.002	0.003

Table 4. Table IV : Computation times with reactivities (full)

Analysis	Monolithic (s)	NGC (s)	NC (s)	NM (s)	Compositional (s)
No parameter	109.404	21.427	3.444	15.221	40.092
Parametric offsets	2303.975	1111.916	210.784	955.663	2278.363
Parametric deadlines	637.169	172.962	28.540	129.770	331.272

Equations

$$w_{\setminus {\mathbb{X}}^{\prime }}^{\nearrow +d}(x)=\{\begin{array}{ll}w(x)& \text{if }x\in {\mathbb{X}}^{\prime }\\ w(x)+d& \text{otherwise}\end{array}$$

Full text

I Introduction

Real-time systems combine concurrent behaviors with hard timing constraints. An out-of-date reply is often considered as invalid even if its content is correct. For critical real-time systems, if a time constraint is violated, then the consequences can be disastrous. Thus, a formal verification phase is essential in order to statically guarantee that all the tasks will be executed in their allocated time, and that the system will return results within the times guaranteed by the specification.

Assessing the absence of timing constraints violations is even more important when the system can be hardly controlled once launched. This is especially true in the aerospace area, where a system can only very hardly be modified or even rebooted after launching.

While verifying a real-time system is already a notoriously difficult task, we tackle here the harder problem of synthesis, i. e., to automatically synthesize a part of the system so that it meets its specification. The next generation of space systems will have to achieve more and more complex missions. In order to master the development cost and duration of such systems, an alternative to a manual design is to automatically synthesize the main parameters of the system.

Contribution

In this paper, we address the specific case of the scheduling of the flight control of a space launcher. Our approach requires two successive steps:

the formalization of the problem to be solved in a parametric formal model and, 2. 2.

the synthesis of the model parameters with a tool.

We first describe the problematic of the scheduling of a launcher flight control, then we formalize this problematic with parametric stopwatch automata, and third we present the results computed by the IMITATOR tool. We compare our results with the ones obtained by other tools classically used in scheduling. A key aspect is the verification and synthesis under some reactivity constraints: the time from a data generation to its output must always be less to a threshold. The solution we propose is compositional.

We propose here a solution to the problems using an extension of parametric timed automata (PTAs), an extension of finite state automata with clocks and parameters [AHV93]. PTAs are notoriously undecidable (see [And19] for a survey), despite some decidable subclasses (e. g., [HRSV02, BL09, AL17, ALR18]), notably in the field of scheduling real-time systems [CPR08, And17]. In spite of these undecidability results, we show that this formalism is handful for solving concrete problems—such as the one considered here.

Outline

After discussing related works in Section II, Section III presents the problem we aim at solving. Section IV recalls parametric stopwatch automata. Sections V and VI expose our modeling, while Section VII gives the results obtained. Section VIII makes a comparison with additional tools of the literature (solving only a part of the problem). Section IX concludes the paper.

II Related works

Scheduling

A long line of works in the last four decades has been devoted to the problem of scheduling analysis of real-time systems with various flavors. Several analytical methods were proposed to study the schedulability for a particular situation. Such analytical methods need to be tuned for each precise setting (uniprocessor or multiprocessor, scheduling policy, absence or presence of offsets, jitters, etc.). Most of them do not cope well with uncertainty. For example, in [BB97], three methods for the schedulability analysis with offsets are proposed. In [BB04], an efficient approach for testing schedulability for $\mathsf{RMS}$ (rate monotonic) in the case of (uniprocessor) analysis is proposed, through a “parameter” (different from our timing parameters) to balance complexity versus acceptance ratio.

Scheduling with model checking

Schedulability with model checking is a trend that started as early as the first works on timed model checking (e. g., [WME92, AHV93, AD94, YMW97, CC99]), and grew larger since the early 2000s. On the negative side, the cost of state space explosion often prevents to verify very large real-time systems. On the positive side, they allow for more freedom, and can model almost any system with arbitrarily complex constraints; in addition, despite the cost of state space explosion, they can be used to verify small to medium-size systems for which no other method is known to apply.

A natural model to perform schedulability analysis is (extensions of) timed automata (TAs) [AD94]. In [AM01, AM02, AAM06], (acyclic) TAs are used to solve job-shop and scheduling problems. This allows to model naturally more complex systems which are not captured so easily in traditional models of operation research.

In [NWY99, FKPY07, And17], task automata are proposed as a formalism extending TAs to ease the modeling (and the verification) of uniprocessor real-time systems: in some cases, the schedulability problem of real-time systems is transformed into a reachability problem for standard TAs and it is thus decidable. This allows to apply model-checking tools for TAs to schedulability analysis with several types of tasks and most types of scheduler.linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]ÉA: remove if space needed?

In [SLS*+*14], hierarchical scheduling systems are encoded using linear hybrid automata, a model that generalizes TAs. This approach outperforms analytical methods in terms of resource utilization. In [SL14], linear hybrid automata are used to perform schedulability analysis for multiprocessor systems under a global fixed priority scheduler: this method is more scalable than existing exact methods, and shows that analytical methods are pessimistic.

In [FLSC16], a schedulability analysis method is introduced using the model of timed regular task automata (using under-approximated WCETs) and then using nested timed automata (which is exact).

The problem we solve here shares similarities with analyses done in [FBG*+*10, MLR*+*10]. An important difference between [FBG*+*10, MLR*+*10] and our case study comes from the fact that, here, there are two distinct notions of “thread” and “processing”, while in [FBG*+*10, MLR*+*10] there was only one notion called “task”. Most importantly, none of these works consider timing parameters.

Scheduling with parameters

When some of the design parameters are unknown or imprecise, the analysis becomes much harder. Model checking with parameters can help to address this. In [CPR08], PTAs are used to encode real-time systems so as to perform parametric schedulability analysis. A subclass (with bounded offsets, parametric WCETs but constants deadlines and periods) is exhibited that gives exact results. In contrast, our work allows for parameterized deadlines; in addition, reactivities are not considered in [CPR08].

In [FLMS12], we performed robust schedulability analysis on an industrial case study, using the inverse method for PTAs [ACEF09] implemented in IMITATOR. While the goal is in essence similar to the one in this manuscript, the system differs: [FLMS12] considers multiprocessor, and preemption can only be done at fixed instants, which therefore resembles more Round Robin than real $\mathsf{FPS}$. In [SSL*+*13], we showed that PTAs-based methods are significantly more complete than existing analytical methods to handle uncertainty. In [SAL15], we solved an industrial challenge by Thales using IMITATOR.

In [LPPR13], the analysis is not strictly parametric, but concrete values are iterated so as to perform a cartography of the schedulability regions. However, the resulting analysis of the system is incomplete.

In [BHJL16], timed automata are “extended” with multi-level clocks, of which exactly one at a time is active. The model enjoys decidability results, even when extended with polynomials and parameters, but it remains unclear whether concrete classes of real-time systems can actually be modeled.

Finally, Roméo [LRST09] also allows for parametric schedulability analysis using parametric time Petri nets [TLR09].

III Description of the system and problem

The flight control of a space launcher is classically composed of three algorithms:

• •

The navigation computes the current position of the launcher from the sensor’s measurement (such as inertial sensors);

• •

The guidance computes the most optimized trajectory from the launch pad to the payload release location;

• •

The control orientates the thruster to follow the computed trajectory.

Due to the natural instability of a space launcher, strict real-time requirements have to be respected by the implementation of the flight control: frequency of each algorithm and reactivity between the sensor’s measurement acquisition and the thruster’s command’s sending.

The case study described in this paper is a simplified version of a flight control composed of a navigation, a guidance, a control and a monitoring algorithms (also called processings). Each processing has a name and a required period. A processing can potentially read data from the avionics bus (“in” data) and / or write data to the same avionics bus (“out” data). Fig. 1 shows an example of such system (all the numerical data provided in this paper are only examples which do not correspond necessarily to an actual system).

III-A Threads and deterministic communications

Processings are allocated on threads run by the processor. In our setting, all the thread’s periods are harmonic, i. e., a thread period is a multiple of the period of the thread just smaller (they pairwise divide each other).

In addition, in order to ensure the determinism of the scheduling (which facilitates the verification of the system), the threads work in a synchronous manner:

• •

The inputs of a thread are read at its start (no inputs are read during the execution of the thread)

• •

The outputs of a thread are provided at its deadline (no outputs are provided during the execution of the thread)

Fig. 2 shows the way data are exchanged between two threads. The fast thread (in yellow) has a period of 1. This period defines the time granularity of the system (this implies that the offset of the fast thread is 0 and that its deadline is 1). On this example, the slow thread (in blue) has an offset of 1 (its start is delayed of 1 cycle compared to the start of the fast thread) and a deadline of 8. The communication between the fast thread and the slow one is performed immediately at the end of the first execution of the fast thread. In order to ensure the determinism and taking into the priority between the threads, the communication between the slow thread and the fast thread is performed at the deadline of the slow thread, i. e., at the end of the cycle 9 (offset + deadline).

III-B Reactivities

To ensure the controllability of the launcher, a reactivity is required between a data read from the avionics bus (a measurement) and a data written to the avionics bus (a command). Several paths are potentially possible between a read data and a written data. Fig. 3 shows an example of such reactivities.

We want to solve the scheduling problem of periodic processing under precedence and reactivity constraints, as in [FBG*+*10]. Reactivities too must follow the deterministic communication model from Section III-A. Consider the reactivity “Meas $\rightarrow$ Navigation $\rightarrow$ Guidance $\rightarrow$ Control $\rightarrow$ Cmd” depicted in Fig. 4 (the values of periods and WCETs are not necessarily the ones given in our case study). Due to the data being communicated at the end of each thread only, the Guidance processing (marked with “G” in green) does not receive the data from the third execution of the Navigation processing (marked with “N” in red), as the data of the third Navigation will be sent at the end of the thread T1 period, but from the second execution of Navigation. Therefore, in Fig. 4, the only path of interest is the path of the data starting from the second execution of Meas, going to the second execution of Navigation, then going to the (only) execution of Guidance, and then finishing in the third execution of Control, before being written to the third occurrence of Cmd. Also note that the data output by the first execution of Navigation are successfully sent to T2 at the end of the first period of T1, but will be overwritten by the second occurrence of Navigation, and are therefore not of interest for the computation of reactivities.

III-C Processings and assignment into threads

A WCET (worst case execution time) is measured or computed for each processing. An example is given in Fig. 5.

An important problem is to find a proper assignment of the processings into threads, with their respective periods. A solution to this problem consists on a set of cyclic threads on which the processings are deployed. In our setting, these threads are scheduled with a preemptive and fixed priority policy ($\mathsf{FPS}$). A thread has a name and is defined by the following data:

• •

a rational-valued period;

• •

a rational-valued offset (with offset $\leq$ period), i. e., the time from the system start until the first periodic activation;

• •

a rational-valued (relative) deadline (with deadline $\leq$ period), i. e., the time after each thread activation within which all processings of the current thread should be completed;

• •

a rational-valued major frame (or “MAF”). A MAF defines the duration of a pattern of processing activation;

• •

a set of processings deployed in the thread. Different processings may be executed at each cycle. However, after a MAF duration, the same pattern of processings is repeated.

III-D Formalization

A real-time system $\mathcal{S}=\{{\cal T},{\cal P},{\cal R}\}$ is viewed here as a set of threads ${\cal T}=\{T_{1},T_{2},\cdots,T_{n}\}$, a set of processings ${\cal P}=\{P_{1},P_{2},\cdots,P_{m}\}$ and a set of reactivities ${\cal R}=\{R_{1},R_{2},\cdots,R_{q}\}$. A thread $T_{i}$ generates a possibly infinite stream of processings $P_{1},P_{2},\cdots$.

A thread $T_{i}$ is periodic, and characterized by a 5-tuple $(PT_{i},OT_{i},DT_{i},MAF_{i},{\cal P}_{i})$, where $PT_{i}$ corresponds to the period, $OT_{i}$ to the offset, $DT_{i}$ to the deadline, $MAF_{i}$ defines the duration of a pattern of processing activation $P_{i,j}$, and ${\cal P}_{i}$ defines a subset of processings of ${\cal P}$ allocated to $T_{i}$.

A processing $P_{i}$ is characterized by two values $WCET_{i}$ and $PP_{i}$. When a processing is activated, it executes for at most time $WCET_{i}$, and has to terminate within the relative period $PP_{i}$.

These definitions are illustrated in Fig. 6.

A reactivity is of the form $R_{i}=((P_{i,1}\rightarrow P_{i,2}\rightarrow\dots\rightarrow P_{i,k}),DR_{i})$ where $(P_{i,1}\rightarrow P_{i,2}\rightarrow\dots\rightarrow P_{i,k})$ denotes a precedence constraint of ${\cal P}$, and $DR_{i}$ is the maximum time of reactivity for $R_{i}$: the end of the thread containing the last processing $P_{i,k}$ of the precedence sequence has to be completed before the deadline $DR_{i}$.

Definition 1**.**

A system $\mathcal{S}$ is schedulable if

• •

$\forall$ $T_{i}$ $\in$ ${\cal T}$, the end of $T_{i}$ occurs before $DT_{i}$.

• •

$\forall$ $R_{i}$ $\in$ ${\cal R}$, the end of thread containing the last processing $P_{i,k}$ of $R_{i}$ occurs before $DR_{i}$.

III-E Description of the case study

We give here the values for the case study of interest.

III-E1 Processings

The processings $P_{i}$ considered corresponds to the lists:

• •

$P_{1}$(Navigation) = $(WCET_{1},PP_{1})=(1,5)$

• •

$P_{2}$(Control) = $(WCET_{2},PP_{2})=(3,10)$

• •

$P_{3}$(Monitoring) = $(WCET_{3},PP_{3})=(5,20)$

• •

$P_{4}$(Guidance) = $(WCET_{4},PP_{4})=(15,60)$

III-E2 Threads

The threads $T_{i}$ considered corresponds to the lists:

• •

$T_{1}$ = $(PT_{1},OT_{1},DT_{1},MAF_{1},{\cal P}_{1})=(5,OT_{1},DT_{1},10,\{P_{1},P_{2}\})$

• •

$T_{2}$ = $(PT_{2},OT_{2},DT_{2},MAF_{2},{\cal P}_{2})=(20,OT_{2},DT_{2},20,\{P_{3}\})$

• •

$T_{3}$ = $(PT_{3},OT_{3},DT_{3},MAF_{3},{\cal P}_{3})=(60,OT_{3},DT_{3},60,\{P_{4}\})$

III-E3 Reactivities

The reactivities (end-to-end flow) $R_{i}$ considered correspond to the lists:

• •

$R_{1}=((P_{1,1},P_{1,4},P_{1,2}),DR_{1})$ where $(P_{1,1}\rightarrow P_{1,4}\rightarrow P_{1,2})$ = (Navigation, Guidance, Control) and $DR_{1}$ = 150.

• •

$R_{2}=((P_{2,1},P_{2,2}),DR_{2})$ where $(P_{2,1}\rightarrow P_{2,2})$ = (Navigation, Control) and $DR_{2}$ = 15.

• •

$R_{3}=((P_{3,1},P_{3,3}),DR_{3})$ where $(P_{3,1}\rightarrow P_{3,3})$ = (Navigation, Monitoring) and $DR_{3}$ = 55.

III-F Objectives

In order to simplify the scheduling problem, we have considered in this paper a pre-allocation of processings on threads, as specified in Fig. 7: that is, Navigation and Control are allocated on T1, while Monitoring and Guidance are allocated on T2 and T3, respectively. In addition, Navigation is executed at every period of T1, while Control is executed (after Navigation) on odd cycles only; this is denoted by the when 1 syntax in Fig. 7(a). The offsets and deadlines of each thread are unknown; that is, the values in Fig. 7 are not part of the input of the problem. The flight control scheduling problem consists thus in computing the offsets and deadlines of each thread in order to fulfill the required reactivities.

Let us summarize the problems we address in this paper. Our problems take as input:

a flight control system i. e., a list of processings with their period, and their input or output data (for example Fig. 1); 2. 2.

a set of reactivities (for example Fig. 3); 3. 3.

a set of WCET for the processings (for example Fig. 5); 4. 4.

an allocation of processings on threads (for example Fig. 7).

A solution to this problem is a set of threads with their period, offset, deadline and MAF (the MAF can in fact be obtained immediately from the period). A solution is correct if the set of reactivities is schedulable (as in Definition 1).

The first problem is to formally verify a solution to the problem:

**scheduling verification problem:

**Input: a flight control system, a set of reactivities, a set of WCET, an allocation of processings on threads, and a solution

Problem: formally verify that $\mathcal{S}$ is schedulable.

The second problem is to synthesize solutions to the problem:

**scheduling synthesis problem:

**Input: a flight control system, a set of reactivities, a set of WCET, an allocation of processings on threads

Problem: exhibit correct solutions.

Recall that our synthesis problem still considers as input the periods, therefore offsets and deadlines are the main results of interest.

IV Parametric stopwatch automata

Clocks, parameters, constraints

We assume a set $\mathbb{X}=\{x_{1},\dots,x_{|\mathbb{X}|}\}$ of clocks, i. e., real-valued variables that evolve at the same rate. A clock valuation is a function $w:\mathbb{X}\rightarrow{\mathbb{R}}_{\geq 0}$. We write $\vec{0}$ for the clock valuation assigning [math] to all clocks. Given $R\subseteq\mathbb{X}$, we define the reset of a valuation $w$, denoted by $[w]_{R}$, as follows: $[w]_{R}(x)=0$ if $x\in R$, and $[w]_{R}(x)=w(x)$ otherwise. Given a valuation $w$, $d\in\mathbb{R}_{+}$ and $\mathbb{X}^{\prime}\subseteq\mathbb{X}$, we define the time-elapsing of $w$ by $d$ except for clocks in $\mathbb{X}^{\prime}$, denoted by $w^{\nearrow+d}_{\setminus\mathbb{X}^{\prime}}$, as the clock valuation such that

[TABLE]

We assume a set $\mathbb{P}=\{p_{1},\dots,p_{|\mathbb{P}|}\}$ of parameters, i. e., unknown constants. A parameter valuation $v$ is a function $v:\mathbb{P}\rightarrow{\mathbb{Q}}_{+}$. We denote ${\bowtie}\in\{<,\leq,=,\geq,>\}$. A guard $g$ is a constraint over $\mathbb{X}\cup\mathbb{P}$ defined by a conjunction of inequalities of the form $x\bowtie d$ or $x\bowtie p$, with $x\in\mathbb{X}$, $d\in{\mathbb{N}}$ and $p\in\mathbb{P}$. Given a guard $g$, we write $w\models v(g)$ if the expression obtained by replacing in $g$ each $x\in\mathbb{X}$ by $w(x)$ and each $p\in\mathbb{P}$ by $v(p)$ evaluates to true.

Parametric stopwatch automata

Parametric timed automata (PTA) extend timed automata with parameters within guards and invariants in place of integer constants [AHV93]. For many real-time systems, especially when they are subject to preemptive scheduling, parametric timed automata are not sufficiently expressive. As a result, we will use here an extension of PTA with stopwatches [CL00], namely parametric stopwatch automata [SSL*+*13].

Definition 2** (PSA).**

A parametric stopwatch automaton (PSA) $\mathcal{A}$ is a tuple $\mathcal{A}=(\Sigma,L,\ell_{0},\mathbb{X},\mathbb{P},\mathcal{I},\mathcal{S},E)$, where:

• •

$\Sigma$ is a finite set of actions,

• •

$L$ is a finite set of locations,

• •

$\ell_{0}\in L$ is the initial location,

• •

$\mathbb{X}$ is a finite set of clocks,

• •

$\mathbb{P}$ is a finite set of parameters,

• •

$\mathcal{I}$ is the invariant, assigning to every $\ell\in L$ a guard $\mathcal{I}(\ell)$,

• •

$\mathcal{S}$ is the stop function $\mathcal{S}:\ell\rightarrow 2^{\mathbb{X}}$, assigning to every $\ell\in L$ a set of stopped clocks,

• •

$E$ is a finite set of edges $e=(\ell,g,a,R,\ell^{\prime})$ where $\ell,\ell^{\prime}\in L$ are the source and target locations, $g$ is a guard, $a\in\Sigma$, and $R\subseteq\mathbb{X}$ is the set of clocks to be reset.

Stopwatch automata can be composed as usual using parallel composition on synchronized actions. Note that our clocks are shared by default, i. e., a same clock (i. e., with the same name) can be read, stopped or reset in several automata. The same applies to parameters.

Given a parameter valuation $v$ and PSA $\mathcal{A}$, we denote by $v(\mathcal{A})$ the non-parametric structure where all occurrences of a parameter $p\in\mathbb{P}$ have been replaced by $v(p)$. Any structure $v(\mathcal{A})$ is also a stopwatch automaton [CL00]. If $\mathcal{S}(\ell)=\emptyset$ for all $\ell\in L$, then by assuming a rescaling of the constants (multiplying all constants in $v(\mathcal{A})$ by their least common denominator), we obtain an equivalent (integer-valued) TA, as defined in [AD94].

Let us now recall the concrete semantics of stopwatch automata.

Definition 3**.**

Given a PSA $\mathcal{A}=(\Sigma,L,\ell_{0},\mathbb{X},\mathbb{P},\mathcal{I},\mathcal{S},E)$, and a parameter valuation $v$, the semantics of $v(\mathcal{A})$ is given by the timed transition system (TTS) $(S,s_{0},{\rightarrow})$, with

• •

$S=\{(\ell,w)\in L\times{\mathbb{R}}_{\geq 0}^{|\mathbb{X}|}\mid w\models v(\mathcal{I}(\ell))\}$,

• •

$s_{0}=(\ell_{0},\vec{0})$,

• •

${\rightarrow}$ consists of the discrete and (continuous) delay transition relations:

discrete transitions: $(\ell,w)\stackrel{{\scriptstyle e}}{{\mapsto}}(\ell^{\prime},w^{\prime})$, if $(\ell,w),(\ell^{\prime},w^{\prime})\in S$, and there exists $e=(\ell,g,a,R,\ell^{\prime})\in E$, such that $w^{\prime}=[w]_{R}$, and $w\models v(g$). 2. 2.

delay transitions: $(\ell,w)\stackrel{{\scriptstyle d}}{{\mapsto}}(\ell,w^{\nearrow+d}_{\setminus\mathcal{S}(\ell)})$, with $d\in{\mathbb{R}}_{\geq 0}$, if $\forall d^{\prime}\in[0,d],(\ell,w^{\nearrow+d^{\prime}}_{\setminus\mathcal{S}(\ell)})\in S$.linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]ÉA: Laurent: j’ai un peu improvisé pour les stopwatches ici, n’hésite pas à jeter un coup d’œil

V Specifying the system

Since the seminal work of Liu and Layland in [LL73], plenty of methods and tools have been designed to verify real-time systems. However, while some aspects are reasonably easy ($\mathsf{FPS}$, no mixed-criticality), the problem we address here is not typical for several reasons:

• •

offsets may be non-null;

• •

threads periods are harmonic;

• •

the executed processings may differ depending on the cycle;

• •

the reactivities must always be met, and therefore define new, non-classical timing constraints;

• •

and, perhaps most importantly, the admissible values for deadlines and offsets may not be known. Only the global end to end reactivity is specified.

As a consequence, we choose to follow a model checking based method. Model checking is known for being more expressive than analytical methods, at the cost of performance or even decidability. We show here that, although we use an undecidable formalism, we do get exact results for the instance of the problem we considered.

We present in the remainder of this section our modeling of the verification and the synthesis problem using parametric stopwatch automata. This formalism has several advantages. First, it is handful to model concurrent aspects of the system (different threads and processings running concurrently). Second, stopwatches can be used to model preemption. Third, parameters can be used to model the unknown constants, and solve the synthesis problem.

V-A Architecture of the solution

A modular solution

To model the system, we use the concurrent structure of parametric stopwatch automata to allow for a modular solution: that is, each element (thread, processing, scheduling policy) and each constraint (reactivity) is defined by an automaton. These automata are then composed by usual parallel composition on synchronization actions.

This makes our solution modular in the sense that, in the case of a modification in the system (e. g., the scheduling policy), we can safely replace one automaton by another (e. g., the $\mathsf{FPS}$ scheduler automaton with another scheduler automaton) without impacting the rest of the system.

Encoding elements and constraints as automata

We model each processing activation as an automaton. These automata ensure that processings are activated periodically with their respective period, and initial offset.

In addition, we create one automaton for each thread: the purpose of these automata is to ensure that the processings associated with each thread are executed at the right time. In the case of our concrete problem, we assign both the Navigation and Control processings to the T1 thread, the monitoring process to T2 and the guidance processing to T3.

The reactivities also follow the concept of modularity. That is, each reactivity is tested using a single automaton. By testing, we mean that a reactivity fails iff a special location is reached. Therefore, ensuring validity of the reactivities is equivalent to unreachability of these special locations.

Finally, we specify a scheduler automaton which provides the scheduling between the different threads (in the case of our problem, recall that the scheduling policy is fixed priority scheduling ($\mathsf{FPS}$).

We give more details on each of these automata in the following.

V-B Modeling periodic processing activations

Each processing is defined by a period and an offset. To model the periodicity of the processings, we create one automaton for each processing activation. This automaton simply performs the activations in a periodic manner. Activations are modeled by a synchronization action, used to communicate with other automata (typically the thread automaton).

In addition, the period processing activation automaton detects whether a processing missed its (implicit) deadline equal to its period; that is, we assume that a processing that has not finished by the next period is a situation to be avoided.

Each such automaton features a single clock.

We present in Fig. 8 the example of the $\mathsf{periodicControl}$ automaton, modeling the periodic activation of the Control processing. This controller contains a clock {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}xControl} and one parameter {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{periodControl}}. Note that the period {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{periodControl}} is known beforehand, and is therefore not strictly speaking a parameter, but that makes our solution both more generic and more readable (in IMITATOR, a parameter can be statically instantiated to a constant before running the analysis).

The initial location is $\mathrm{init}$: from then, the first occurrence of Control is immediately activated (action {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{actControl}}), and the automaton enters the $\mathrm{periodic}$ location. Then, exactly every {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{periodControl}} time units (guard {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}xControl}={\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{periodControl}}), another instance of Control is activated.

V-C Modeling threads

We create one automaton for each thread. Each of these automata contains one clock for the thread (used to measure the thread period and offset), as well as one clock per processings assigned to the thread. For example in Fig. 9, the thread automaton $\mathsf{threadT1}$ contains {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}xT1} (the thread clock), as well as {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}xExecControl} and {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}xExecNavigation} (the clocks associated to the processings of T1). Parameters include the offset, period and deadline of the thread, but also the WCETs of the processings assigned to this thread.

The thread automaton is responsible for:

encoding the initial thread offset, i. e., starting the periodic thread activation only after the offset; 2. 2.

performing the periodic thread activation; 3. 3.

executing the processings associated with the thread; 4. 4.

detecting the deadline misses.

The clocks associated with the processings are used to measure the execution time of these processings: they are in fact stopped most of the time, except when the thread is actively executing the processing. This is in contrast with the clocks associated with the processing activation automaton, that are never stopped, as they measure a period. Then, a deadline miss occurs if the clock measuring the thread period reaches the deadline (recall that the deadline is less than or equal to the period, and therefore we can use the same clock), while the clock measuring a processing execution time is strictly less than its WCET.

We give in Fig. 9 a fragment of the automaton $\mathsf{threadT1}$. We only give the odd cycle, as this is the most interesting; that is, we removed the fragment corresponding to the even cycle (only executing Navigation) between locations $\mathrm{init}$ and $\mathrm{exec\_nav\_odd}$ (and the transition from $\mathrm{idle}$ should go to the removed $\mathrm{exec\_nav\_even}$ location). We also abbreviate some variable names to save space (e. g., {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}xExecC} for {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}xExecControl} and {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}xExecN} for {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}xExecNavigation} or {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{WCETN}} for {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{WCETNavigation}}).

First, the automaton waits for the offset: that is, it stays in $\mathrm{init}$ exactly {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{offsetT1}} time units. Then, it executes the first processing of the odd cycle, i. e., Navigation: it stays in $\mathrm{exec\_nav\_odd}$ until completion, i. e., for {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{WCETNavigation}} time units.111In the full model, we can allow for a best case execution time, in which case the duration is non-deterministically chosen in the interval [{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{BCETNavigation}},{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{WCETNavigation}}].

Note that this is the only location where {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}xExecNavigation} is elapsing, i. e., is not stopped, as it measures the execution time. Then, upon completion of the Navigation processing, the automaton moves to $\mathrm{exec\_control\_odd}$, where Control is executed. Upon completion, it moves to $\mathrm{idle}$, and waits until the clock {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}xT1} reaches its period. Then, the cycle restarts and so on.

In addition, at any time, possible deadline misses are checked for. A deadline miss occurs on an odd cycle while execution Navigation whenever {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}xT1}={\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{deadlineT1}} and either {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}xExecControl}<{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{WCETControl}} or {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}xExecNavigation}<{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{WCETNavigation}}.222This encoding is not necessarily optimal. In fact, on odd cycles, as Navigation is executed first, and followed by Control, a deadline miss can be detected earlier, i. e., if Navigation is still executed, but there is not enough time to finish the execution of Navigation and that of Control: that is, an optimized deadline miss condition could be {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}xT1}+{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{WCETControl}}={\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{deadlineT1}} and {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}xExecNavigation}<{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{WCETNavigation}}. This optimization has not been implemented, so as to leave the model (relatively) simple and maintainable, but could be tested in the future.

When executing Control, only the execution time of Control needs to be checked.

Remark 1*.*

Our model is in fact more complicated as, for sake of modularity, we make no assumption in the thread automaton on how the other automata behave, notably the processings activation automata. Therefore, we allow for processings to be activated at any time, which must be taken care of in the thread automaton.

V-D Modeling the $\mathsf{FPS}$ scheduler

The $\mathsf{FPS}$ scheduler is modeled using an additional automaton. It reuses existing works from the literature (e. g., [FKPY07, SSL*+*13]), and does not represent a significant original contribution. We mainly reuse the scheduler encoding of [SSL*+*13], which consists of an automaton synchronizing with the rest of the system on the start and end task synchronization actions as well as the task activation actions. Whenever a new task is activated, the scheduler decides what to do depending on its current state and the respective priorities of the new and the executing tasks (if any).

Nevertheless, we had to modify this encoding due to the fact that existing scheduler automata simply schedule tasks: in the setting of our case study, the scheduler schedules both the threads and the threads’ processings. Among the various modifications, in case of preemption, our scheduler does not stop the clocks measuring the execution times of the preempted threads (because such clocks do not exist), but stop the clocks measuring the execution times of the processings belonging to the preempted threads.

We give in Fig. 10 an example of such a scheduler in a simplified version, with only two threads T1 and T2; the full scheduler is of course more complete. If any of the two threads get activated ({\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{actT1}} or {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{actT2}}), the scheduler starts executing them. If a second thread gets activated, the highest priority thread (T1) is executed, while T2 is put in waiting list (which is encoded in location $\mathrm{execT1waitT2}$). This is the location responsible for stopping the clock of the (only) processing of T2, i. e., Monitoring (clock {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}xexecM}). Only after T1 has completed ({\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{finT1}}), T2 can execute. Our real scheduler is in fact significantly more complex as it has to cope with three threads, but also with special cases such as the activation of a new thread activation of $T_{i}$ while executing a previous instance of $T_{i}$, etc.

V-E Reachability synthesis

Finally, the system is schedulable if none of the “bad” locations (corresponding to deadline misses, e. g., in the thread automata) is reachable. If all parameters are valuated, the system is a TA, and schedulability reduces to reachability checking. If some parameters are free (i. e., the analysis is parametric), the set of valuations for which the system is schedulable exactly corresponds to the valuations for which these bad locations are unreachable, i. e., the complement of the valuations set result of reachability synthesis. This guarantees our method correctness.

VI Compositional verification of reactivities

An originality of our work—which among other reasons justifies our choice to use model checking—is the encoding of reactivities. Indeed, our goal is to verify a system, or synthesize valuations, for which all reactivities are met.

How to properly encode reactivities turned out rather subtle. Let us first exemplify the complexity of the definition of reactivities.

Example 1**.**

Consider the third reactivity in Fig. 3 (abbreviated by NM in the following) that requires that any data transmission Meas $\rightarrow$ Navigation $\rightarrow$ Monitoring $\rightarrow$ Safeguard must always be less than 55 ms. Recall that data are transmitted upon the end of a thread period.

We can see this reactivity as the start of a timer at the beginning of the last thread period of an execution of Navigation that completed before the end of an execution of task T1, where T1 is such that it is the last execution of T1 the period of which ends before the start of an execution of Monitoring; then, the timer stops following the end of the period of an execution of T1 immediately following the end of the period of T3 corresponding to the end of the aforementioned execution of Monitoring. At the end, the timer must be less than 55 ms.

In other words, this reactivity requires that any following sequence of actions should take less than 55 ms: {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{startT1}}, {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{startNavigation}} followed by {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{endNavigation}} (without any occurrence of {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{startNavigation}} in between) followed by {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{endT1}}, followed by {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{startT3}} (without any occurrence of {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{endT1}} in between), {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{startMonitoring}} followed by {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{endMonitoring}} (without any occurrence of {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{startMonitoring}} in between), followed by {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{endT3}}.

Encoding reactivities is arguably the most technical part of our solution, and we tried multiple solutions (either incorrect or that represented a too large overhead) before converging to this solution. Nevertheless, the solution we chose still represents a large overhead, as we will see in Section VII.

In our solution, each reactivity is encoded as a sort of observer automaton [ABBL03, And13]; an observer automaton observes the system behavior without interfering with it. That is, it can read clocks, and synchronize on synchronization actions, but without impacting the rest of the systems; in particular, it must be non-blocking (except potentially once the property verified by the observer is violated). In addition, an observer often reduces to reachability analysis: the property encoded by the observer is violated iff a special location of the observer is reachable.

Each reactivity automaton uses a single (local) clock used to check the reactivity constraint, and synchronizes with the rest of the system on synchronization labels encoding the start and end of processings and tasks.

In fact, we deviate from the principle of observer automaton by allowing it to block in some cases. Indeed, a key point in the definition of reactivities in our problem is the communication between threads as exemplified in Example 1. In order to allow a generic solution for reactivities, and due to the fact that some timing parameters are unknown, we cannot make assumptions on the respective ordering of processings w.r.t. each other. Therefore, when a given processing is faster than another one (e. g., Navigation is faster than Guidance), it is not a priori possible to know which instance of the fast processing (e. g., Navigation) will effectively transmit its data to the following slower processing (e. g., Monitoring). As a consequence, our observer will non-deterministically “guess” from which instance of the slower processing to start its timer: this is achieved by a non-deterministic choice in the initial location of the automaton. If the guess is wrong, the observer “blocks” the system (impossibility to fire a transition or let time elapse).

Example 2**.**

Consider again reactivity NM. Consider a given instance of Navigation. If a second full instance of Navigation (including the end of thread T1) is observed before the start of T2, our observer made a wrong guess, and the observer clock is not measuring a proper reactivity, as the instance of Navigation on which the clock should be started must be the last completed instance before the start of T2. In that case, the observer simply blocks.

Note that, while blocking is usually not an admissible feature of observer automata, this is harmless in this case as, due to the non-deterministic guess and the fact that model checking explores all choices, all possible behaviors of the system are still explored by our solution.

VI-A Observer construction

Therefore, our solution consists in translating the sequence of starting and ending actions of threads and processings following the definition of the reactivities, while forbidding some actions in some locations to ensure the proper encoding of the definition of thread communication and reactivities. In addition, a clock measuring the reactivity is started upon the (non-deterministic) activation of the first thread, and is checked against the reactivity nominal maximum time upon completion of the last thread. If this maximum time constraint is violated, the observer enters a special “bad” location. This observer violation location is added to the list of “bad” locations in Section V-E when performing reachability synthesis.

Example 3**.**

We give the observer automaton corresponding to reactivity NM in Fig. 11. We abbreviate in Fig. 11 the names of processings (N and M stand for Navigation and Monitoring respectively). The only clock is {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}xNM} while {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{reacNM}} denotes the maximum nominal reactivity for NM (55 ms in our setting). $\Sigma_{NM}$ stands for this automaton alphabet; given $a\in\Sigma_{NM}$, $\overline{a}$ denotes $\Sigma_{NM}\setminus\{a\}$ (we extend this notation to sets of actions). In addition, whenever {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}xNM}>{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{reacNM}} occurs in any location (except the initial location), a transition leads to $\mathrm{bad}$ (not depicted in Fig. 11 for sake of clarity).

The non-deterministic choice is encoded in the initial location where, upon action {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{startT1}}, the automaton can either self-loop in $\mathrm{init}$, or go to $\mathrm{startT1}$ to try to measure the reactivity from this instance of T1. The blocking is encoded by the absence of transition labeled with {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{endT1}} in location $\mathrm{wait\_T3}$ (an alternative is to synchronize on {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{endT1}} to a sink location that also blocks time elapsing).

Both remaining reactivities in Fig. 3 follow easily from this scheme: the first reactivity (Navigation $\rightarrow$ Guidance $\rightarrow$ Control) follows the same principle for Navigation and Guidance, and is immediately followed by a third check for Control, while the second reactivity (Navigation $\rightarrow$ Control) is simpler as both Navigation and Control are on the same thread.

VI-B Compositional verification and synthesis

Due to the non-deterministic choice, the verification of the reactivities entails a clear overhead to the verification (see Section VII). Verifying all three reactivities can be naturally done by adding the three observer automata to the same system, and performing synthesis on the composition of all these automata.

However, we claim that this can be done in a compositional fashion. Indeed, checking reactivities is checking that a constraint is met for all executions; this can be seen as a global invariant. Therefore, checking that these three invariants are valid can be done separately. In the non-parametric case, we will perform three different verifications of the system, with only one reactivity automaton at a time. Then, if the “bad” locations are unreachable for the three different verifications, then the system is schedulable and the reactivities are met. In the case of synthesis, we will intersect the result of the synthesis applied to the three parametric models.

This compositional analysis comes in contrast with many works on scheduling, where compositionality is hard to achieve.

VII Experiments

VII-A Experimental environment

We modeled our network of PSA in the IMITATOR input language [AFKS12]. IMITATOR is a parametric model checker taking as input networks of PSA extended with useful features such as synchronization actions and discrete variables. Synthesis can be performed using various properties including reachability—which is the feature we use here. When IMITATOR terminates (which is not guaranteed in theory), the tool is often able to infer whether the result is exact (sound and complete); all analyses mentioned in this manuscript terminate with an exact result.

The translation effort was manual due to the specificity of our solution (with the exception of the scheduler, for which we started from an automated generator). However, we tried to keep our translation as systematic as possible to allow for a future automated generation from the problem input data. We made intensive use of clock resets and stopwatches for clocks not necessary at some points, in order to let IMITATOR apply inactive clock reductions.

All experiments were conducted using IMITATOR 2.10.4 “Butter Jellyfish” on an ASUS X411UN Intel Core$\texttrademark$ i7-8550U 1.80 GHz with 8 GiB memory running Linux Mint 19 64 bits.333Sources, binaries, models and results are available at imitator.fr/static/ACSD19/

VII-B Verification and synthesis without reactivities

In order to evaluate the overhead of the satisfaction of the reactivities, we first run analyses without reactivities.

Non-parametric model

First, a non-parametric analysis shows that the bad locations are unreachable, and therefore the system is schedulable under the nominal values given in Figs. 1 and 5. We give in Fig. 15 in Section -D the Gantt chart (obtained with Cheddar [Sin]) of this entirely instantiated model. Computation times of all the analyses without reactivities are given in Table I.

Parameterized offsets

We then parameterize offsets, i. e., we seek admissible offsets for which the system is schedulable. The constraint is given in Section -A1. We can see that, while several conditions for schedulability are given, at least one offset must be 0 to ensure schedulability.

Parameterized deadlines

We then parameterize deadlines, i. e., we seek admissible deadlines for which the system is schedulable. The constraint is: {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{deadlineT2}}{}\in[11,20]\land\ {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{deadlineT1}}{}\in[4,5]\land\ {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{deadlineT3}}{}=60. That is, the deadline of T3 is strict, while T1 and T2 can be relaxed while preserving schedulability.

VII-C Compositional verification of reactivities

We then solve the scheduling verification and scheduling synthesis problems with reactivities, using two methods:

• •

monolithic verification: all three reactivity automata are included in the model;

• •

compositional verification: we verify sequentially three different models, each of them including all automata modeling the system, but only one reactivity at a time.

We give the various computation times in Table II. A full version of this table, including the overhead incurred by each reactivity, is given in Table IV in Section -B1. Table II shows the interest of the compositional verification over monolithic verification, as the computation time is divided by a factor 2.

VIII Comparison with other tools

We perform a comparison with two other well-known tools, one from the real-time system community, namely Cheddar [Sin], and one from the timed automata community, namely Uppaal [LPY97]. Both tools cannot handle parameters nor consider partially specified problems, and therefore can only solve the scheduling verification problem. Therefore, in this section, we consider the instantiated version of the system according to the nominal values given in Figs. 1 and 5. In addition, to the best of our knowledge, Cheddar cannot test the reactivities.

Comparison with Cheddar

Cheddar is a real-time scheduling tool distributed under the GPL license. Cheddar is used to model software architectures of real-time systems and to check if the system is schedulable.

We checked the system’s schedulability using Cheddar when the system is instantiated (i. e., all offsets are initialized to 0 and the deadline of each thread equal to the period). We have indicated the period, the execution time and deadline of each processings.

As result, Cheddar proves that the system is schedulable and there are no deadline missed in the computed scheduling. In this solution, the number of context switches per period of T3 is 29 and the number of preemptions is 8.linecolor=purple,backgroundcolor=purple!25,bordercolor=purple]JJ: Ce modèle rassemble un peu le modèle instancié de GNC, la différence est que: dans ce modèle Control s’exécute pendant le cycle pair (cycle impair dans GNC). Les 29 switches et 8 préemptions (3 préemptions de Monitoring et 5 préemptions de Guidance ) sont calculés pendant 60 ms(periode de Guidance). J’ai ajouté un autre modèle avec Cheddar où control s’exécute pendanr le cycle impair comme le modèle GNC et qui donne aussi 29 switches et 8 préemptionslinecolor=blue,backgroundcolor=blue!25,bordercolor=blue]ÉA: Merci. Mais c’est toi qui a mis la limite de 60, ou c’est Cheddar? linecolor=purple,backgroundcolor=purple!25,bordercolor=purple]JJ: Oui, c’est Cheddar qui a choisit la limite de 60

Cheddar cannot give a solution to the scheduling synthesis problem since it only works with instantiated systems, so we cannot determine offsets and deadlines, and also it does not deal with reactivities.

Comparison with Uppaal

We also compare the obtained results using IMITATOR with Uppaal results. We wrote a Uppaal model identical to the IMITATOR model—with instantiated parameters.

As result, Uppaal proves that the instantiated system is schedulable, both without and with reactivities.

Summary of comparisons

We give the computation times without reactivities in Table III. Clearly, without parameters, Cheddar or Uppaal should be used. However none of these tools cope with uncertain constants.

IX Conclusion and perspectives

We proposed an approach to synthesize timing valuations ensuring schedulability of the flight control of a space launcher. A key issue is to ensure that the system reactivities are met—for which we proposed a compositional solution.

Future works

We omitted an element of the problem: the switch between two threads has a CPU cost due to the copy of data between the contexts of each thread which is in our example $500\,\mu{}s$. This can be added by modifying the scheduler automaton; a more interesting outcome will be to synthesize the maximum admissible switch time (possibly depending on other parameters) that still ensures schedulability.

Due to the efficiency gap of an order of magnitude, combining some non-parametric analyses (e. g., with Uppaal or Cheddar) with parametric analyses (IMITATOR) would be an interesting future work.

The harmonic periods are a strong assumption of the problem. Tuning our solution to benefit from this assumption is on our agenda.

We envisage two tracks for our longer-term future works:

• •

Generalizing the flight control scheduling problem by automatically synthesizing the allocations of processings on threads. This generalization raises first the issue of modeling such problematic (how to model an allocation with a parameter) and second the classical combinatorial explosion of states.

• •

Applying this approach to the automatic synthesis of the launcher sequential, i. e., of the scheduling of all the system events necessary to fulfill a mission: ignition and shut-down of stages, release of firing, release of payloads, etc.

-A Parametric analyses without reactivities

-A1 Parametric offsets

See Fig. 12.

-A2 Parametric offsets and deadlines

-B Parametric analyses with reactivities

-B1 Precise computation times

The computation times with reactivities giving the details of the compositional analysis is given in Table IV.

-C Parametric analyses with switch time without reactivities

-C1 Parametric offsets

See Fig. 13.

-C2 Parametric deadlines

See Fig. 14.

-D Scheduling with Cheddar

We give in Fig. 15 (obtained with Cheddar [Sin]) the Gantt chart of this entirely instantiated model.

In Fig. 16, we present an example of a scheduling analysis of a system with Cheddar.linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]ÉA: là, il vaudrait mieux mettre l’ordonnancement de notre système (instancié, donc), plutôt que “un” système arbitraire

linecolor=purple,backgroundcolor=purple!25,bordercolor=purple]JJ: J’ai ajouté la Fig. 15 qui présente le modèle GNC avec Cheddar

linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]ÉA: là j’ai supprimé pas mal de choses qui ne compilaient pas, à remettre