TLA+
Cette page est une très courte ébauche oubliée.
À l'instar du célèbre « Une pomme est un fruit » qui a marqué l'histoire de Wikipédia, n'hésitez pas à la développer (comment ?)
Vous pouvez également enrichir les pages proposées dans la rubrique « Pommes à croquer » du bistro du jour.
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 specifications techniques. Toutefois, les specifications TLA+ sont écrites dans un language formel logique et mathematique, 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).
Notes et références[modifier | modifier le code]
