IMITATOR

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

Time: 9am to 6pm

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

Resources and content

Slides

Real-time systems (Giuseppe Lipari)

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

Practical session

A monoprocessor system

A distributed system

  1. 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)
  2. 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?
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. 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.