분산된 차량 ECU 사이의 경쟁 상태(Race Condition)는 기존 단위 테스트로 포착하기 어려운 간헐적 시스템 오류를 유발합니다. 차량 전원 제어, OTA 펌웨어 전환 및 제동 핸드오버 로직을 TLA+ 정형 수학 명세로 모델링함으로써, 발생 가능한 수억 가지 동시 실행 시퀀스 전반에서 교착 상태(Deadlock)가 없음을 수학적으로 증명합니다.
회생 제동에서 유압 마찰 제동으로 전환되는 순간 ABS가 개입하는 복합 상황을 가정해 보겠습니다. 모터 제어기가 유압 펌프의 가압 완료를 지레짐작하고 회생 토크를 차단했으나, 유압 밸브가 초기화 중이었다면 80ms 동안 차량 감속도가 0으로 떨어질 수 있습니다. TLA+ 정형 모델링은 하드웨어 제작 전 이 비동기 상태 불일치를 완벽하게 찾아내어 수정했습니다.