A TLA+ specification for the Dexcom G7 continuous glucose monitoring system. Formally verifies the behavior and safety properties of the device’s state machine.
The TLA+ specification is on GitHub: https://github.com/EricSpencer00/tla-dexcom-g7
TLA+ Model of Dexcom G7
A formal TLA+ specification of the Dexcom G7 continuous glucose monitor's behavior and safety properties.