eSpark a utilisé TLA+ pour prouver qu'aucune conception ne satisfaisait les 3 règles, puis en a abandonné une

eSpark Learning, fournisseur de technologies éducatives pour les écoles primaires, exécutait un processus de configuration manuel et semi-régulier pour chaque client, qui coordonnait plusieurs systèmes tiers et modifiait directement les réseaux informatiques des clients. À mesure que la base d'utilisateurs croissait, la charge de travail est devenue intenable — l'équipe de support a réalisé qu'elle aurait besoin d'une nouvelle embauche à temps plein chaque année rien que pour suivre le rythme. La direction avait toujours jugé l'automatisation du processus trop dangereuse : une erreur pouvait toucher le réseau d'un client et coûter le contrat.

L'ingénieur Hillel Wayne avait récemment utilisé la spécification formelle (dans le style TLA+) sur un projet de téléversement par lots et avait gagné une semaine de livraison en détectant des bugs d'architecture avant d'écrire le code. Le chef de projet avait défini trois propriétés que le remplacement automatisé devait garantir pour être sûr. Wayne a modélisé le système dans un langage de spécification et l'a fait passer par un vérificateur de modèles, qui simule de manière exhaustive chaque scénario qu'une spécification autorise et renvoie une trace concrète lorsqu'il en trouve un qui enfreint une règle.

Après deux jours de modélisation, toutes les conceptions échouaient soit immédiatement, soit à cause d'un défaut subtil qui pouvait rester inaperçu en production pendant des mois avant de s'effondrer. Certaines conceptions satisfaisaient deux des trois propriétés requises, mais aucune ne satisfaisait les trois. Plutôt que d'en choisir une quand même en espérant que ça passe, Wayne a fait entrer le chef de projet dans les artefacts de modélisation, lui a montré concrètement comment chaque conception échouerait, et lui a demandé de quelle propriété l'entreprise pouvait se passer.

Des experts en conception internes ont déterminé qu'une propriété n'avait besoin d'être vérifiée qu'habituellement, et non toujours. Une fois ce seul compromis circonscrit, le vérificateur de modèles a confirmé que plusieurs conceptions fonctionneraient désormais, et l'équipe en a construit une. Le service de configuration automatisé a fonctionné sans incident pendant des années par la suite, survivant au mandat des ingénieurs qui l'ont construit.

Le vérificateur de modèles a prouvé qu'aucune conception ne satisfaisait les 3 règles ; négocier

La modélisation dans un langage de spécification est peu coûteuse à jeter ; une base de code largement construite ne l'est pas, donc tester chaque idée de conception avant l'implémentation a évité de perdre du temps d'ingénierie.

Un vérificateur de modèles renvoie une trace d'échec concrète, ce qui est plus convaincant pour une partie prenante non ingénieure qu'un avertissement de risque abstrait.

Mettre en évidence « aucune de ces conceptions ne satisfait les trois exigences » avant d'écrire du code a transformé une hypothèse implicite et non examinée en une décision explicite que le chef de projet pouvait réellement prendre.

Quand chaque conception que vous essayez semble échouer, modélisez d'abord formellement l'espace. Un vérificateur de modèles transforme un sentiment vague de risque en un compromis précis et négociable que vous pouvez soulever avant d'écrire la moindre ligne de code.

Le service de gestion de configuration automatisé a fonctionné efficacement pendant des années, bien au-delà des mandats des ingénieurs qui l'ont construit. Wayne a ensuite travaillé à temps plein comme consultant en spécification formelle et a écrit sur cette pratique, notamment un livre sur le sujet et des travaux de documentation pour le langage de spécification Alloy.