An essential introduction to the analysis and verification of control
system software
The verification of control system software is critical to a host of
technologies and industries, from aeronautics and medical technology to
the cars we drive. The failure of controller software can cost people
their lives. In this authoritative and accessible book, Pierre-Loïc
Garoche provides control engineers and computer scientists with an
indispensable introduction to the formal techniques for analyzing and
verifying this important class of software.
Too often, control engineers are unaware of the issues surrounding the
verification of software, while computer scientists tend to be
unfamiliar with the specificities of controller software. Garoche
provides a unified approach that is geared to graduate students in both
fields, covering formal verification methods as well as the design and
verification of controllers. He presents a wealth of new verification
techniques for performing exhaustive analysis of controller software.
These include new means to compute nonlinear invariants, the use of
convex optimization tools, and methods for dealing with numerical
imprecisions such as floating point computations occurring in the
analyzed software.
As the autonomy of critical systems continues to increase--as evidenced
by autonomous cars, drones, and satellites and landers--the numerical
functions in these systems are growing ever more advanced. The
techniques presented here are essential to support the formal analysis
of the controller software being used in these new and emerging
technologies.
