С переходом к сервис-ориентированной сети круиз-контроль, удержание в полосе и стояночный тормоз требуют координации между множеством узлов. При колебаниях сетевых задержек и троттлинге процессоров возникают опасные состояния гонки. В статье показано применение формального model checking в TLA+.
В TLA+ безопасность доказывается не тестами, а универсальными инвариантами, верными для любого состояния. Для электропривода газа: при нажатии на тормоз тяга мотора обязана быть строго нулевой. Модельный чекер TLC перебирает миллионы состояний и при малейшем нарушении выдает пошаговую трассу ошибки.