Descriptif

L'interaction de composantes informatiques, qui calculent et communiquent, avec leur environnement régi par des lois physiques, comme pour un avion ou un système médical implanté, est au centre du domaine émergent des systèmes cyber-physiques. Parmi les défis posés par ces systèmes auxquels nous nous intéresserons, l'utilisation croissante d'algorithmes d'intelligence artificielle (réseaux de neurones typiquement), que ce soit pour la perception ou le contrôle.

Maitriser la modélisation, le contrôle et la vérification du comportement de tels systèmes est crucial pour garantir l'efficacité, les fonctionnalités et la fiabilité de ces systèmes, toujours plus complexes et le plus souvent critiques en terme de sécurité ou de coût.

Le cours s'attachera à trouver un équilibre entre modélisation et vérification, et entre fondations théoriques et les aspects pratiques. Il introduira notamment aux principes et à l'utilisation de quelques outils représentatifs de l'état de l'art, et s'intéressera à des cas d'étude réalistes (notamment un modèle temporel de pacemaker modélisé et vérifié avec l'outil Uppaal).

Le cours est central aux thématiques de la filière Design of Intelligent Autonomous Systems, mais il est également naturel dans le parcours Electrical Engineering ou dans les filières The Internet of Everything for a Digitized Society (IOE4DS) ou Algorithms and Foundations of Programming Languages. Des sujets de projets 3A en lien avec des thématiques peuvent être proposés. 

Contenu:

1. Introduction, modèles et langages synchrones
2. Langages synchrones: spécification et vérification
3. Automates temporisés
4. Logique temporelle et verification par model-checking 
5. Modélisation et simulation de systèmes hybrides
6. Analyse d'atteignabilité de systèmes hybrides
7. Stabilité et contrôle de systèmes hybrides
8. Sureté des systèmes autonomes intelligents

Le cours est illustré par des exercices applicatifs (en cours), et par les séances de travaux pratiques utilisant différents outils de modélisation et vérification. Les quatre dernières séances sont dédiées à un projet, dans lequel l'accent pourra être mis, au choix des étudiants, sur la modélisation et vérification d'un système cyber-physique, ou sur l'étude plus poussée d'un aspect d'une méthode de vérification. 

Le cours sera validé pour une petite moitié sur les TPs, et la grosse moitié restante sur le projet et l'oral associé.

Langue d'enseignement :

Les documents sont en anglais, les cours sont donnés en français par défaut, en anglais sur demande