Je soutiendrai ma thèse le Mardi 24 Septembre à 14:00 dans la salle de conférence du pavillon des jardins Pavillon des Jardins, à l'ENS Paris-Saclay. Elle sera suivie du traditionnel "pot de thèse" à la cafétéria du Pavillon des Jardins.
Les systèmes digitaux jouent un rôle croissant dans le bon fonctionnement de notre société. Au delà de la grande diversité de leur domaines d'utilisations, on confie aujourd'hui des tâches importantes à des algorithmes. Déjà largement utilisés dans des domaines aussi délicat que le transport, la chirurgie ou l'économie, il est aujourd'hui de plus en plus question de faire de la place aux systèmes digitaux dans les domaines sociaux et politiques : vote électronique, algorithmes de sélection, profilage électoral... Pour les tâches confiées à des algorithmes, la responsabilité est déplacées de l'exécutant vers les concepteurs, développeurs et testeurs de ces algorithmes. Il incombe aussi aux chercheurs qui étudient ces algorithmes de proposer des techniques de vérifications fiable qui pourront être utilisées à tous les niveaux : conception, développement et test.
Les méthodes de vérifications formelles donnent des outils mathématiques pour prévenir des erreurs à chaque niveaux. Parmi elle, le diagnostic d'erreur consiste en la création d'un diagnostiqueur basé sur un modèle formel du système à vérifier. Le diagnostiqueur est exécuté en parallèle du système qu'il doit surveiller et prévient un contrôleur si il détecte un comportement dangereux du système. Pour les systèmes modélisés par des automates temporisés, il n'est pas toujours possible de construire un diagnostiqueur sous la forme d'un autre automate temporisé. En effet les automates temporisés, introduits par Alur&Dill dans les années 90 et largement étudiés et utilisés depuis pour modéliser des systèmes avec contraintes temporelles, ne sont pas déterminisable.
Une machine plus puissante qu'un automate temporisé peut cependant être utilisée pour construire le diagnostiqueur d'un automate temporisé comme le montre Tripakis en 2002. L'aboutissement de ce travail de thèse est la construction automatique d'un diagnostiqueur pour les automates temporisés à une horloge. Ce diagnostiqueur, dans le même esprit que celui de Tripakis, est une machine plus puissante qu'un automate temporisé.
La partie I du manuscrit introduit un cadre formel pour ce type de machine et plus généralement pour la modélisation et la déterminisation de systèmes quantitatifs. Y est introduit le modèle des automates sur structures temporisés, qui apporte un nouveau point de vue sur la manière de modéliser les systèmes avec variables quantitatives. La partie II étudie le problème de la déterminisation des automates sur structures temporises, et plus spécifiquement celui des automates temporisés qui peuvent se traduire dans ce cadre nouveau cadre formel. La partie III montre comment utiliser les automates sur structure temporisés pour construire de manière générique un diagnostiqueur pour les automate temporisés à une horloge. Cette technique est implémentée dans un outils, DOTA, et comparée à la machine construite par Tripakis