Lab de méthodes formelles : Z3, SPIN, TLA+ et Alloy dans une VM

Ce lab donne à chaque élève quatre outils de vérification dans une VM Ubuntu. Un test montre qu’une conception marche sur les cas essayés. Une méthode formelle demande à une machine d’examiner tous les cas et de prouver la propriété ou de rendre un contre-exemple. Les élèves utilisent Z3, un solveur, SPIN, un vérificateur de modèles pour Promela, TLA+ avec son vérificateur TLC, et Alloy, chacun sur un petit problème.

Rien n’est installé sur l’ordinateur de l’élève. Les outils sont les vrais, et le README du lab donne les problèmes et aucune réponse.

Ce que les élèves apprennent

Ce que veut dire vérifier une conception au lieu de l’essayer, en quatre parties. Avec Z3, ils énoncent les règles d’un planning d’examens, puis une affirmation que les règles rendent vraie et que Z3 prouve en constatant que son contraire n’a aucune solution. Avec SPIN, ils trouvent dans une trace une course entre deux processus, puis écrivent un verrou pour qu’il ne reste aucune erreur. Avec TLA+, ils écrivent l’invariant qui dit à quoi sert un verrou, lisent le contre-exemple que TLC affiche pour un verrou qui ne verrouille pas, et le corrigent. Avec Alloy, ils lisent un contre-exemple dessiné en personnes et en amitiés, et réparent le modèle par un nouveau fait.

L’exécuter dans le navigateur

Les labs VM se règlent comme une tâche Lab dans un module, et l’exemple est sur la page du lab. La machine est petite : un processeur, 1 Go de mémoire et 10 Go de disque. Chaque outil Java est limité à 128 Mo et l’ensemble tient largement. Z3 et SPIN n’ont besoin que de l’archive d’Ubuntu. TLA+ et Alloy sont téléchargés depuis GitHub, que ne joint pas une VM d’invité sans compte : ces deux parties demandent une VM avec un compte connecté.

  1. Ajouter le lab. Dans un module que vous enseignez, ajoutez une tâche et choisissez la carte Lab VM Ubuntu. La page affiche une courte description de la machine au lieu d’un fichier compose.
  2. Partir de l’exemple. La page propose des labs prêts à l’emploi pour démarrer. Choisissez Formal methods. Utiliser un exemple remplace le texte, et Annuler rend le vôtre.
  3. Publier et démarrer votre propre copie. Publiez, puis Démarrez. Le script setup du lab installe Z3, SPIN et un environnement Java depuis l’archive d’Ubuntu, télécharge TLA+ et Alloy depuis leurs versions publiées sur GitHub et vérifie chaque fichier avec une somme de contrôle fixe, au premier démarrage de la VM, en quelques minutes.
  4. Ouvrir le terminal. Ouvrez son terminal et lisez README.md dans le dossier personnel : il dit quoi faire en quatre parties et ne donne aucune réponse.

Une leçon de base sur ce lab

Formal Methods Basics est une petite leçon travaillée dans ce lab, qui est une VM Ubuntu. Elle comporte une accroche, un objectif « Je peux », des mots-clés, un point de départ, une vérification après chaque idée, une erreur fréquente et une vérification finale, et chaque étape a un bouton Exécuter qui tape sa commande dans le terminal de la machine. L’élève pose à Z3 une question à laquelle il peut répondre et une autre non, laisse SPIN trouver la course dans le modèle du lab et la rejoue, lit le contre-exemple que TLC affiche pour un invariant faux d’un verrou correct, et voit une instance d’Alloy.

La leçon regarde autour d’elle et laisse à l’élève les tâches propres du lab : elle ne donne donc aucune réponse.

Comment il est noté

Le lab a une vérification, qui croit les outils et jamais les mots de l’élève. Z3 compare lui-même les règles du planning de l’élève à celles du README : une réponse écrite à la main ou une règle manquante échoue, et l’affirmation doit découler des règles sans être vraie sans elles. SPIN exécute le verrou de l’élève dans un cadre propre à la vérification, et le verrou ne peut nommer rien de ce qui appartient au cadre. TLC exécute le verrou corrigé avec l’invariant de la vérification et celui de l’élève, les deux processus doivent pouvoir entrer, et l’invariant de l’élève doit être violé par le verrou défaillant fourni : un invariant TRUE échoue. Alloy ouvre le modèle de l’élève depuis un fichier à lui, avec ses propres assertions, qui doivent tenir, et une exécution qui doit encore trouver un groupe d’amis. La première ligne affichée dit pourquoi.

  1. Le distribuer. Attribuez le lab comme n’importe quelle tâche, avec une échéance si vous le souhaitez. Chaque élève reçoit une VM à lui, conservée d’une séance à l’autre s’il a un compte.
  2. Lancer la vérification. Sur la ligne d’un élève dans la liste de la classe, appuyez sur Lancer la vérification. Elle démarre une copie de sa machine enregistrée, qui n’est pas sauvegardée ensuite, exécute le script de vérification du lab en root et indique s’il a réussi, ce qu’il a affiché et quand. L’élève n’est pas informé du résultat.
  3. Noter. Lisez la première ligne de ce que la vérification a affiché : elle nomme la partie et dit ce qui ne va pas, par exemple une règle que Z3 trouve manquante, un verrou où SPIN trouve encore une erreur, un invariant qui ne détecte pas le verrou défaillant, ou un modèle qui a encore un contre-exemple. Renvoyez le travail avec un motif s’il faut aller plus loin.

La définition sur GitHub

Le fichier est toute la définition du lab, le texte même que la plateforme exécute : taille, script setup, commandes d’aide, README et vérification. Copiez-le et changez les problèmes pour faire un lab plus long.

Essayer ce lab, et ce qu’il coûte

Un compte personnel gratuit permet de suivre les leçons de base de ce lab, avec chaque mois assez de crédit gratuit pour suivre la plupart des leçons, sans carte. Pour une classe, un établissement a ses 365 premiers jours gratuits pour 50 élèves au plus, puis paie par élève et par an, tous les labs compris et les enseignants gratuits.

Questions fréquentes

Le lab nécessite-t-il une licence ?
Non. Z3 est sous licence MIT, SPIN sous BSD, les outils TLA+ sous MIT et Alloy sous Apache 2.0, avec des solveurs sous leurs propres licences libres dans son jar. Ils sont installés sur la VM de l’élève au démarrage, et nous n’en distribuons aucun.
Un élève sans compte peut-il le faire ?
Les parties un et deux, Z3 et SPIN, oui. Une VM sans compte ne joint que l’archive d’Ubuntu, donc TLA+ et Alloy n’y sont pas téléchargeables. La VM d’un élève connecté joint GitHub et reçoit les quatre.
Les élèves peuvent-ils abîmer quelque chose ?
Seulement leur propre copie. Les outils vérifient des modèles et n’exécutent rien d’autrui. Si un élève abîme un fichier, la copie d’origine est dans /usr/share/formallab.
Le lab a-t-il été testé dans une vraie VM d’élève ?
Le script setup, les commandes de la leçon et la vérification ont été exécutés dans un vrai Ubuntu 26.04 en conteneur à la place de la VM, et la vérification a été vue échouer à chaque façon de tricher sur chaque partie et réussir avec la solution de référence. Une VM d’élève réellement démarrée, et le téléchargement par le proxy de la plateforme, valent un essai avant un cours.