Con il passaggio da centraline isolate a reti orientate ai servizi, funzioni come il cruise control o il freno di stazionamento esigono il consenso tra molteplici nodi. Con jitter di rete e throttle delle CPU nascono bug subdoli. Vi presentiamo il model checking formale con TLA+.
In TLA+, la sicurezza non viene validata tramite semplici test di regressione. L'ingegnere specifica invarianti universali che devono risultare veri in qualsiasi stato raggiungibile. Per l'acceleratore: premere il freno impone coppia zero al motore. TLC analizza milioni di transizioni e isola la traccia di qualsiasi violazione.