Using Theorem Provers to Guarantee Closed-Loop System Properties

This paper presents a new approach for leveraging the power of theorem provers for formal verification to provide sufficient conditions that can be checked on embedded control designs. Theorem provers are often most efficient when using generic models that abstract away many of the controller details, but with these abstract models very general conditions can be verified under which desirable properties such as safety can be guaranteed for the closed-loop system. We propose an approach in which these sufficient conditions are static conditions that can be checked for the specific controller design, without having to include the dynamics of the plant. We demonstrate this approach using the KeYmaera theorem prover for differential dynamic logic for two examples: an intelligent cruise controller and a cooperative intersection collision avoidance system (CICAS) for left-turn assist. In each case, safety of the closed-loop system proved using KeYmaera provides static sufficient conditions that are checked for the controller design.