Ph.D. funding available at Univ. Grenoble Alpes / Verimag (France)
h.D. funding available at Univ. Grenoble Alpes / Verimag (France)
Supervisors: Saddek Bensalem and Yliès Falcone, Univ. Grenoble Alpes (emails: Saddek.Bensalem@univ-grenoble-alpes.fr
<mailto:Saddek.Bensalem@univ-grenoble-alpes.fr> and Ylies.Falcone@univ-grenoble-alpes.fr <mailto:Ylies.Falcone@univ-grenoble-alpes.fr>)
This thesis aims at complementing rigorous system design with runtime verification techniques for cyber-physical
In particular, we are interested in the following important features of CPSs: real-time behavior, distributed
execution, and architecture dynamicity.
A rigorous system design flow is a formal accountable and iterative process for deriving trustworthy and
optimized implementations from application software and models of its execution platform and its external
environment. Rigorous system design is a formally defined process decomposed into steps. It is also model-based:
successive system descriptions are obtained by the application of correct-by-construction source-to-source of
a single expressive model rooted in well-defined semantics. An additional demand is accountability that is the
possibility to explain which among the requirements is satisfied and which may not be satisfied.
Runtime verification (RV) is the umbrella term to encompass all aspects of monitoring and analysis of hardware,
software and the executions of systems in general. RV techniques are lightweight dynamic techniques to assess
and enforce correctness, reliability, and robustness during system execution. These techniques are significantly
more powerful, versatile and rigorous than conventional testing, and more practical than exhaustive formal
The RSD Research Group (http://www-verimag.imag.fr/RSD.html <http://www-verimag.imag.fr/RSD.html>) seeks motivated
candidates with a Masters degree in CS and a solid background on some of the following topics algorithms,
automata, logic, formal methods, machine learning, and statistical reasoning.
Such candidates who are ready to learn new things and complete their background are kindly requested to send
an e-mail (with "PhD candidate" in the title) with:
- a CV,
- a motivation letter, and
- recommendation letter(s),
to Saddek.Bensalem@univ-grenoble-alpes.fr <mailto:Saddek.Bensalem@univ-grenoble-alpes.fr> and Ylies.Falcone@univ-grenoble-alpes.fr
The Grenoble area, in addition to being surrounded skiable mountains is easily accessible: Lyon (1 hour),
Geneva (1.5 hours), Torino (2 hours), Paris (3 hours by train) and Barcelona (6 hours). It features one of
Europe’s largest concentrations of academic/industrial research and development with a lot of students,
a cosmopolite atmosphere and work opportunities.
VERIMAG, is a leading academic lab in verification and model-based design of embedded cyber-physical systems.
Its past contributions include model checking (J. Sifakis, Turing Award 2007), the data-flow language Lustre
(P. Caspi, N. Halbwachs) underlying the SCADE programming environment for safety-critical systems.