Habilitation Defense Uli Fahrenberg

From LRDE

Revision as of 10:19, 23 May 2022 by Daniela Becker (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)


Logo-cartouche- UP Saclay-CMJN.jpg Lrde.png Epita-logo-2.png 

SOUTENANCE D'HABILITATION A DIRIGER DES RECHERCHES
ULI FAHRENBERG
MARDI 10 MAI 2022
Université Paris-Saclay et via Zoom A 9H00



A Generic Approach to Quantitative Verification

Abstract:


Ce mémoire porte sur la vérification quantitative, c’est-à-dire la vérification des propriétés quantitatives des systèmes quantitatifs. Ces systèmes se retrouvent dans de nombreuses applications, et leur vérification quantitative est importante, mais aussi assez complexe. En particulier, étant donné que la plupart des systèmes trouvés dans les applications sont plutôt larges, il est alors essentiel que les méthodes soient compositionnelles et incrémentielles. Afin d’assurer la robustesse de la vérification, nous remplaçons les réponses booléennes de la vérification standard par des distances. Selon le contexte de l’application, de nombreux types de distances différentes sont utilisées dans la vérification quantitative. Par conséquent, il est nécessaire d’avoir une théorie générale des distances de systèmes qui puisse s’abstraire des distances concrètes, et de développer une vérification quantitative qui est indépendante de la distance. Nous sommes de l’avis que dans une théorie de la vérification quantitative, les aspects quantitatifs devraient être traités, tout autant que les aspects qualitatifs, comme des éléments d’entrée d’un problème de vérification. Dans ce travail, nous développons de la sorte une théorie générale de la vérification quantitative. Nous supposons comme entrée une distance entre traces, ou exécutions, puis utilisons la théorie des jeux à objectifs quantitatifs pour définir des distances entre systèmes quantitatifs. Différentes versions du jeu de bisimulation ( quantitatif ) donnent lieu à différents types de distances : distance de bisimulation, distance de simulation, distance d’équivalence de trace, etc., permettant de construire une généralisation quantitative du spectre temps linéaire–temps de branchement de van Glabbeek. Nous étendons notre théorie générale de la vérification quantitative à une théorie des spécifications quantitatives. Pour cela nous utilisons des systèmes de transitions modaux, et nous développons les propriétés quantitatives des opérateurs usuels pour les théories de spécifications. Tout cela est indépendant de la distance concrète entre les traces utilisée.


Manuscript


Composition du Jury :

  • Christel BAIER, Technische Universität Dresden, Allemagne, Rapportrice
  • Paul-André MELLIÈS, CNRS & Université Paris Denis Diderot, France, Rapporteur
  • Rob VAN GLABBEEK, The University of New South Wales, Australia, Rapporteur
  • Nathalie BERTRAND, Inria Rennes - Bretagne Atlantique, France, Examinatrice
  • Patricia BOUYER-DECITRE, CNRS & ENS Paris-Saclay, France, Examinatrice
  • Georg STRUTH, The University of Sheffield, Royaume Uni, Examinateur