Parametric Schedulability Analysis of a Launcher Flight Control System under Reactivity Constraints^*

Issue title: Special Issue of Selected Papers from ACSD 2019

Guest editors: Jörg Keller and Wojciech Penczek

Article type: Research Article

Authors: André, Étienne^{a; †; ‡} | Coquard, Emmanuel^b | Fribourg, Laurent^c | Jerray, Jawher^d | Lesens, David^b

Affiliations: [a] Université de Lorraine, CNRS, Inria, LORIA, Nancy, France. eandre93430@lipn13.fr | [b] ArianeGroup SAS, Les Mureaux, France | [c] Université Paris-Saclay, LSV, CNRS, ENS Paris-Saclay, France | [d] Université Sorbonne Paris-Nord, LIPN, CNRS, UMR 7030, F-93430, Villetaneuse, France

Correspondence: [†] Address for correspondence: Université de Lorraine, CNRS, Inria, LORIA, Nancy, France.

Note: [*] This work is partially supported by the ANR national research program PACS (ANR-14-CE28-0002) and ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST.

Note: [‡] Also affiliated at: JFLI, CNRS, Tokyo, Japan, National Institute of Informatics, Tokyo, Japan.

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 for 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 problem of the scheduling of a launcher flight control, then we show how this problem can be formalized with parametric stopwatch automata; we then present the results computed by the parametric timed model checker IMITATOR. We enhance our model by taking into consideration the time for switching context, and we compare the results to those obtained by other tools classically used in scheduling.

Keywords: scheduling, real-time systems, model checking, parameter synthesis, IMITATOR

DOI: 10.3233/FI-2021-2065

Journal: Fundamenta Informaticae, vol. 182, no. 1, pp. 31-67, 2021