Cours : N8EN08A - Systèmes de transitions

Aperçu des sections

Systèmes de transitions

Installation de la TLA+ Toolbox (pour les TP en local) : https://lamport.azurewebsites.net/tla/toolbox.html
Sur les machines école, /mnt/n7fs/tla/toolbox/toolbox (cf README du premier sujet de TP).
Autre fonctionnement : plugin TLA+ pour Visual Studio Code. Éditeur plus agréable mais moins de finesse dans les paramètres de vérification.

Planning:

C1	21/01	système de transitions
TD1	23/01	TLA+ actions partie 1
TD2	29/01	TLA+ actions partie 2
TP1	31/01	missionnaires et cannibales
C2	12/02	L'équité
C3	14/02	logique temporelle LTL
TD3	18/02 ou 19/02	TLA+ logique
TD4	19/02 ou 21/02	exclusion mutuelle, Peterson
TD5	26/02	exclusion mutuelle avec jeton
C4	28/02	logique temporelle CTL
TP2	04/03	exclusion mutuelle avec jeton
C5	05/03	outil de vérif + démo preuve
TP3	11/03 ou 12/03	philosophes
TP4	14/03	vchan
TP5	18/03 ou 19/03	vchan (suite)
Examen	09/04

TLA+, c'est encore Leslie Lamport qui en parle le mieux...

Supports de cours
- CH1 - Systèmes de transitions Fichier
  
  327.7 Ko
- CH2 - TLA+ : les actions (la partie modèle de TLA+) Fichier
  
  325.7 Ko
- CH3 - L'équité dans les systèmes de transitions Fichier
  
  281.8 Ko
- CH4 - Logique temporelle linéaire LTL Fichier
  
  276.5 Ko
- CH5 - TLA+ : la logique et l'équité Fichier
  
  266.9 Ko
- CH6 - Logique temporelle arborescente CTL Fichier
  
  266.4 Ko
- CH7 - vérification de propriétés Fichier
  
  313.8 Ko
- CH8 - conclusion Fichier
  
  73.9 Ko
- L'intégralité en 4 transparents par page Fichier
  
  1.2 Mo
Support de cours avec audio
- Les supports de certaines séances sont accompagnés de commentaires audio.
- CH1 - Systèmes de transitions Fichier
  
  13.1 Mo Archive (ZIP)
- CH3 - L'équité dans les systèmes de transitions Fichier
  
  35.4 Mo Archive (ZIP)
- CH4 - Logique temporelle linéaire LTL Fichier
  
  26.3 Mo Archive (ZIP)
- CH6 - Logique temporelle arborescente CTL Fichier
  
  26.5 Mo Archive (ZIP)
Supports de TP
- TP1 - le problème des missionnaires et des cannibales Fichier
  
  290.0 Ko
- TP2 - l'exclusion mutuelle avec jeton circulant Fichier
  
  20.0 Ko
- TP3 - le problème des philosophes Fichier
  
  10.0 Ko
- TP4-5 - protocole de communication Xen vchan Fichier
  
  240.0 Ko
Annales d'examens
- Les corrections présentes avec les sujets sont parfois des éléments sommaires pour donner une idée de la correction. Une réponse complète devrait contenir des explications supplémentaires.
- 2014-2015 Fichier
  
  465.7 Ko
- 2015-2016 Fichier
  
  242.2 Ko
- 2016-2017 Fichier
  
  389.3 Ko
- 2017-2018 Fichier
  
  640.3 Ko
- 2018-2019 Fichier
  
  469.6 Ko
- 2020-2021 Fichier
  
  385.6 Ko
- 2021-2022 Fichier
  
  479.1 Ko
- 2022-2023 Fichier
  
  482.0 Ko
- 2023-2024 Fichier
  
  518.9 Ko

Aperçu des sections

Systèmes de transitions

TLA+, c'est encore Leslie Lamport qui en parle le mieux...

Supports de cours

Support de cours avec audio

Supports de TP

Annales d'examens