Thématiques de Recherche


Depuis septembre 2013, je suis maître de conférences à l'université de Nantes/LS2N, dans l'équipe AeLoS.


Je travaille dans le domaine du design et de la vérification de systèmes complexes. En particulier, mes points d'intérêt principaux sont:

  • Le Model Checking Statistique et ses extensions;
  • Les théories d'asbtraction stochastiques;
  • Les théories d'interfaces pour systèmes temporisés, stochastiques, adaptifs;
  • Les Systèmes de systèmes (SoS);
  • Les systèmes (probabilistes) paramétrés
  • La modélisation et la vérification de systèmes naturels incertains
  • ...

Habilitation à diriger des recherches



J'ai soutenu mon HDR le 10 décembre 2020 à l'université de Nantes.

Modélisation et vérification de systèmes incertains

Benoît DELAHAYE - Université de Nantes / LS2N


Le but des sciences en général est d'étudier le fonctionnement de systèmes complexes afin de mieux les comprendre et, éventuellement, de pouvoir prédire leur comportement futur. Une part importante de cette étude est la réalisation d'un modèle, objet abstrait qui représente fidèlement les connaissances existantes à propos du système, et qui pourra alors être étudié et simulé à la place du système lui-même. Malheureusement, il est fréquent que les connaissances existantes à propos des systèmes soient incomplètes ou sujettes à incertitudes. Il est alors important d'inclure ces incertitudes à l'intérieur des modèles et de développer des techniques afin d'automatiser l'analyse de ces modèles. Ce document présente quatre contributions au domaine de la modélisation et de l'analyse de tels systèmes. Deux de ces contributions sont à vocation plutôt théorique et proposent des langages de modélisation permettant d'inclure les incertitudes à l'intérieur des modèles ainsi que des techniques de vérification associées. Les deux autres contributions sont plus pratiques, l'une proposant une technique de vérification statistique et prouvant son efficacité sur un cas d'étude industriel, et l'autre proposant une technique de construction automatique de modèle à partir d'un ensemble de données ainsi qu'une analyse de son niveau de sécurité.


Télécharger le document, les slides.



Doctorat



J'ai soutenu ma thèse le 8 octobre 2010 à l'IRISA, Rennes.

Spécification Modulaire et Analyse Compositionnelle
de Systèmes Stochastiques

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


Cette thèse présente des contributions originales pour la conception et la vérification de systèmes non-déterministes et stochastiques. Nos résultats sont divisés selon trois lignes directrices. Premièrement, nous généralisons la théorie des interfaces au cas stochastique, en s'appuyant sur le formalisme classique des chaînes de Markov à intervalles pour construire la première théorie de spécification compositionnelle pour systèmes stochastiques : les chaînes de Markov à contraintes. Deuxièmement, nous étendons la notion de contrats hypothèse-garantie et développons une théorie compositionnelle à base de contrats pour systèmes stochastiques, pour laquelle nous proposons des notions quantitatives de raffinement et de satisfaction. Finalement, nous proposons une méthodologie pour la vérification de systèmes complexes, basée sur une abstraction stochastique. Cette méthodologie, combinée avec le model-checking statistique, est appliquée avec succès à un cas d'étude industriel.


Télécharger le document, les slides.