Com a mudança de ECUs isoladas para redes orientadas a serviços, funções como piloto automático e freio de mão exigem coordenação entre múltiplos nós. Se um nó sofre atraso na rede e outro reduz o clock, surgem falhas raras. Apresentamos a verificação formal com TLA+ para carros.
No TLA+, a segurança não é testada por cenários comuns. O engenheiro escreve regras universais que nunca podem falhar. No acelerador eletrônico, a regra é: pedal de freio pressionado implica torque zero no motor. O TLC avalia milhões de passos. Se houver qualquer falha em uma interrupção, ele gera o rastreamento exato do erro.