Controller Verification and Design with Logical Analysis Support

Modern computer-controlled systems deployed for safety-critical applications
are growing increasingly large and complex. Industry professionals submit their
designs to rigorous testing procedures to detect possible errors and re-design the
system as necessary. Nonetheless, design errors can go undetected and appear in the
final product. In safety-critical systems, these errors may cause severe financial and
even human losses. As a result, the modern engineering development process needs
to address safety specifications as well as performance specifications.
This dissertation proposes the use of control envelopes, which are abstractions
on the input-output relation of a controller. Control envelopes can be used to verify
safety of proposed controllers. Since the control envelope does not depend on
any specific controller implementation, it can be reused throughout the system development
cycle. As a result, safety specifications can be checked with the control
envelope by a static check on the input-output of the controller. Second, control
envelopes constitute a reusable specification. Initial effort devoted to computing a
good control pays for itself throughout the rest of the development process in terms
of flexibility and reusability.
We describe a tool called Perseus to automatically check when a controller satisfies
a control envelope. We illustrate our approach on control design case studies for
autonomous driving scenarios intended to reduce accidents at traffic intersections.
Our case studies make use of the theorem prover KeYmaera to verify plants controlled
by control envelopes. KeYmaera uses a powerful representation language
called differential dynamic logic, which supports symbolic parameters and can handle
nonlinear dynamics without resorting to approximation techniques that incur errors.
However, KeYmaera (and theorem proving approaches in general) suffer from
a lack of automation, and often require specialized knowledge to operate. We propose
the addition of a forward invariant cut proof rule to KeYmaera’s reasoning
calculus, which allows one to leverage designer insights into proofs of safety of a
closed-loop system. We describe the tool Manticore, which aids the search for forward
invariants. We illustrate our approach on a case study of a benchmark fuel
control system.