Avec la transition vers des architectures orientées services, le régulateur adaptatif et le frein de parking requièrent des négociations entre plusieurs calculateurs. Si le réseau hésite et qu'un processeur régule sa charge, des bugs critiques surgissent. Découvrez la vérification formelle TLA+.
Avec TLA+, la sécurité ne se vérifie pas par de simples assertions de tests. L'ingénieur formule des invariants universels devant être vrais dans chaque état. Pour l'accélérateur, la règle interdit tout couple si le frein est actionné. Le vérificateur TLC passe au crible des millions d'états pour prouver l'absence de faille.