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.
Il est central aux thématiques de la filière Conception des systèmes autonomes intelligents. 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.
Objectifs pédagogiques
Diplôme(s) concerné(s)
- M2 PDS - Parallel and Distributed Systems
- M1 MPRI - Foudations of Computer Science
- Echanges PEI
- M1 CPS - Cyber Physical Systems
- M2 Cyber Physical System
- Titre d’Ingénieur diplômé de l’École polytechnique
- MScT-Internet of Things : Innovation and Management Program (IoT)
Parcours de rattachement
Format des notes
Numérique sur 20Littérale/grade réduitPour les étudiants du diplôme MScT-Internet of Things : Innovation and Management Program (IoT)
Le rattrapage est autorisé (Note de rattrapage conservée)- Crédits ECTS acquis : 4 ECTS
La note obtenue rentre dans le calcul de votre GPA.
Pour les étudiants du diplôme M2 Cyber Physical System
Le rattrapage est autorisé (Note de rattrapage conservée)Pour les étudiants du diplôme Titre d’Ingénieur diplômé de l’École polytechnique
Le rattrapage est autorisé (Note de rattrapage conservée)- Crédits ECTS acquis : 5 ECTS
Pour les étudiants du diplôme M1 CPS - Cyber Physical Systems
Le rattrapage est autorisé (Note de rattrapage conservée)Pour les étudiants du diplôme M1 MPRI - Foudations of Computer Science
Le rattrapage est autorisé (Note de rattrapage conservée)Pour les étudiants du diplôme M2 PDS - Parallel and Distributed Systems
Le rattrapage est autorisé (Note de rattrapage conservée)Pour les étudiants du diplôme Echanges PEI
Le rattrapage est autorisé (Note de rattrapage conservée)- Crédits ECTS acquis : 5 ECTS
Programme détaillé
Contenu
- Modèles et langages synchrones
- Introduction à la spécification et vérification de propriétés de modèles synchrones du point de vue de l’utilisateur
- Automates temporisés
- Logique temporelle et verification par model-checking
- Systèmes hybrides: modélisation, simulation, analyse de stabilité
- Systèmes hybrides: analyse d’atteignabilité
- Introduction à la vérification des réseaux de neurones et systèmes autonomes intelligents
Le cours est illustré par des exercices applicatifs, et par les séances de travaux pratiques utilisant différents outils de l’état de l’art pour modéliser et vérifier des cas d’étude réalistes (modèle synchrone de controleur de métro, modèle temporisé de pacemaker).
Dans une seconde partie du cours, des méthodes de vérification sont implémentés et expérimentées.
Le cours est évalué sur les rendus des TPs et un oral final (lecture et présentation d’article).