Verified Execution for Differential Dynamic Logic

Verifying an abstract model of a system gives us valuable insights, but only guarantees safety of the real system insofar as the system is faithful to the model. If the system is not actually faithful to the model, all bets are off. One way to address the gap between models and implementations is by automatically generating a verified runtime monitor from the model, which then dynamically checks that the real system obeys the assumptions of the model and takes failsafe measures if it does not. This approach is taken by ModelPlex, but this alone does not provide a full answer because the monitors are expressed as formulas in differential dynamic logic, which are not obviously executable because they contain computations over real numbers.

In this work we first lower these monitors toward execution by soundly translating them to compute with interval arithmetic. We then soundly generate a concrete implementation in CakeML and compile it soundly to machine code. We have tested the resulting code on a Rasperry Pi-controlled ground robot and in a simulation implemented in AirSim.

The interval arithmetic proofs are performed in Isabelle/HOL while the initial model safety proof is performed in KeYmaera X. To reduce the trusted base, we built on a prior formalization of differential dynamic logic to build a verified proof checker for proofs exported from KeYmaera X.

In followup work, we used constructive hybrid games as a new foundation to improve robustness of verified execution while supporting a wider range of models.