Descriptif
Les logiques sont des langages universels qui permettent de spécifier de manière mathématiquement précise le comportement de systèmes, mais aussi de guider le développement d'algorithmes complexes pour garantir leur sûreté et leur contrôle. La richesse de ces logiques est d'autant plus cruciale pour des systèmes complexes, pour lesquels de nombreux phénomènes différents doivent être pris en compte (temporalité, incertitudes, connaissances, concurrence).
Dans ce cours, nous nous intéresserons particulièrement aux logiques utiles à l'analyse de systèmes hybrides, c’est-à-dire de systèmes soumis à la fois à des dynamiques physiques continues et à du contrôle numérique de systèmes informatiques, comme par exemple les véhicules autonomes. Nous explorerons la richesse des logiques et des langages de modélisation dans ce contexte, et nous ferons un tour d'horizon des méthodes formelles basées ou guidées par ces logiques.
Objectifs pédagogiques
Les objectifs sont multiples :
- Apprendre à modéliser des systèmes et à spécifier des problèmes dans des langages riches (logiques, langages de modélisation)
- Développer un socle solide pour des algorithmes de base mais essentiels en méthodes formelles logiques (ex. : SMT)
- Découvrir une variété de méthodes formelles pour l'analyse, la vérification et le contrôle de systèmes hybrides basées sur la logique
- Se faire la main sur quelques outils informatiques du domaine (Z3, KeYmaera X)
Diplôme(s) concerné(s)
Pour les étudiants du diplôme Programmes d'échange internationaux
Aucun.
Suivre les cours CSC_51075_EP et CSC_51051_EP en P1 est un plus.
Pour les étudiants du diplôme Titre d’Ingénieur diplômé de l’École polytechnique
Aucun.
Suivre les cours CSC_51075_EP et CSC_51051_EP en P1 est un plus.
Format des notes
Numérique sur 20Littérale/grade réduitPour les étudiants du diplôme Programmes d'échange internationaux
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
La note obtenue rentre dans le calcul de votre GPA.
Programme détaillé
- Langages de modélisation pour les systèmes hybrides
- Diverses logiques de spécifications formelles
- Théories décidables (ou non)
- SMT pour l'arithmétique réelle non-linéaire: méthodes symboliques et numériques
- Invariants différentiels: méthodes de preuve
- Invariants différentiels: génération automatique
- Vérification de modèles de systèmes hybrides
- Monitorat de systèmes hynrides
- Synthèse symbolique de controle