v2.11.0 (5976)

Programme d'approfondissement - CSC_52070_EP : Logical verification of hybrid systems

Domaine > Informatique.

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)

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 20

Littérale/grade réduit

Pour 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)
    L'UE est acquise si note finale transposée >= C
    • Crédits ECTS acquis : 5 ECTS

    La note obtenue rentre dans le calcul de votre GPA.

    Programme détaillé

    1. Langages de modélisation pour les systèmes hybrides
    2. Diverses logiques de spécifications formelles
    3. Théories décidables (ou non)
    4. SMT pour l'arithmétique réelle non-linéaire: méthodes symboliques et numériques
    5. Invariants différentiels: méthodes de preuve
    6. Invariants différentiels: génération automatique
    7. Vérification de modèles de systèmes hybrides
    8. Monitorat de systèmes hynrides
    9. Synthèse symbolique de controle
    Veuillez patienter