Mit dem Umstieg auf serviceorientierte Architekturen erfordern Tempomat, Spurhalteassistent und Handbremse Handshakes ueber viele Knoten hinweg. Latenzen und CPU-Throttling fuehren zu heimtueckischen Fehlern. Dieser Artikel zeigt, wie TLA+-Model-Checking Seriensoftware schuetzt.
In TLA+ beweist man Sicherheit nicht ueber Beispielfaelle, sondern durch universelle Invarianten. Fuer ein Drive-by-Wire-System gilt etwa: Betraetigt der Fahrer die Bremse, muss das Drehmoment zwingend null sein. Der TLC-Model-Checker prueft Millionen Zustaende und liefert bei Verstoessen den genauen Ablauf.