Aller au menu Aller au contenu
Une voie, plusieurs choix
Informatique et Mathématiques appliquées
Une voie, plusieurs choix

> Formation > Cursus ingénieur

Modèles et langages pour le model checking (en anglais) - 5MMMVSC7

A+Augmenter la taille du texteA-Réduire la taille du texteImprimer le documentEnvoyer cette page par mail cet article Facebook Twitter Linked In
  • Volumes horaires

    • CM : 18.0
    • TD : -
    • TP : -
    • Projet : -
    • Stage : -
    • DS : -
    Crédits ECTS : 1.5
  • Responsables : Frederic LANG

Objectifs

Ce cours présente des méthodes et des outils pour la conception fiable des systèmes constitués d'agents (ou processus) s'exécutant en parallèle de manière asynchrone et possiblement soumis à des contraintes de temps-réel. Ces méthodes et outils répondent aux besoins des telecoms (protocoles de télécommunication), du logiciel (algorithmique répartie, cloud computing, ...) des systèmes embarqués et du matériel (architectures multi-processeurs, protocoles d'arbitrage, protocoles de cohérence de caches, circuits asynchrones, architectures GALS, ...). Les méthodes se basent sur une description formelle du système dans un langage approprié, qui peut être automatiquement validée par des outils mettant en oeuvre des techniques de vérification telles que le model checking ou l'equivalence checking.

Contenu

Concepts de base du parallélisme asynchrone et du temps-réel;
Modèles formels : automates communicants, automates temporisés, algèbres de processus;
Techniques de vérification formelle par model checking et equivalence checking);
Logique temporelle.

Prérequis

Des connaissances sur les langages de programmation.

Contrôles des connaissances

CONTRÔLE CONTINU :
Type d'évaluation (ex : TP, assiduité, participation) : pas de contrôle continu.

SESSION NORMALE :
Type d'examen (écrit, oral, examen sur machine) : écrit
Salle spécifique : non
Durée : 2h
Documents autorisés (ex : aucun, résumé feuille A4 manuscrite, dictionnaires, tous documents) : tous documents
Documents interdits (ex : livres, tous documents) : aucun
Matériel (ex : calculatrices): aucun

  • matériel autorisé, préciser :
  • matériel interdit, préciser :
    Commentaires :

SESSION DE RATTRAPAGE :
Type d'examen (écrit, oral, examen sur machine) : oral
Salle spécifique : non
Durée : 30 minutes
Documents autorisés (ex : aucun, résumé feuille A4 manuscrite, dictionnaires, tous documents) : tous documents
Documents interdits (ex : livres, tous documents) : aucun
Matériel (ex : calculatrices): aucun

  • matériel autorisé, préciser :
  • matériel interdit, préciser :
    Commentaires :

Si participation à la SESSION DE RATTRAPAGE, la note finale est la note de l'examen de la SESSION DE RATTRAPAGE.
Sinon, la note finale est la note de l'examen de la SESSION NORMALE.

L'examen existe uniquement en anglais FR

Calendrier

Le cours est programmé dans ces filières :

  • Cursus ingénieur - Filière ISI - Semestre 9 (ce cours est donné uniquement en anglais EN)
cf. l'emploi du temps 2020/2021

Informations complémentaires

Code de l'enseignement : 5MMMVSC7
Langue(s) d'enseignement : FR

Le cours est rattaché aux structures d'enseignement suivantes :

Vous pouvez retrouver ce cours dans la liste de tous les cours.

Bibliographie

H. Garavel. Défense et illustration des algèbres de processus. In Zoubir Mammeri (Ed), Actes de l'Ecole d'été Temps Réel ETR 2003 (Toulouse, France), Institut de Recherche en Informatique de Toulouse, septembre 2003.
http://www.inrialpes.fr/vasy/Publications/Garavel-03.html

S. Merz and N. Navet (Eds). Modeling and Verification of Real-Time Systems. Wiley, 2008.

A+Augmenter la taille du texteA-Réduire la taille du texteImprimer le documentEnvoyer cette page par mail cet article Facebook Twitter Linked In

mise à jour le 18 juin 2017

Université Grenoble Alpes