ESWEEK Tutorial: Schedulability Analysis under Uncertainty using Formal Methods

CALL FOR PARTICIPATION

Tutorial: Schedulability Analysis under Uncertainty using Formal Methods

ESWEEK satellite event

September 30, 2018 | Torino, Italy | https://www.imitator.fr/tutorials/ESWEEK18/

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

Etienne Andre (Universite Paris 13, France)
Giuseppe Lipari (Universite Lille, France)

Support

The tutorial is partially supported by French project ANR PACS (Parametric
analyses of concurrent systems).

https://lipn.univ-paris13.fr/PACS/