- TLA+ est un langage destiné à modéliser les logiciels à un niveau supérieur au code, et à modéliser le matériel à un niveau supérieur aux circuits
- Il fournit un environnement de développement intégré (IDE) permettant d’écrire et de vérifier des modèles
- L’outil le plus utilisé par les ingénieurs est le model checker TLC, et un vérificateur de preuves est également disponible
- TLA+ repose sur les mathématiques et ne ressemble à aucun langage de programmation
- Pour la plupart des ingénieurs, il est plus simple de commencer avec PlusCal qu’avec TLA+
- Les modèles TLA+ sont généralement appelés des "spécifications (Specification)". Dans l’introduction ci-dessous, ils sont appelés
modèles
PlusCal
- PlusCal est un langage pour écrire des algorithmes, en particulier des algorithmes parallèles et distribués
- Il sert à écrire des algorithmes sous forme de code précis et testable plutôt que de pseudo-code
- Il ressemble à un langage de programmation simple et fournit des constructions pour exprimer la concurrence et la non-détermination
- Il est très expressif, car il permet d’utiliser des formules mathématiques comme expressions
- Les algorithmes PlusCal sont convertis en modèles TLA+ et peuvent être vérifiés avec les outils TLA+
- Comme il ressemble à un langage de programmation, il est facile à apprendre, mais TLA+ est mieux adapté à la structuration de modèles complexes
Qu’est-ce qu’un modèle ?
- Les ordinateurs et les réseaux obéissent à des lois physiques continues, mais il est naturel de modéliser leur comportement comme un ensemble d’événements discrets
- Aucun modèle ne décrit parfaitement un système réel ; un modèle ne décrit que certains aspects du système dans un but donné
- TLA+ est un langage de modélisation fondé sur l’état, qui représente l’exécution d’un système comme une séquence d’états
- Un événement est représenté par une paire de deux états consécutifs, appelée une "étape" (
step)
- Un système est modélisé comme un ensemble d’actions décrivant toutes les exécutions possibles
Modéliser au-delà du niveau du code
- TLA+ sert à modéliser les systèmes à un niveau supérieur au code
- Par exemple, l’algorithme d’Euclide peut être décrit comme une procédure de calcul du plus grand commun diviseur (GCD), et non comme du code
- définir la variable x à M, et y à N
- soustraire de manière répétée la plus petite des deux valeurs x et y à la plus grande
- répéter jusqu’à ce que x et y deviennent égaux, et cette valeur est le GCD
- Une telle description omet des détails comme le type des variables ou la gestion des exceptions, et n’exprime que l’idée essentielle de l’algorithme
- Si l’on se concentre uniquement sur le codage, il est difficile de trouver de bons algorithmes → une pensée abstraite est nécessaire
- La plupart des programmeurs commencent à coder sans modèle de haut niveau, ce qui entraîne des erreurs de conception
- TLA+ est un langage de modélisation de haut niveau qui permet de décrire clairement le comportement du code et sa manière d’opérer
- Plus un système est complexe, plus la simplification est importante ; elle ne s’obtient pas par la technique de codage, mais par une pensée de niveau supérieur
- Dans un projet industriel, la modélisation avec TLA+ a permis de réduire d’un facteur dix la taille du code d’un système d’exploitation temps réel
- La modélisation est efficace pour détecter les erreurs de conception en amont et plus fiable que les tests ou les corrections du code
Modélisation des systèmes concurrents
- Un système concurrent se compose de plusieurs composants (processus) qui fonctionnent simultanément
- Un système distribué est constitué de processus spatialement séparés qui communiquent par messages
- TLA+ modélise l’état global de l’ensemble du système comme un état global
- D’après plus de 40 ans d’expérience, modéliser les systèmes distribués à partir d’un état global est l’approche la plus généralement utile
Machine à états (State Machine)
- TLA+ définit un ensemble de comportements à l’aide des deux éléments suivants :
- condition initiale : spécifie les états de départ possibles
- relation de transition : spécifie les étapes possibles (paires d’états consécutifs)
- L’ensemble des comportements qui satisfont ces deux conditions constitue le modèle
- Ce type de modèle est appelé une machine à états (state machine)
- Une machine à états finis (finite-state machine) est une machine à états dont le nombre d’états est fini
- Une machine de Turing est un exemple de machine à états ; pour une machine de Turing déterministe, chaque état a au plus un état suivant
- Une manière pratique de décrire précisément la sémantique d’un langage de programmation consiste à le traduire en machine à états au moyen d’une sémantique opérationnelle
- L’action de transition ne spécifie que les étapes qui peuvent se produire ; cela ne signifie pas qu’elles doivent nécessairement se produire
- Pour indiquer qu’une étape doit nécessairement se produire, il faut ajouter une propriété d’équité (fairness property)
- Même sans équité, cela suffit pour trouver des erreurs de commission, mais pas des erreurs d’omission
- Dans la plupart des cas, les erreurs sont surtout des erreurs de commission, et les débutants devraient commencer par écrire la condition initiale et la relation de transition
Vérification des propriétés
- On écrit un modèle pour vérifier si un système se comporte comme souhaité
- Les outils TLA+ permettent de vérifier si le modèle satisfait une propriété donnée pour tous les comportements possibles
- Exemple : même si l’exécution se termine normalement dans 99 % des états initiaux, il faut vérifier que toutes les exécutions se terminent normalement
- La propriété la plus courante est l’invariance (invariance property), qui doit toujours être vraie dans tous les états
- Un modèle avec des propriétés d’équité doit aussi vérifier des propriétés de vivacité (liveness property) → par exemple : l’exécution se termine nécessairement
- Des propriétés plus complexes peuvent être exprimées comme des machines à états, et l’on peut vérifier si une autre machine à états les implémente
- Dans TLA+, il n’existe pas de distinction formelle entre machine à états et propriété : les deux sont exprimées de la même manière, sous forme de formule mathématique
- Dire qu’une machine à états en implémente une autre signifie que la formule correspondante est logiquement incluse
- En pratique, on ne vérifie le plus souvent que l’invariance et quelques propriétés simples de vivacité, mais comprendre des concepts plus complexes aide aussi à prévenir les erreurs dans le code
Le langage TLA+ lui-même
- TLA+ est un langage fondé sur les mathématiques et ne ressemble pas à un langage de programmation
- Les programmeurs étant plus familiers des langages de programmation que des expressions mathématiques, cela peut sembler difficile au début
- Mais en réalité, les mathématiques sont plus expressives qu’un langage de programmation
- Exemple : on peut définir le GCD comme le plus grand entier positif qui divise deux nombres (sans préciser la méthode de calcul)
- Une définition mathématique permet de ne conserver que l’essentiel nécessaire à l’objectif et d’abstraire les détails d’implémentation inutiles
- La procéduralisation n’apporte pas d’abstraction ; elle ne fait que cacher le code ailleurs
- PlusCal convient bien pour débuter avec TLA+, et même les utilisateurs expérimentés le préfèrent pour les modèles simples
- Mais pour penser mathématiquement et faire de la modélisation de haut niveau, il est important d’apprendre TLA+ lui-même
3 commentaires
https://cacm.acm.org/research/… C’est bien utilisé chez AWS.
Coder n’est pas programmer
Comme cela a été mentionné dans cet article, je suis allé me renseigner.
Moi aussi, je l’ai découvert pour la première fois dans cet article, alors j’étais en train de faire des recherches dessus.