TLA+

Cet article est une ébauche concernant l’informatique théorique.

Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.

TLA+, acronyme de « Temporal Logic of Actions » (« logique temporelle des actions » en anglais), est un langage de méthode formelle développé by Leslie Lamport. Il est utilisé pour la conception, la modélisation, la documentation et la vérification de programmes, en particulier les systèmes distribués et concurrents. Le pseudo-code du langage TLA+ est considéré comme exhaustivement testable. Il peut aussi servir à générer des représentations visuelles (blueprints) de systèmes logiciels.

Pour la conception et la documentation, TLA+ rempli le même besoin que d'autres spécifications techniques. Toutefois, les spécifications TLA+ sont écrites dans un langage formel logique et mathématique, et la précision des spécifications ainsi écrites permettent de découvrir des erreurs de conception de systèmes avant leur implémentation. Le vérificateur de model trouve tous les comportements possibles du système jusqu'à un nombre prédéfini d'étapes d'exécution et les examine pour des violations de propriétés d'invariance de sécurité et en fonctionnement. Les spécifications TLA+ utilisent une théorie des ensembles basique pour définir la sécurité (rien de mal ne va arriver) et la logique temporelle pour définir l'activité en fonctionnement (de bonne chose vont éventuellement arriver).