Tutorial on Schedulability Analysis under Uncertainty using Formal Methods

Practical information in a nutshell

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

Room: Sella

Description of the tutorial

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.

Speakers

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

Resources and content

Slides

Real-time systems (Giuseppe Lipari)

slides
slides

Real-time systems and parametric timed automata (Étienne André)

slides part 2

Practical session

A monoprocessor system

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

A distributed system

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.

Bibliography

[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.