05Portfolio
led-auto — a BLE gateway for a Golf IV
A Raspberry Pi Zero 2 W for a Golf IV: entry lighting driven by the door-lock signals, the only connection to the LED strip and an encrypted channel to the phone. A model checker verifies the logic across every reachable state; the gateway is now fitted in the car.
By the numbers
- Model-checked properties
- 18
- Unit tests
- 154
- Mutations caught
- 10/10
Problem
The LED strip controller in the car accepts a single Bluetooth connection, so a phone and a second controller would end up fighting over it. Nothing tells the lights that a door is opening — the factory lock exposes just two bare signals: latch position and door state. On top of that, the strip controller has no encryption and never reports its state.
Approach
A C++ program on the Pi Zero 2 W reads four lock inputs (10 kΩ / 2.2 kΩ divider, 50 ms debounce in the kernel) and is the only thing that talks to the strip — over raw L2CAP, without blocking the sd-event loop. The phone running WireAmbi connects to the Pi over the WireLink channel (ECDH P-256, HKDF, AES-GCM, anti-replay window), byte-for-byte compatible with the Kotlin implementation. Pairing shows six colours on the strip and on the phone, then you confirm by opening the driver’s door. The logic core has no I/O, so it can be checked exhaustively: the model checker walks 12.6 million states and about 100 million transitions against 18 properties — a single writer to the strip, sparing the car battery, and an entry light that always comes on, among others. Remote access goes through an encrypted relay and deliberately cannot unlock the car.
Outcome
The gateway passes bench tests — on real lock inputs and with the target timings: opening a door switches on the entry light, closing it brings back the colour set on the phone, and locking the car after getting out turns everything off. The Pi is prepared for sudden power loss (hardware watchdog, journal in RAM, boot in about 30 s) and came back clean from three hard resets; the next test is several days without power. The gateway uses about 11 MB of RAM with loop latency of 1 ms or less. The Pi is now fitted in the car and works with the Android Auto panel, while the code for the windows, central lock and mirrors is waiting for the hardware.