05Portfolio
led-auto — brama BLE do Golfa IV
Raspberry Pi Zero 2 W dla Golfa IV: światło wejścia sterowane sygnałami z zamków, jedyne połączenie z taśmą LED i szyfrowany kanał do telefonu. Logikę sprawdza model checker na wszystkich osiągalnych stanach; brama jest już zamontowana w aucie.
W liczbach
- Własności w model checkerze
- 18
- Testy jednostkowe
- 154
- Wykryte mutacje
- 10/10
Problem
Sterownik taśmy LED w aucie przyjmuje po Bluetooth tylko jedno połączenie, więc telefon i drugi sterownik zaczęłyby się o nie bić. Nic nie mówi światłu, że drzwi właśnie się otwierają — fabryczny zamek daje tylko dwa gołe sygnały: pozycję rygla i stan drzwi. Do tego sterownik taśmy nie ma żadnego szyfrowania i nie zgłasza swojego stanu.
Podejście
Program w C++ na Pi Zero 2 W czyta cztery wejścia z zamków (dzielnik 10 kΩ / 2,2 kΩ, debounce 50 ms w jądrze) i jako jedyny trzyma połączenie z taśmą — przez surowe L2CAP, bez blokowania pętli sd-event. Telefon z aplikacją WireAmbi łączy się z Pi przez kanał WireLink (ECDH P-256, HKDF, AES-GCM, okno anty-replay), zgodny bajt w bajt z implementacją w Kotlinie. Parowanie to sześć kolorów na taśmie i w telefonie plus potwierdzenie drzwiami kierowcy. Rdzeń logiki nie ma wejścia-wyjścia, więc da się go sprawdzić wyczerpująco: model checker przechodzi 12,6 mln stanów i ok. 100 mln przejść, pilnując 18 własności — m.in. jednego zapisującego do taśmy, oszczędzania akumulatora i tego, że światło wejścia zawsze się zapali. Zdalny dostęp idzie przez szyfrowany przekaźnik i celowo nie pozwala odryglować auta.
Efekt
Brama przechodzi testy na stole — na prawdziwych wejściach zamka i z docelowymi czasami: otwarcie drzwi zapala światło wejścia, zamknięcie przywraca kolor z telefonu, zaryglowanie po wyjściu gasi wszystko. Pi jest przygotowane na nagłe odcięcie zasilania (watchdog sprzętowy, dziennik w RAM, start w ok. 30 s) i wróciło bez strat po trzech twardych resetach; kolejna próba to kilka dni bez prądu. Brama zajmuje ok. 11 MB RAM przy opóźnieniu pętli do 1 ms. Pi jest już zamontowane w aucie i współpracuje z panelem Android Auto, a kod do sterowania szybami, zamkiem i lusterkami czeka na sprzęt.