Introduction a la validation formelle avec TLA+ et Pluscal

Valider formellement un algorithme permet, de s’assurer que le design ne contient pas de faute de logique. Pour de petits algorithmes, il est plutôt simple d’avoir en tête la liste de tous les états possibles du systèmes. Mais lorsque l’on prend en compte de la concurrence ainsi que du non-déterminisme rajouté par le réseau, ce n’est pas possible d’avoir en tête l’entièreté des états possibles du système.

La Vérification Formelle est le fait de prouver l’exactitude d’un système par rapport à une spécification formelle et des propriétés, utilisant des méthodes formelles mathématiques. Il existe différents types de vérification formelle, certaines permettent de vérifier des algorithmes, d’autres des implémentations.

Il y a une différence à noter entre la vérification formelle et la validation formelle, qui sont souvent associés. La validation permet d’assurer que le produit spécifié correspond aux besoins, la vérification permet d’assurer que le produit est conforme aux spécifications.

Pour cette introduction, je vais me concentrer sur la validation formelle, plus spécifiquement sur TLA+ qui utilise le Model Checking, explorant tous les états possibles d’un système pour vérifier des propriétés..

TLA+

TLA + (Temporal Logic of Action) est un langage permettant de modéliser des programmes ou des systèmes, en particulier des programmes ou systèmes concurrents et distribués. Cet outil crée par Leslie Lamport est basé sur l’idée que la meilleure façon de décrire précisément un système est de le faire avec des mathématiques simples. C’est un outil de vérification formelle qui permet de détecter des erreurs fondamentales de design.

TLA+ se base sur la théorie des ensembles et définit un système ou programme comme un ensemble d’état possible du système ainsi qu’un ensemble de transitions entre ces états. Le TLA+ est écrit en langage formel, de logique et de mathématiques. La précision demandée des spécifications écrite dans ce langage permet de détecter les erreurs de design avant l’implémentation.

TLA+ en lui même est plutôt complexe, surtout lorsque l’on commence à vouloir modéliser des programmes avec de nombreuses transitions. Aussi TLA+ n’a pas une syntaxe très familière pour les développeurs, ce qui rend son apprentissage assez complexe.

TLA+ est extrêmement expressif et permet de décrire avec une précision très fine le fonctionnement d’un algorithme ou d’un système. Mais cette expressivité est son principal défaut car pour commencer à écrire des preuves, il faut énormément de connaissances et de pratique sur le langage. Modéliser un algorithme en TLA+ pur est beaucoup plus coûteux en temps, que ce soit pour l’apprentissage du langage et de l’outil, ou pour l’écriture de la spécification.

PlusCal

Pour simplifier cette tache pour les développeurs, Leslie Lamport a crée PlusCal¹, un langage de spécification qui compile vers TLA+. PlusCal ressemble plus à de la programmation impérative².

PlusCal possède beaucoup moins d’expressivité que TLA+, ce qui lui permet d’être plus simple a utiliser. PlusCal a été voulu qu’il s’écrive comme du pseudo code, avec deux syntaxes, une similaire à C et une similaire à Pascal. Ce qui permet aux développeurs à l’aise avec ces syntaxes, d’apprendre à écrire des spécifications plus rapidement.

Il y a plusieurs notions importantes dans PlusCal. C’est une langage “algorithmique”, c’est à dire que l’on décrit un algorithme avec des états et des transitions entre ces états. Chaque spécification PlusCal ne contient qu’un seul algorithme et il est uniprocess, c’est a dire qu’il n’a qu’un seul fil d’exécution. Pour que l’algorithme ait plusieurs fils d’exécution concurrents, il faut ajouter ce qu’on appelle des process.

Un process est un algorithme qui va être exécuté par un nombre de thread défini. Chaque process peut avoir entre 1 et N threads, et il peux y avoir plusieurs process différents dans un algorithme.

Par exemple, dans un service de compression vidéo, on peut imaginer un process qui télécharge une vidéo et la place dans un tampon, un process qui récupère une vidéo du tampon, qui la compresse et l’enregistre. On peut représenter ce service par un algorithme avec 2 process avec un nombre de thread défini pour chaque processus. L’intérêt de prouver un algorithme comme celui la serait de vérifier que le tampon ne déborde jamais et qu’il n’y a pas de problème de concurrence sur la lecture et l’écriture du tampon.

L’Équité dans PlusCal

