Physics Engines for Verification of Robotic Systems

Simulation is widely used to informally test designs, but the evidence it provides is restricted to the scenarios that are simulated. This limitation can be addressed by complementing simulation with proof, which provides mathematical evidence of expected behaviour across all relevant scenarios. Proof-based verification helps meet the trustworthiness demands of modern robotic applications. However, co-verification using simulation and proof requires consistency between the simulation and proof models. Achieving such consistency remains difficult because the physics engines used by most simulators do not expose their underlying algorithms; at best, reliance on source code is required. This thesis introduces a framework that enables transparency, configurability, and extensibility in the use of physics engines. The results not only support consistent co-verification, but also help expose, and therefore address, the reality gap by explicitly recording simulation assumptions.