Recherche
Mes intérêts de recherche et domaines d'intérêt.
Systèmes de Cybersécurité
Recherche sur les méthodes formelles appliquées à la cybersécurité, analyse des protocoles de sécurité et développement de techniques de vérification pour les systèmes sécurisés.
Systèmes Cyber-Physiques
Modélisation et vérification de systèmes intégrant des processus informatiques et physiques, garantissant la sécurité et la fiabilité dans les applications critiques.
Systèmes Distribués
Modélisation et vérification des systèmes distribués, en se concentrant sur les protocoles, les algorithmes et les techniques de vérification formelle pour les systèmes concurrents.
Systèmes Temps Réel
Recherche sur la modélisation, la vérification et l'analyse des systèmes temps réel utilisant des automates temporisés et des spécifications de logique temporelle.
Systèmes Embarqués Critiques
Développement de techniques de vérification formelle pour les systèmes embarqués dans des domaines critiques pour la sécurité, garantissant l'exactitude et la fiabilité.
Automates Temporisés
Recherche fondamentale sur les automates temporisés avec horloges partiellement indépendantes, développement de nouveaux modèles et algorithmes de vérification pour les systèmes temps réel.
Logiques Temporelles
Recherche sur les logiques temporelles pour spécifier et vérifier les propriétés des systèmes temps réel et distribués, y compris TCTL et autres formalismes temporels.
Simulation et Bisimulation
Développement de relations d'équivalence et de techniques de raffinement pour les systèmes temporisés et distribués utilisant la théorie de simulation et bisimulation.
Vérification de Modèles
Application de techniques de vérification de modèles utilisant des outils comme UPPAAL et SCADE pour vérifier l'exactitude des systèmes temps réel et distribués.
Méthodes Formelles
Application de techniques mathématiques et de spécifications formelles pour concevoir, développer et vérifier les systèmes logiciels et matériels avec des garanties de correction rigoureuses.
Démonstration de Théorèmes
Recherche sur la démonstration interactive de théorèmes et les assistants de preuve pour vérifier les propriétés complexes des systèmes temps réel et des modèles d'automates.
Tests Basés sur des Modèles
Développement de méthodologies de test dérivées de modèles formels pour générer automatiquement des cas de test pour des systèmes complexes et des lignes de produits logiciels.
Tests de Mutation
Recherche sur les techniques de tests de mutation pour évaluer la qualité des suites de tests et améliorer l'efficacité des tests dans les systèmes hautement configurables.
Lignes de Produits Logiciels
Recherche sur la modélisation de la variabilité, les tests de systèmes hautement configurables et la mise à l'échelle de l'analyse de variabilité dans les lignes de produits logiciels.
Analyse et Représentation Symbolique
Développement de techniques symboliques et de structures de données pour l'analyse et la vérification efficaces de grands espaces d'états dans les systèmes temporisés et distribués.