Le Pôle Modèles forme le cœur de l’activité du LMF en matière de construction et d’analyse de modèles computationnels. Il regroupe trois thématiques étroitement liées — Model Checking et Synthèse, Systèmes Concurrents et Distribués, et Systèmes Critiques — qui couvrent un large éventail de problématiques liées à la modélisation formelle des systèmes discrets et hybrides.
Les travaux menés visent à développer des modèles abstraits à la fois expressifs et traitables algorithmiquement, capables de représenter des propriétés essentielles des systèmes : contraintes temporelles, phénomènes stochastiques, concurrence, interactions avec un environnement physique, ou encore présence humaine dans la boucle décisionnelle. L’objectif central est d’identifier les cadres de modélisation les plus adaptés à la spécification, la vérification et la synthèse de systèmes complexes.
Chaque thématique apporte une perspective complémentaire à cet effort commun :
- Model Checking et Synthèse explore comment la correction des systèmes peut être établie par vérification automatique, et comment on peut dériver automatiquement des implémentations à partir de spécifications formelles. Les sujets abordés incluent les automates temporisés et pondérés, les logiques de spécification, la surveillance et la prédiction dans les systèmes à événements discrets, les méthodes de synthèse fondées sur la théorie des jeux, ainsi que l’analyse algorithmique de systèmes à états infinis.
- Systèmes Concurrents et Distribués étudie le comportement et la coordination de composants interagissant avec une connaissance locale partielle. Les axes de recherche comprennent les automates distribués et la théorie des traces, les protocoles d’accord dans les réseaux dynamiques, les techniques d’analyse fondées sur le dépliage des réseaux de Petri, et la modélisation de phénomènes physiques comme la métastabilité.
- Systèmes Critiques se concentre sur les systèmes exigeant des garanties élevées de sûreté et de fiabilité, notamment dans les domaines des transports, de l’énergie et du contrôle embarqué. Les recherches portent sur les systèmes cyber-physiques, la conception et la vérification de fonctions de conduite automatisée, l’interaction homme–machine, ainsi que l’ingénierie de modèles métier intégrés à des environnements de simulation.
L’activité du Pôle Modèles s’inscrit dans un dialogue actif avec d’autres axes de recherche, notamment sur l’intelligence artificielle et la biologie synthétique.