TLA+

Carte Commune · n° 333631

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+ remplit 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 modèle 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...

Lire sur Wikipédia · Image Edward Lamport, MIT