L’Ecole doctorale : Ecole Doctorale de l’Institut Polytechnique de Paris
et le Laboratoire de recherche SAMOVAR – Services répartis, Architectures, Modélisation, Validation, Administration des Réseaux
présentent
l’AVIS DE SOUTENANCE de Monsieur Evgenii VINARSKII
Autorisé à présenter ses travaux en vue de l’obtention du Doctorat de l’Institut Polytechnique de Paris, préparé à l’Institut Polytechnique de Paris Télécom SudParis en :
Mathématiques et Informatique
« Machines à états finis temporisées avec délais de sortie : identification d’état et applications dans les systèmes et réseaux distribués »
le JEUDI 5 NOVEMBRE 2026 à 10h00
à
Amphithéâtre 6
19 Place Marguerite Perey, 91120 Palaiseau
Membres du jury :
Mme Natalia KUSHIK , Maîtresse de conférences, Télécom SudParis / Institut Polytechnique de Paris, FRANCE – Directrice de thèse
M. Djamal ZEGHLACHE, Professeur, Télécom SudParis / Institut Polytechnique de Paris, FRANCE – CoDirecteur de these
Mme Olga KOUCHNARENKO, Professeure, Université Marie et Louis Pasteur, FRANCE – Rapporteur
M. Thomas CHATAIN, Maître de conférences, ENS Paris-Saclay, FRANCE – Rapporteur
M. Olivier BARAIS, Professeur, Université de Rennes, FRANCE – Examinateur
M. Uli FAHRENBERG, Professeur, Université Paris-Saclay, FRANCE – Examinateur
M. Mohamed SELLAMI, Maître de conférences, Télécom SudParis / Institut Polytechnique de Paris, FRANCE – Examinateur
« Machines à états finis temporisées avec délais de sortie : identification d’état et applications dans les systèmes et réseaux distribués »
présenté par Monsieur Evgenii VINARSKII
Résumé :
Les séquences d’identification d’état pour les machines à états finis (Finite State Machines, FSMs) ont fait l’objet de nombreuses recherches au cours des dernières décennies. Les séquences de synchronisation (synchronizing and homing sequences) permettent de ramener une FSM non initialisée dans un état courant connu, tandis que l’état initial peut être déterminé au moyen d’une séquence de distinction (distinguishing sequence). De nombreuses méthodes ont été proposées pour vérifier l’existence de ces séquences d’identification d’état et en permettre la synthèse. Bien que les FSMs classiques soient largement utilisées pour modéliser le comportement des systèmes réactifs, elles ne sont pas suffisamment expressives pour représenter leur comportement temporel, notamment les délais de traitement, les interactions asynchrones, les conditions de compétition (race conditions) ou d’autres phénomènes dépendants du temps. C’est pourquoi plusieurs modèles temporisés ont été proposés et étudiés. Dans cette thèse, nous étudions les machines à états finis temporisées (Timed Finite State Machines, TFSMs) avec délais de sortie, dans lesquelles chaque transition entrée/sortie est enrichie d’une garde temporelle et d’un délai de sortie. Ce modèle permet de représenter des procédures concurrentes tout en préservant la structure des FSMs classiques pour la modélisation du comportement des systèmes réactifs. Cette thèse s’intéresse au problème de l’identification d’état dans les TFSMs avec délais de sortie et met en évidence l’intérêt des séquences d’identification d’état pour améliorer la fiabilité et l’efficacité des systèmes de réseaux distribués et des infrastructures d’informatique en nuage (cloud computing). Dans une première partie, nous introduisons formellement les séquences de synchronisation pour les TFSMs avec délais de sortie et en étudions les propriétés. Les similitudes et les différences entre les séquences de synchronisation dans les modèles temporisés et non temporisés sont analysées. Nous développons également des algorithmes permettant de vérifier l’existence de telles séquences pour une TFSM avec délais de sortie et d’en effectuer la synthèse. Dans une deuxième partie, ces séquences sont exploitées afin de prévenir les problèmes de concurrence et de réduire le temps d’exécution des requêtes dans un environnement de cloud computing, les résultats étant validés par une évaluation expérimentale. La troisième partie est consacrée aux séquences de distinction pour deux TFSMs avec délais de sortie initialisées. Nous en proposons une définition formelle, étudions leurs propriétés et développons des algorithmes permettant de vérifier leur existence ainsi que d’en réaliser la synthèse. Dans la quatrième partie, nous examinons l’applicabilité des séquences de distinction proposées au test basé sur les modèles (model-based testing). Plus précisément, nous dérivons des suites de tests garantissant une couverture de fautes vis-à-vis des défauts liés au temps, tels que les problèmes de concurrence ou le positionnement incorrect des temporisations (timeouts). L’efficacité des approches proposées est validée au moyen d’une évaluation expérimentale. Cette thèse apporte ainsi une contribution au domaine de l’identification d’état des modèles temporisés en démontrant l’applicabilité pratique des séquences de synchronisation et de distinction pour améliorer la fiabilité et l’efficacité des systèmes de réseaux distribués et de cloud computing, ainsi que pour dériver des suites de tests de haute qualité offrant une couverture garantie contre les fautes liées aux contraintes temporelles.
Abstract :
State identification sequences for Finite State Machines (FSMs) have been extensively studied in the past decades. Synchronizing and homing sequences bring a non-initialized FSM to the known current state, while the initial state can be determined when a distinguishing sequence is applied. A number of methods have been proposed for the existence check and derivation of the state identification sequences. Although classical FSMs are widely-used to model the behavior of reactive systems, they are not expressive enough to represent their time-dependent behavior, such as processing delays, asynchronous interactions, race conditions, etc. Correspondingly, timed state models have been proposed and studied. In this thesis, we investigate Timed Finite State Machines (TFSMs) with output delays, where each input/output transition is augmented with a timed guard and an output delay. Such a model enables the representation of concurrent procedures while preserving the structure of classical FSMs when modeling the behavior of reactive systems. In this thesis, the state identification problem for TFSMs with output delays is studied, and the effectiveness of using state identification sequences is shown for improving the reliability and efficiency of distributed networking and cloud computing systems. In the first part, we formally introduce synchronizing and homing sequences for TFSMs with output delays and study their properties. The similarities and differences between synchronizing and homing sequences for timed and untimed state models are investigated. We also develop algorithms for checking the existence and derivation of synchronizing and homing sequences for a TFSM with output delays. In the second part, TFSM synchronizing and homing sequences are applied for preventing concurrency and minimizing the request execution time in a cloud computing environment with relevant experimental evaluation. The third part is devoted to distinguishing sequences for two initialized TFSMs with output delays. We formally define such sequences, investigate their properties, and develop algorithms for checking the existence of such sequences and their derivation. In the fourth part, the applicability of the proposed distinguishing sequences to model-based testing is considered. In particular, we derive test suites with the guaranteed fault coverage against time-related faults, such as concurrency issues and wrongly-placed timeouts. The effectiveness of the proposed approaches is validated through an experimental evaluation. The thesis therefore contributes to the state identification for timed state models demonstrating the practical applicability of synchronizing, homing and distinguishing sequences for improving the reliability and efficiency of distributed networking and cloud computing systems, as well as for deriving high-quality test suites against time-related faults.