단일 기능 ECU에서 중앙 집중형 서비스 지향 아키텍처(SOA)로 전환됨에 따라 어댑티브 크루즈 컨트롤, 차선 유지, 전자식 주차 브레이크와 같은 기능들은 여러 컴퓨팅 노드 간의 복잡한 분산 핸드셰이크를 수반합니다. 패킷 지터와 CPU 스로틀링이 맞물릴 때 발생하는 치명적 동시성 결함을 TLA+ 정형 모델 체킹으로 사전 검증하는 방안을 제시합니다.
TLA+에서 소프트웨어 안전성은 몇 가지 단위 테스트 통과로 입증되지 않습니다. 엔지니어는 모든 도달 가능한 시스템 상태에서 반드시 참이어야 하는 전역 불변성(Universal Invariant)을 수학적으로 정의합니다. 전자식 스로틀 시스템의 경우, 브레이크 페달이 밟혀 있을 때 모터 출력 토크는 반드시 0이어야 합니다. TLC 모델 체커는 수백만 가지의 상태 전이 경로를 전수 탐색하여 안전 불변성을 단 한 번이라도 위반하는 실행 트레이스를 정확히 적출해 냅니다.