Research topics

I am now an associate professor at University of Nantes/LS2N in the AeLoS team.


I work on design and verification of complex systems. My main interests lie in:

  • Statistical Model Checking and its extensions;
  • Stochastic Abstraction;
  • Interface theories for timed/stochastic/adaptive systems;
  • Systems of Systems (SoS);
  • Software Product Lines (SPL);
  • (Probabilistic) Parametric Systems;
  • Modeling and verification of natural uncertain systems;
  • ...

Habilitation


I defended my habilitation the 10th of december 2020 at Université de Nantes.

Modeling and verification of systems with uncertainties

Benoît DELAHAYE - Université de Nantes / LS2N

The goal of science in general is to study the functioning of complex systems in order to better understand them and potentially to be able to predict their future behaviour. An important part of this study is the realization of a model, an abstract object that faithfully represents existing knowledge about the system, and which can then be studied and simulated instead of the system itself. Unfortunately, existing knowledge about systems is often incomplete or subject to uncertainties. It is then important to include these uncertainties in the models and to develop techniques to automate the analysis of these models. This document presents four contributions to the field of modeling and analysis of such systems. Two of these contributions are somewhat theoreticaly-oriented, proposing modeling languages to include uncertainties in models and associated verification techniques. The other two contributions are more practical, one proposing a statistical verification technique and proving its efficiency on an industrial case study, and the other proposing a technique for automatied model construction from a data set and an analysis of its security level.


Download the dissertation, the slides.
Watch my presentation.



PhD


I defended my PhD thesis the 8th of october 2010 at IRISA, Rennes.

Modular Specification and Compositional Analysis
of Stochastic Systems

Benoît DELAHAYE - S4 Team - Université de Rennes 1 / IRISA

This thesis presents new contributions in the design and verification of systems mixing both non-deterministic and stochastic aspects. Our results can be divided into three main contributions. First, we generalize interface theories to the stochastic setting. We build upon the known formalism of Interval Markov Chains to develop Constraint Markov Chains, the first fully compositional specification theory for stochastic systems. Second, we extend the notion of assume-guarantee contracts and develop a contract-based theory for stochastic systems, proposing quantitative notions for satisfaction and refinement. Finally, we propose a methodology for the verification of complex systems. This methodology is based on a stochastic abstraction of the environment where two components are working, allowing to verify the components individually. Combined with statistical model checking, this methodology is successfully applied to the verification of an industrial case study.


Download the dissertation, the slides.