This repository contains KeYmaera X proofs of the theorems in "Verified Train Controllers for the Federal Railroad Administration Model: Balancing Competing Brake and Track Forces". Aditi Kabra, Stefan Mitsch, André Platzer. Verified Train Controllers for the Federal Railroad Administration Model: Balancing Competing Brake and Track Forces. International Conference on Embedded Software (EMSOFT), 2022. It also contains a Docker setup to run the proofs. ## Content Repeatability scripts: - setup.sh: the setup script for creating the Docker container - Dockerfile: the Docker configuration file used by setup.sh - keymaerax.math.conf: the KeYmaera X configuration file used in setup.sh - check_all.sh: the run script to check all the proofs Proof files: - Theorem IV.I (Conservative controller is safe): IV_I_conservative.kyx - Theorem V.I (Slope estimating controller is safe): V_I_slopecurve.kyx - Theorem V.II (Air brake exploiting controller is safe): V_II_airbrakes.kyx - Theorem V.III (Taylor polynomial controller is safe): V_III_taylor.kyx - Theorem VI.I (Physical controller is safe). A physical instantiation of V.III with actual freight train numbers. Please run theorem V.II before running this proof archive, since the current proof uses the proof of V_II_airbrakes.kyx as a lemma. File: VI_I_airbrakes_freight.kyx - Theorem V.II expanded. (Air brake exploiting controller is safe). We expand out function definitions such as stopping distance and braking distance to present the true arithmetic complexity of the proof. Please run theorem V.II before running this proof archive, since the current proof uses the proof of V_II_airbrakes.kyx as a lemma. File: V_II_airbrakes_expanded.kyx ## Setup The following instructions assume that Docker is installed on your machine and working correctly, see [docs.docker.com/get-docker/](https://docs.docker.com/get-docker/). We recommend having at least 8–16 GB RAM on your machine to avoid compilation issues when building the Docker container. For a complete evaluation, KeYmaera X requires an activated version of Wolfram Engine. The license for Wolfram Engine can be obtained for free and you will be prompted during installation to do so. 1. Run the setup script with the command ``` ./setup.sh ``` Please note that the installation process may take a long time to complete because it installs Wolfram Engine. 1. During installation, you will see a dialog asking for one-time activation of Wolfram Engine. Please register for a free Wolfram Engine license: ``` The Wolfram Engine requires one-time activation on this computer. Visit https://wolfram.com/engine/free-license to get your free license. Wolfram ID: ``` We recommend you register for a license with a new Wolfram account. If the script fails midway, please try to re-run it a few times to see if it makes further progress. Specifically, if the script fails in compilation with a Java Heap Space error, please try to increase memory for the Docker container and/or increase the SBT heap space in Dockerfile line 96 (-Xmx4G) and re-run. The artifact was tested with 16GB of memory available to the Docker container and 4GB of SBT heap space. If the script fails when installing Wolfram Engine with error messages similar to `Error: Download failed. Check the network connection and retry.`, or `ZIP decompression failed`, please check your internet connection and/or try increasing the amount of disk space available to the Docker container and/or simply retry since the Wolfram Engine download sites may temporarily be unavailable. ## Checking the Proofs Run the proof-checking script as follows: ``` ./check_all.sh ``` You should see output similar to ``` ***************************** KeYmaera X artifact checking. ***************************** KeYmaera X prover 4.9.9 ... Proving entries from 1 files Proving /home/{user}/IV_I_conservative.kyx#IV-I Conservative Control... Done /home/{user}/IV_I_conservative.kyx#IV-I Conservative Control (proved) PROVED IV-I Conservative Control: tactic=IV-V Conservative Control: Proof, ... ... ********************************* KeYmaera X all artifacts checked. ********************************* ``` ## Running with a Local Installation of KeYmaera X To run the proofs with a local installation of KeYmaera X, in a directory containing keymaerax.jar and the .kyx proof files, on the command line, ``` java -da -jar keymaerax.jar -launch -prove [filename] ``` Please run theorems in the order listed in check_all.sh, since: - V_II_airbrakes_expanded.kyx and VI_I_airbrakes_freight.kyx use V_II_airbrakes.kyx as a lemma - VI_I_taylor_freight.kyx uses V_III_taylor.kyx as a lemma Detailed instructions to use KeYmaera X: https://keymaerax.org.