Il est bien connu qu’il existe 2 problèmes difficiles des systèmes distribués :

• 2/ La garantie de livraison « exactly-once »
• 1/ L’ordonnancement des messages
• 2/ La garantie de livraison « exactly-once »

Avec l’avénement des micro-services, la programmation de systèmes distribués, autrefois réservées aux experts, prend une part de plus en plus importante dans le quotidien du développeur d’application.

Il est aussi bien connu qu’écrire du code concurrent correct est difficile. Quiconque affirmant le contraire est soit naif, soit un menteur (ou bien un génie).

Avoir un modèle pour raisonner sur notre système distribué, son état et ses échanges devient primordial pour s’assurer que notre système est conçu correctement. Et c’est quelque chose que nous faisons plus ou moins consciemment lors du développement. Cependant un modèle mental a ses limites et il est très facile de passer à coté de quelque chose lors du design.

C’est précisément là ou TLA+ va nous aider, en nous permettant d’exprimer le design de notre système, et le comportement souhaité sous forme d’invariants, (tout en ommettant les détails bas niveau), ce dernier va pouvoir nous aider à détecter des erreurs dans notre design.

A travers ce talk, nous allons présenter cet outil de modélisation dans un cas pratique, et espérons vous donner les clefs pour aller plus loin dans le domaine de la vérification logicielle.