Eric Spencer
projects
This TLA+ spec models a sensor, transmitter, receiver, expiry, and alerts as an abstract state machine inspired by a Dexcom G7. It is an educational formal-methods exercise, not device validation or medical advice.
It is one of three TLA+ specs, alongside the walk-in oven and laptop models. The interactive microwave spec is a friendlier on-ramp for a reader who has never used TLA+.
In this model, the sensor has a ten-day lifetime, a 30-minute warmup, five-minute samples, a BLE connection to a receiver, and a 12-hour grace period after expiration.
g7.tla models all of that as a state machine. The state variables look like this:
VARIABLES
now, \* elapsed minutes since sensor insertion
sensorState, \* "NotInserted" | "Warmup" | "Active" | "Expired"
lastSample, \* most recent sample produced by the sensor
receiverStore, \* sequence of samples stored on the receiver
connected, \* BLE connection status
alerts \* { high: BOOL, low: BOOL }
The actions are the things the device can do: InsertSensor, FinishWarmup, ProduceSample, ConnectOrDisconnect, TransmitSample, UpdateAlerts, ClearAlerts, ExpireSensor, and a Tick that advances now by one minute. Transmission is nondeterministic, since packets can be delivered or dropped: in practice the phone is often in another room and the BLE link is unreliable.
There are two config files. g7.debug.cfg shrinks everything (lifetime 10 minutes, glucose values 80 to 82) so TLC can finish in a second. g7.realistic.cfg uses real numbers: 30-minute warmup, 10-day lifetime, 12-hour grace, glucose range 40 to 400. The realistic one explodes the state space.
The safety property that matters most is NoReadingsAfterExpiry:
NoReadingsAfterExpiry ==
\A i \in 1..Len(receiverStore) :
receiverStore[i].time <= LIFETIME_MINS + GRACE_MINS
In English: nothing should land in the receiver's store with a timestamp past the modeled expiration. The counterexample is a property of this abstraction; it does not describe a production device or a patient's care.
Running TLC against the debug config catches this. The model surfaces a state where lastSample gets produced and stored after the sensor should have moved to Expired, because ExpireSensor and ProduceSample race on the same tick. That is the point of writing the spec: the invariant is not satisfied by the current model, and the trace says where to tighten it.
A lot. The spec does not model calibration (the G7 mostly does not need it, but the API surface still exists). It does not model the signal loss state when the transmitter and receiver are out of range for too long. It does not model the difference between the sensor producing a sample and the transmitter packaging it for BLE. Alerts are a single high/low flag instead of the hysteresis the device actually uses: Dexcom will not refire the low alert if the wearer is already in low territory and has not climbed back out. There is no model of the predictive "you'll be low in 20 minutes" alerts.