Formal Verification of a SCUBA Dive Computer
This repository contains formal methods associated with our EMSOFT 2019 paper Verifiably safe SCUBA diving using commodity sensors: work-in-progress
SCUBA diving is an activity in which divers remain underwater for prolonged periods by using a self-contained breathing apparatus. Diving is safety critical because changing depth too rapidly or running out of oxygen before surfacing can result in life-threatening consequences. These risks are currently minimized by using a wrist-mounted, 'air-integrated' dive computer that monitors time, depth and air tank pressure (received through expensive wireless transceivers or a hose). These computers are costly for the average recreational dive.
We present a hybrid systems model and safety proof for a SCUBA diving computer that estimates air consumption of the diver using commodity heart rate sensors. We employ a mathematical model of oxygen uptake in response to exercise and thereby predict the time remaining for the air supply to be depleted, as well as obviate the need for a tank-mounted wireless transmitter or the cumbersome hose integrated computer for directly monitoring tank pressure. We formally verify a controller that ensures the diver can always surface without running out of breathable air.
Our model is written in differential dynamic logic and our proofs are constructed using KeYmaera X with the Mathematica backend for first order real arithmetic.
There are three models/proofs:
- tApprox: Contains the theorem statement, proof, and proof documentation for the basic model.
- tApproxUpdate: Allows occasional manual ground truth updates for
- nitrogen: Establishes both nitrogen safety and oxygen safety.
Each folder contains:
.kyxfile: A human-readable copy of the KeYmaera X model (open in your favorite text editor that supports unix line endings).
.kytfile: The Bellerophon tactic for proving the property in the
.kyafile : A KeYmaera X "archive" file containing the model and proof.
Instructions for Checking the Proofs
Part 1: Download, install, and initialize KeYmaera X
Install the correct version of the Java runtime. You will need a Java 8 JRE. On Ubuntu, run
sudo apt-get install openjdk-8-jrethen run
sudo update-alternatives --config javaand select the version 8 option.
download version 4.4 of KeYmaera X (note: this is NOT the current version!)
If you have a previous version of KeYmaera X installed, back up and then delete your
Now we need to accept the KeYmaera X lincense (GPL) and initialize the KeYmaera X lemma cache. To do this, boot KeYmaera X by running:
java -jar keymaerax.jar
Once KeYmaera X is running, a browser window should open to
If this does not happen automatically after a couple of minutes, navigate your browser to that URL manually.
Register an account and accept the license.
If you have a Mathematica installation, setup KeYmaera X to use mathematica by going to
Arithmetic Solver, and then selected defaults.
NOTE: Mathematica is optional for KeYmaera X, but our proof may not complete without a mathematica installation because Z3 will time out on some subgoals and some machines. If the proof does not complete during part 2 and you see a warning message about Z3 in STDOUT, then you will need to install Mathematica and configure KeYmaera X to use mathematica before proceeding.
- While logged in to KeYmaera X, click the "shutdown / turn off" icon (NOT the "log out" icon). This is the second to last icon on the right-hand side of the menu bar. You should see a " KeYmaera X is now offline. Please close the browser window." message.
Part 2: check the proof
copy the archive file (
.kya) into the directory that your keymaerax.jar file is located in.
Once KeYmaera X is shut down, run:
java -jar keymaerax.jar -check final.kya
The final command might take a while, especially if you don't have a Mathematica installation. Warning: this will drain a laptop's battery.
You should see the following output:
========================================== Proving final.kya: model nitrogen with tactic nitrogen: Proof =============== Succeeded =============== Proved final.kya: nitrogen with nitrogen: Proof Proof duration [ms]: 92782 QE duration [ms]: 78803 Tactic size: 347 Tactic lines: 228 Proof steps: 63687 ========================================== =============== Succeeded =============== Proved final.kya: nitrogen with nitrogen: Proof Proof duration [ms]: 92782 QE duration [ms]: 78803 Tactic size: 347 Tactic lines: 228 Proof steps: 63687 ========================================== Shutting down Mathematica... ...Done No need to shut down MathKernel if no link has been initialized
You can check each of these proofs by changing into the appropriate directory and running KeYmaera X with the -check flag on the appropriate .kya file. For example,
cd nitrogen; java -jar path/to/keymaerax4.4.jar -check final.kya
- Viren Bajaj
- Karim Elmaaroufi
- Nathan Fulton firstname.lastname@example.org