Forward Invariant Cuts to Simplify Proofs of Safety

Abstract:

The use of deductive techniques, such as theorem provers, has several advantages in safety verification of hybrid systems. State-of-the-art theorem provers, however, suffer from a significant lack of automation. Furthermore, there is often a gap between the type of assistance that a theorem prover requires to make progress on a proof task and the assistance that a system designer is able to provide.  This paper presents an extension to the deductive verification framework of differential dynamic logic that allows the theorem prover to leverage system designer intuition about stability within particular modes as part of a proof task. For stable modes of operation, numerical methods can be used to search for forward invariants. Our technique allows the theorem prover to leverage these forward invariants as part of a proof of safety by locally reasoning about behaviors.  Our key contribution is a new inference rule, the forward invariant cut rule introduced into the proof calculus of Keymaera. We describe Manticore, a new Keymaera strategy engine for discovering forward invariant cuts using designer insight. Keymaera uses the cut rules found with Manticore to excise parts of the hybrid state space for which local invariants can be computed from the overall safety proof, resulting in a smaller sub-goal.  We demonstrate the cut rule in action on illustrative examples, including a representative automotive powertrain control systems.