Visible to the public Using Theorem Provers to Guarantee Closed-Loop System Properties

Abstract--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 ecient 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 sucient 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 dierential 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
sucient conditions that are checked for the controller design.

Preview: Text

Other available formats:   

Using Theorem Provers to Guarantee Closed-Loop System Properties
Switch to experimental viewer