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.
Visionner mon exposé de soutenance.
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.
