Forward invariant cuts to simplify proofs of safety

摘要

The use of deductive techniques, such as theorem provers, has several advantages in safety verification of hybrid systems; however, state-of-the-art theorem provers require manual intervention to handle complex systems. 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 directly. This paper presents an extension to KeYmaera, a deductive verification tool for differential dynamic logic; the new technique allows local reasoning using system designer intuition about performance within particular modes as part of a proof task. Our approach allows the theorem prover to leverage forward invariants, discovered using numerical techniques, as part of a proof of safety. We introduce a new inference rule into the proof calculus of KeYmaera, the forward invariant cut rule, and we present a methodology to discover useful forward invariants, which are then used with the new cut rule to complete verification tasks. We demonstrate how our new approach can be used to complete verification tasks that lie out of the reach of existing automatic verification approaches using several examples, including one involving an automotive powertrain control system.