E-Book Overview
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.
E-Book Content
Formal Verification of Control System Software
PRINCETON SERIES IN APPLIED MATHEMATICS Ingrid Daubechies (Duke University); Weinan E (Princeton University); Jan Karel Lenstra (Centrum Wiskunde & Informatica, Amsterdam); Endre S¨ uli (University of Oxford) The Princeton Series in Applied Mathematics publishes high quality advanced texts and monographs in all areas of applied mathematics. Books include those of a theoretical and general nature as well as those dealing with the mathematics of specific applications areas and real-world situations. A list of titles in this series appears at the back of the book.
Formal Verification of Control System Software
Pierre-Lo¨ıc Garoche
PRINCETON UNIVERSITY PRESS PRINCETON AND OXFORD
c 2019 by Princeton University Press Copyright Published by Princeton University Press 41 William Street, Princeton, New Jersey 08540 6 Oxford Street, Woodstock, Oxfordshire OX20 1TR press.princeton.edu All Rights Reserved LCCN 2019930479 ISBN 978-0-691-18130-1 British Library Cataloging-in-Publication Data is available Editorial: Vickie Kearn, Susannah Shoemaker, and Lauren Bucca Production Editorial: Brigitte Pelner Jacket/Cover credit: Sculpture by Patrick Meichel Production: Erin Suydam Publicity: Alyssa Sanford This book has been composed in LATEX Printed on acid-free paper ∞ Printed in the United States of America 10
9
8
7
6
5
4
3
2
1
To Pierre Garoche: the captain, the engineer, and the researcher
Contents I
1
Need and Tools to Verify Critical Cyber-Physical Systems
1
Critical Embedded Software: Control Software Development and V&V
3
2
Formal Methods: Different Approaches for Verification 2.1 Semantics and Properties 2.2 A Formal Verification Methods Overview 2.3 Deductive Methods 2.4 SMT-based Model-checking 2.5 Abstract Interpretation (of Collecting Semantics) 2.6 Need for Inductive Invariants
7 7 11 19 21 23 29
3
Control Systems 3.1 Controllers’ Development Process 3.2 A Simple Linear System: Spring-mass Damper
31 31 35
II Invariant Synthesis: Convex-optimization Based Abstract Interpretation
41
4
Definitions–Backg