I will defend my thesis on Tuesday 24th September, 2019, at 14:00 in the conference room of the Pavillon des Jardins, at the ENS Paris-Saclay. It will be followed by the traditional "pot de thèse" at the cafeteria of the Pavillon des Jardins.
Digital system are now part of our society. They are used in a wide range of domains and in particular they have to handle delicate tasks. Already used in domains such as transportation, surgery or economy, we speak now of using digital systems for social or political matters : electronic vote, selection algorithms, electoral profiling... For task handled by algorithm, the responsibility is moved from the executioner to the designer, developer and tester of those algorithms. It is also the responsibility of computer scientists who study those algorithms to propose reliable techniques of verification which will be applicable in the design, the development or the testing phase.
Formal verification methods provide mathematical tools to prevent executions error in all phases. Among them, fault-diagnosis consist on the construction of a diagnoser based on a formal model of the system we aim to check. The diagnoser runs in parallel with the real system and emit a warning any time it detect a dangerous behavior. For systems modeled by timed automata, it is not always possible to construct a timed automaton to diagnose it. Indeed timed automata, introduce in the nineties by Alur&Dill and widely studied and used since to model timed systems, are not determinizable.
A machine, more powerful than a timed automaton, can still be used to construct the diagnoser of a timed automaton as it is done in Tripakis in 2002. This thesis work aim at constructing a diagnoser for any one-clock timed automata. This diagnoser is constructed with the help of a machine more powerful than timed automata, following the idea of Tripakis.
Part I of this thesis introduce a formal framework for the modeling of quantitative systems and the study of their determinization. In this framework we introduce automata on timed structures, the model used to construct the diagnoser. Part II study the determinization problem of automata on timed structures, and particularly the one of timed automata determinization in this framework. Part III illustrate how automata on timed structures can be used to construct in a generic way a diagnoser for one clock timed automata. This technique is implemented in a tool, DOTA , and is compared to the technique used by Tripakis in his work.