Avant de modeliser un algorithme, il y a quelque chose de crucial a déterminer, comment un programme choisi quel état suivant choisir. L’algorithme défini les étapes qui peuvent être choisies, mais ne certifie pas que l’algorithme choisira de changer d’état. Il faut donc définir l’équité avec laquelle les transitions entre état se font.

Il y a deux types d’équité : l’équité faible et l’équité forte.

1. L’équité faible affirme que si la transition A est possible tout le temps, alors cette transition doit se produire.
2. L’équité forte affirme que si la transition A est possible, même si elle est non possible de nombreuses fois, alors cette transition devra se produire.

PlusCal permet de définir l’équité que ce soit au niveau de l’état, du processus ou de l’algorithme. PlusCal et TLA+ permettent donc de modéliser des systèmes ou programmes, et pour vérifier ces spécifications, il existe le TLC Model Checker. Il crée un modèle d’état fini à partir des spécifications TLA+ pour vérifier le système.

Le système est composé des variables de l’algorithme et tous les processus ainsi que leurs variables. Dans un état du système, on retrouve l’état de chaque processus, de ses variables, et l’état des variables de l’algorithme.

TLC construit le graphe à états du système en commençant par l’état initial. Puis parcours toutes les transitions possibles à partir de cet état initial et continue de manière récursive jusqu’à ce que tous les chemins possibles aient été explorés. Les transitions possible d’un état est construit par TLC, en évaluant l’ensemble des scénarios possibles, par exemple une transition par différent processus qui avance dans son graphe à états.

TLC nous permet donc de partir d’un seul graphe à états d’un processus ce qui est simple a modéliser pour un humain, a l’ensemble des transitions du système, au graphe des états accessibles du système entier, en prenant en compte chaque processus et chaque variable, ce qui est simple à déduire pour un ordinateur. Donc plus on met de processus en concurrence, plus le nombre d’état et le nombre de transitions augmente.

Et c’est lors de la création de ce graphe des états accessibles du système que TLC va vérifier la modélisation par rapport à la spécification.

Que vérifie TLC ?

TLC vérifie trois choses :

Il vérifie qu’il n’y a pas de deadlock; une situation de deadlock est quand un état ne possède aucune transition pour sortir de cet état. A noter qu’un deadlock est différent d’une fin prévue du programme.

Il vérifie des Invariants; un invariant est une formule mathématique qui doit être vraie pour chaque état possible du système (par exemple, pour notre base de données avec écrivain unique, un invariant est que le nombre de transaction ouvertes en écriture sur une base est inférieur ou égale a 1. ).

Il vérifie des Propriétés; c’est une propriété temporelle qui est vraie pour chaque exécution du système (avec le même exemple, une propriété est que chaque utilisateur qui veut ouvrir une transaction en écriture doit réussir à terme ).

Apprendre TLA+ et la modélisation formelle

On peut trouver sur internet des ressources pour apprendre TLA+ ainsi que la modélisation formelle. .Leslie Lamport propose un site web interactif avec plusieurs ressources très interessantes.

1. The TLA+ Video Course est un cours de 10 chapitre, chaqu’un contenant une vidéo ainsi que des exercices. Je recommande vivement cette ressource même si PlusCal suffirais pour votre cas d’usage. Ce cours permet de penser différement les interactions dans un programme, en faisant abstraction de l’implémentation exacte et en se concentrant sur son design.

2. The PlusCal Tutorial est un cours en 11 chapitre, avec pour chaque chapitre une explication sous format texte, avec des questions et réponses pour s’assurer de la comprehension. Ce cours permet de faire le tour de la syntaxe de PlusCal ainsi que de toutes ses possilibités.

Pour comprendre plus en profondeur la conception de la programmation de Leslie Lamport, je recommande aussi cette présentation de Leslie Lamport a Stanford en 2024.

Je trouve aussi les ressources d’Hillel Wayne très intéréssantes, en particulier cet article de blog portant sur le sujet de la représentation des files de messages en TLA+. Il est aussi le responsable du site (https://learntla.com)[https://learntla.com] qui présente TLA+ d’un autre angle que celui de Leslie Lamport, permettant une comprehension plus en profondeur.

J’ai pratiqué la validation formelle, TLA+ et PlusCal lors de mon passage chez Dassault Systèmes, j’ai écrit des spécifications pour valider des algorithmes et j’ai validé ces algorithmes, utilisant les ressources ci dessus pour me former.