IMITATOR: Experiments Data for Fundamenta Informatica 2021

Models, sources and results related to "Parametric schedulability analysis of a launcher flight control system under reactivity constraints"

A static version of this page was permanently archived in June 2021 at 10.5281/zenodo.5042059.

We refer here to the case study first considered in [ACFJL19] and then in [ACFJL21].

Description of the system:

The case study is a flight control system of a space launcher that is composed of 3 threads, 4 processings and 3 reactivities constraints.
The system is analyzed in two settings:

Without time switch (here an example of scheduling chronogram fig)
With time switch (here an example of scheduling chronogram fig).

Models:

Some models using IMITATOR:
- The model of processing Control: fig
- The model of threadT1: fig
- The model of super scheduler (for the case without switch time): fig
- The model of super scheduler (for the case with switch time): fig
- The model of reactivityNC: fig
Some models using Uppaal:
- The model of processing Control: fig
- The model of threadT2: fig
- The model of super scheduler: fig
- The model of reactivityNM: fig

Experimental raw data

Version of IMITATOR

The version of IMITATOR used to run the experiments is IMITATOR v2.10.4 "Butter Jellyfish".

Download

Source code from GitHub
Binary (Ubuntu-like, Debian-like 64 bits); this binary is standalone and can hence be executed without any external library

Calling IMITATOR

The exact command used can be seen in the .log files. For most analyses, the following command was used:

> ./imitator [case_study.imi] -mode EF -merge -incl -output-result

For selected analyses, we also used the -no-inclusion-test-in-EF option.

Experimental environment

We conducted the experiments on a ASUS X411UN i7-8550U running Linux Mint 19 64bits with 8GiB memory.

Data

Without switch time:
- Model with no reactivities :
  - Non-parametric: model result log
  - Parametric offsets: model result log
  - Parametric deadlines: model result log
  - Parametric offsets and deadlines: model result log
- Model with reactivity NC:
  - Non-parametric: model result log
  - Parametric offsets: model result log
  - Parametric deadlines: model result log
- Model with reactivity NM:
  - Non-parametric: model result log
  - Parametric offsets: model result log
  - Parametric deadlines: model result log
- Model with reactivity NGC:
  - Non-parametric: model result log
  - Parametric offsets: model result log
  - Parametric deadlines: model result log
- Model with the 3 reactivities at the same time:
  - Non-parametric: model result log
  - Parametric offsets: model result log
  - Parametric deadlines: model result log
With switch time:
- Model with no reactivities :
  - Non-parametric: model result log
  - Parametric offsets: model result log
  - Parametric deadlines: model result log
- Model with reactivity NC:
  - Non-parametric: model result log
  - Parametric offsets: model result log
  - Parametric deadlines: model result log
- Model with reactivity NM:
  - Non-parametric: model result log
  - Parametric deadlines: model result log
- Model with reactivity NGC:
  - Non-parametric: model result log
  - Parametric deadlines: model result log
- Model with the 3 reactivities at the same time:
  - Non-parametric: model result log
  - Parametric deadlines: model result log