The tutorial took place on Sunday 30th of September 2018 in ESWEEK 2018 (Torino, Italy).

Time: 9am to 6pm

Room: Sella

Modern real-time systems must cope with different sources of variability. Modern hardware processors introduce several sources of variability in the execution time of the software (cache, pipeline, bus contention, etc.); and the timing of external events may change due to changes in the environments, malfunctions, etc. This variability adds additional challenges for the design, development and validation of modern cyber-physical systems.

It is then necessary to estimate the robustness of the system w.r.t. variations of the parameters. A key issue is to estimate for which values of the parameters the system continues to meet all its timing constraints.

In this tutorial, we present the background for analyzing real-time systems using formal methods, and notably the formalism of parametric timed automata to analyze real-time scheduling under uncertainty. Then we will give a survey of some real-time scheduling problems, and we will show how to model a typical real-time system using the IMITATOR tool. The participants will be guided toward building and verifying a model of a real-time system, exploring the capability of the analysis tool.

- Étienne André (Université Paris 13, France)
- Giuseppe Lipari (Université Lille, France)

- slides
- slides

- Download the slides, that contain all the commands
- Download the scripts: RETIMI
- Download the models:
- Response time analysis
- Sensitivity analysis
- Response time with offsets

- Download and open the file exModel.imi using your favorite text editor (if you use a KDE environment, Kate with the Ocaml highlighting mode does an almost-perfect job)
- Generate a graphical version of the model as follows:
> ./imitator exModel.imi -PTA2PNG

This will generate a file exModel-pta.png This model is non-parametric. Which real-time system is this model modeling? How many tasks? How many processors? Which tasks are triggered by other tasks? Are periodic? Are sporadic? - Schedulability reduces to safety checking. Perform schedulability analysis using the following command:
> ./imitator exModel.imi -mode EF -merge -incl -output-result

The system is schedulable if and only if the answer of safety is "true", i.e., no deadline miss is reachable. - Let us now parameterize the WCET of task 1.1. This is achieved by commenting the value of parameter WCET_T11 ("= 5") in the header.
The resulting file can be obtained here.
Parametric schedulability reduces to parametric safety checking. Perform parametric schedulability analysis using the following command:
> ./imitator exModel-1-WCET11.imi -mode EF -merge -incl -output-result

The system is schedulable for exactly the set of valuations output by IMITATOR. - Let us now parameterize the WCET of both tasks 1.1 and 2.1. This is achieved by commenting the value of parameters WCET_T11 and WCET_T21 in the header.
The resulting file can be obtained here.
Parametric schedulability reduces to parametric safety checking. Perform parametric schedulability analysis using the following command:
> ./imitator exModel-2-WCET11-21.imi -mode EF -merge -incl -output-result -output-cart

The system is schedulable for exactly the set of valuations output by IMITATOR. The generated file exModel-2-WCET11-21_cart.png shows a graphical representation of the schedulable parameter space. - Let us now parameterize (only) the offset of task 2.1. This is achieved by commenting the value of parameter offsetT21 in the header.
The resulting file can be obtained here.
Parametric schedulability reduces to parametric safety checking. Perform parametric schedulability analysis using the following command:
> ./imitator exModel-3-offset21.imi -mode EF -merge -incl -output-result

The system is schedulable for exactly the set of valuations output by IMITATOR. - Let us now parameterize the WCET of both tasks 2.1 and 2.2. This is achieved by commenting the value of parameters WCET_T11 and WCET_T21 in the header.
The resulting file can be obtained here.
Parametric schedulability reduces to parametric safety checking. Perform parametric schedulability analysis using the following command:
> ./imitator exModel-4-WCET21-22.imi -mode EF -merge -incl -output-result -output-cart

The system is schedulable for exactly the set of valuations output by IMITATOR. The generated file exModel-2-WCET11-21_cart.png shows a graphical representation of the schedulable parameter space.

- [AFKS12]
- Étienne André, Laurent Fribourg, Ulrich Kühne and Romain Soulat. IMITATOR 2.5: A Tool for Analyzing Robustness in Scheduling Problems. In Dimitra Giannakopoulou and Dominique Méry (eds.), FM’12, LNCS 7436, Springer, pages 33–36, August 2012. (English) [PDF | PDF (author version) | BibTeX]
- [AHV93]
- Rajeev Alur, Thomas A. Henzinger, Moshe Y. Vardi: Parametric real-time reasoning. STOC 1993: 592-601.
- [AS13]
- Étienne André and Romain Soulat. The Inverse Method. ISTE Ltd and John Wiley & Sons Inc. ISBN: 9781848214477. January 2013. (English) [PDF | BibTeX]
- [LSAF14]
- Giuseppe Lipari, Sun Youcheng, Étienne André and Laurent Fribourg. Toward Parametric Timed Interfaces for Real-Time Components. In Étienne André and Goran Frehse (eds.), SynCoP’14, EPTCS, April 2014.