UE Models and languages for model checking

Informations aux utilisateurs

Veuillez noter que vous consultez une page du catalogue de formation 2020-2021. Le recrutement est actuellement terminé pour les licences, licences professionnelles, masters, DUT et formations réglementées de santé. Pour consulter le catalogue des formations 2021-2022, cliquez sur le lien suivant.

Diplômes intégrant cet élément pédagogique :

Descriptif

This lecture presents methods and tools for the correct design of systems consisting of agents (or processes) running asynchronously in parallel, possibly subject to real-time constraints. These methods and tools respond to the needs of telecoms (telecommunication protocols), software (distributed algorithms, cloud computing, ...), embedded systems, and hardware (multiprocessor architectures, arbitration protocols, cache coherency protocols, asynchronous circuits, GALS architectures, ...). The methods rely on a formal description of the system in an appropriate language, which can be automatically validated by tools implementing verification techniques, such as model checking or equivalence checking.

Contents :

Basic concepts of asynchronous concurrency and real-time
Formal models: communicating automata, timed automata, process algebras
Formal verification techniques (model checking, equivalence checking)
Temporal logic

Pré-requis recommandés

Some knowledge of programming languages.

Compétences visées

  • 1 Définir et organiser le travail à effectuer pour répondre à un besoin ou une demande
    • 1.2 Définition des spécifications
      • 1.2.1 Méthodologie et langages :E Maths discrètes & fondement de l'info
  • 2 Réaliser une solution efficiente en réponse à un besoin ou une demande
    • 2.2 Développement de solutions
      • 2.2.3 Formaliser : E Maths discrètes & fondement de l'info
  • 3 Mettre en œuvre des processus de validation
    • 3.2 Mise en œuvre et exploitation
      • 3.2.1 Validation théorique : E Maths discrètes & fondement de l'info
      • 3.2.2 Éprouver la qualité : E Maths discrètes & fondement de l'info
      • 3.2.3 Définir une batterie de tests : E Maths discrètes & fondement de l'info
  • 5 Formaliser des problèmes complexes
    • 5.2 Création d’architectures logicielles
      • 5.2.1 Décomposer un système complexe en sous-systèmes : E Maths discrètes & fondement de l'info
      • 5.2.2 Construire et raisonner sur des abstractions : E Maths discrètes & fondement de l'info

Informations complémentaires

Méthode d'enseignement : En présence
Langue(s) : Anglais