You are here

Event Details

MP Associates, Inc.
SUNDAY September 30, 9:00am - 6:00pm | Sella
Schedulability Analysis Under Uncertainty Using Formal Methods

Étienne André - Univ. Paris 13
Giuseppe Lipari - Univ. Lille
Étienne André - Univ. Paris 13
Giuseppe Lipari - Univ. Lille
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é is an associate professor with Université Paris 13, France. His research interests include model checking real-time systems, notably in the presence of timing uncertainty, or unknown constants. He contributed to the field of parametric timed automata, and is the lead developer of IMITATOR, a state-of-the-art parametric model checker, applied in several industrial contexts (including ST-microelectronics, Astrium State Space transportation, and Thales). Web page:

Giuseppe Lipari is Professor of Computer Science at University of Lille. He is head of the Embedded Real-Time Adaptative system Design and Execution (Émeraude) team of the Centre de Recherche en Informatique, Signal et Automatique (CRIStAL) de Lille. His research interests are in real-time systems, real-time operating systems, scheduling algorithms, embedded systems. He is an IEEE Fellow. Web page: