Muutke küpsiste eelistusi

Formal Verification of Control System Software [Kõva köide]

  • Formaat: Hardback, 232 pages, kõrgus x laius: 235x155 mm, 79 b/w illus.
  • Sari: Princeton Series in Applied Mathematics
  • Ilmumisaeg: 14-May-2019
  • Kirjastus: Princeton University Press
  • ISBN-10: 0691181306
  • ISBN-13: 9780691181301
Teised raamatud teemal:
Formal Verification of Control System SoftwareSuurem pilt
  • Formaat: Hardback, 232 pages, kõrgus x laius: 235x155 mm, 79 b/w illus.
  • Sari: Princeton Series in Applied Mathematics
  • Ilmumisaeg: 14-May-2019
  • Kirjastus: Princeton University Press
  • ISBN-10: 0691181306
  • ISBN-13: 9780691181301
Teised raamatud teemal:
Püsilink: https://www.kriso.ee/db/9780691181301.html
Märksõnad:

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.

Arvustused

Innovative, mathematically exact, and very well written. Garoche is a rare resource, and his book will enrich the knowledge of both the computer-science and control-systems communities.Eric Feron, Georgia Institute of Technology "This book makes a timely contribution at the crossroads of formal computer science, optimization, and control. It should be of interest to computer scientists and control engineers."Didier Henrion, LAAS-CNRS Toulouse and Czech Technical University in Prague A pleasure to read. Garoches excellent and timely book presents state-of-the-art methods building on convex optimization to perform static analysis for control systems and software.Taylor Johnson, Vanderbilt University

I Need and Tools to Verify Critical Cyber-Physical Systems
1(40)
1 Critical Embedded Software: Control Software Development and V&V
3(4)
2 Formal Methods: Different Approaches for Verification
7(24)
2.1 Semantics and Properties
7(4)
2.2 A Formal Verification Methods Overview
11(8)
2.3 Deductive Methods
19(2)
2.4 SMT-based Model-checking
21(2)
2.5 Abstract Interpretation (of Collecting Semantics)
23(6)
2.6 Need for Inductive Invariants
29(2)
3 Control Systems
31(10)
3.1 Controllers' Development Process
31(4)
3.2 A Simple Linear System: Spring-mass Damper
35(6)
II Invariant Synthesis: Convex-optimization Based Abstract Interpretation
41(86)
4 Definitions---Background
43(21)
4.1 Discrete Dynamical Systems
43(11)
4.2 Elements of (Applied) Convex Optimization
54(10)
5 Invariants Synthesis via Convex Optimization: Postfixpoint Computation as Semialgebraic Constraints
64(47)
5.1 Invariants, Lyapunov Functions, and Convex Optimization
64(4)
5.2 Quadratic Invariants
68(8)
5.3 Piecewise Quadratic Invariants
76(11)
5.4 k-inductive Quadratic Invariants
87(8)
5.5 Polynomial Invariants
95(8)
5.6 Image Measure Method
103(5)
5.7 Related Works
108(3)
6 Template-based Analyses and Min-policy Iteration
111(16)
6.1 Template-based Abstract Domains
111(1)
6.2 Template Abstraction Fixpoint as an Optimization Problem
112(2)
6.3 SOS-relaxed Semantics
114(8)
6.4 Example
122(2)
6.5 Related Works
124(3)
III System-level Analysis at Model and Code Level
127(38)
7 System-level Properties as Numerical Invariants
129(18)
7.1 Open-loop and Closed-loop Stability
130(9)
7.2 Robustness with Vector Margin
139(6)
7.3 Related Work
145(2)
8 Validation of System-level Properties at Code Level
147(18)
8.1 Axiomatic Semantics of Control Properties through Synchronous Observers and Hoare Triples
147(8)
8.2 Generating Annotations: A Strongest Postcondition Propagation Algorithm
155(4)
8.3 Discharging Proof Objectives using PVS
159(6)
IV Numerical Issues
165(36)
9 Floating-point Semantics of Analyzed Programs
167(24)
9.1 Floating-point Semantics
167(3)
9.2 Revisiting Inductiveness Constraints
170(3)
9.3 Bound Floating-point Errors: Taylor-based Abstractions aka Zonotopic Abstract Domains
173(17)
9.4 Related Works
190(1)
10 Convex Optimization and Numerical Issues
191(10)
10.1 Convex Optimization Algorithms
191(5)
10.2 Guaranteed Feasible Solutions with Floats
196(5)
Bibliography 201(16)
Index 217(3)
Acknowledgments 220
Pierre-Loïc Garoche is senior research scientist at ONERA, Frances national aerospace research center.