Formal Verification of Control System Software

Name: Formal Verification of Control System Software
Brand: Princeton University Press
Price: 121.95 EUR
Availability: OnlineOnly

Pierre-Loïc Garoche(Autor*in)

Princeton University Press

1. Auflage

Erschienen am 14. Mai 2019

232 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-0-691-18958-1 (ISBN)

121,95 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Person

Inhalt

Cover
Contents
I. Need and Tools to Verify Critical Cyber-Physical Systems
1. Critical Embedded Software: Control Software Development and V&V
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
3. Control Systems
3.1 Controllers' Development Process
3.2 A Simple Linear System: Spring-mass Damper
II. Invariant Synthesis: Convex-optimization Based Abstract Interpretation
4. Definitions-Background
4.1 Discrete Dynamical Systems
4.2 Elements of (Applied) Convex Optimization
5. Invariants Synthesis via Convex Optimization: Postfixpoint Computation as Semialgebraic Constraints
5.1 Invariants, Lyapunov Functions, and Convex Optimization
5.2 Quadratic Invariants
5.3 Piecewise Quadratic Invariants
5.4 k-inductive Quadratic Invariants
5.5 Polynomial Invariants
5.6 Image Measure Method
5.7 Related Works
6. Template-based Analyses and Min-policy Iteration
6.1 Template-based Abstract Domains
6.2 Template Abstraction Fixpoint as an Optimization Problem
6.3 SOS-relaxed Semantics
6.4 Example
6.5 Related Works
III. System-level Analysis at Model and Code Level
7. System-level Properties as Numerical Invariants
7.1 Open-loop and Closed-loop Stability
7.2 Robustness with Vector Margin
7.3 Related Work
8. Validation of System-level Properties at Code Level
8.1 Axiomatic Semantics of Control Properties through Synchronous Observers and Hoare Triples
8.2 Generating Annotations: A Strongest Postcondition Propagation Algorithm
8.3 Discharging Proof Objectives using PVS
IV. Numerical Issues
9. Floating-point Semantics of Analyzed Programs
9.1 Floating-point Semantics
9.2 Revisiting Inductiveness Constraints
9.3 Bound Floating-point Errors: Taylor-based Abstractions aka Zonotopic Abstract Domains
9.4 Related Works
10. Convex Optimization and Numerical Issues
10.1 Convex Optimization Algorithms
10.2 Guaranteed Feasible Solutions with Floats
Bibliography
Index
Acknowledgments

Systemvoraussetzungen

Als PDF speichern Als Link merken