Al migrar de ECUs individuales a redes orientadas a servicios, funciones como el control de crucero y el freno de mano exigen acuerdos entre varios procesadores. Con congestión de red o caídas de frecuencia en CPUs, aparecen fallos extraños. Introducimos el model checking formal en TLA+.
En TLA+, la seguridad no se prueba pasando tests. El ingeniero define invariantes que deben cumplirse en todo estado alcanzable. En el acelerador electrónico, la regla dicta: si se pisa el freno, el par motor debe ser cero. El verificador TLC analiza millones de casos y muestra la traza si halla un fallo.