Description
Date depot: 1 janvier 1900
Titre: Modélisation et analyse de systèmes de transport automatiques
Directrice de thèse:
Béatrice BÉRARD (LIP6)
Encadrant :
Claude DUTHEILLET (LIP6)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
La conception et la réalisation de systèmes automatiques de transport posent de nombreux problèmes de fiabilité et de sécurité. Pour de tels systèmes complexes et répartis, une des approches possibles est de concevoir des stratégies de contrôle afin de garantir des propriétés comme l'évitement des collisions ou l'obtention de marges de sécurité, et d'inclure ces stratégies dans les mécanismes d'assistance à la conduite automatisée.
Le travail proposé consiste à étudier les différents modèles existants pour ces systèmes et à poursuivre l'approche fondée sur la recherche de contrôleur. Un premier objectif est d'utiliser pour cela les ITS (Instantiable Transition Systems), une technologie développée dans l'équipe MoVe, qui permet le codage efficace d'espace d'états par des diagrammes de décision hiérarchiques. Une implémentation de la recherche de contrôleur dans ce cadre fournira une solution générale qui pourra ensuite être appliquée aux systèmes de transports automatisés.
Dans cette modélisation, la représentation du temps est simplifiée pour obtenir un modèle discret comportant deux étapes qui alternent : celles qui sont contrôlées et les autres. Un deuxième objectif consiste à intégrer une notion explicite de temps dans les modèles traités, par exemple en utilisant des automates temporisés. Ces automates manipulent des variables qui évoluent avec le temps, et qui peuvent être testées et remises à zéro lors de transitions discrètes. Les nombreux travaux menés sur ce modèle depuis une quinzaine d'années ont montré qu'il possédait de bonnes propriétés, à la fois sur le plan de l'expressivité et pour les résultats d'analyse qui y ont été obtenus. En particulier, le problème de l'accessibilité est décidable, même en temps dense. Le travail prévu étendra la recherche de contrôleur dans ce cadre temporisé et réparti. Une activité de validation de cette approche doit également être menée, sur l'exemple du système d'autoroute automatique.
Doctorant.e: Zhang Yan