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 systems (CPSs). 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 verification. 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 <mailto: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.
Master of Science in Informatics at Grenoble (MOSIG 2016-2020)
