Verifying Cyber-Physical Systems
A Path to Safe Autonomy
by Mitra
ISBN: 9780262363112 | Copyright 2021
Instructor Requests
A graduate-level textbook that presents a unified mathematical framework for modeling and analyzing cyber-physical systems, with a strong focus on verification.
Verification aims to establish whether a system meets a set of requirements. For such cyber-physical systems as driverless cars, autonomous spacecraft, and air-traffic management systems, verification is key to building safe systems with high levels of assurance. This graduate-level textbook presents a unified mathematical framework for modeling and analyzing cyber-physical systems, with a strong focus on verification. It distills the ideas and algorithms that have emerged from more than three decades of research and have led to the creation of industrial-scale modeling and verification techniques for cyber-physical systems.
The book discusses such computer science concepts as undecidability and abstractions, alongside concepts from control theory including multiple Lyapunov functions and barrier certificates, all within a unified mathematical language. It explains algorithms for reachability analysis, counter-example guided abstraction refinement, and data-driven verification, as well as the key data structures that enable their effective implementation. Other topics include invariants, deductive verification, progress analysis, sensitivity analysis, simulation relations, fairness, model checking, satisfiability modulo theories, temporal logics, compositional reasoning, convergence analysis, asynchronous processes, and verification of black-box systems.
The book provides more than twenty examples of cyber-physical verification, ranging from conceptual models to advanced driving-assist systems. Each chapter offers exercise problems; supporting materials, including slides, simulation code, additional exercises, and solutions are available on the book's website.
| Expand/Collapse All | |
|---|---|
| Contents (pg. vii) | |
| Preface (pg. xv) | |
| 1. Introduction (pg. 1) | |
| 1.1 What is this book about? The verification problem (pg. 1) | |
| 1.2 Testing and verification for establishing system requirements (pg. 2) | |
| 1.3 From systems to models of systems (pg. 3) | |
| 1.4 Design automation ecosystem (pg. 7) | |
| 1.5 Challenges and state of the art (pg. 7) | |
| 1.6 Road map (pg. 11) | |
| 1.7 Learning and teaching using this book (pg. 14) | |
| 2. Modeling Computation (pg. 17) | |
| 2.1 Quick introduction to automata (pg. 17) | |
| 2.1.1 Example: JK flip-flop (pg. 17) | |
| 2.1.2 Language for specifying automata (pg. 17) | |
| 2.2 Specifying automata (pg. 20) | |
| 2.2.1 State variables and valuations (pg. 20) | |
| 2.2.2 Predicates (pg. 20) | |
| 2.2.3 Transitions (pg. 21) | |
| 2.2.4 Automata (pg. 22) | |
| 2.3 Special automata classes (pg. 23) | |
| 2.3.1 Finite and discrete automata (pg. 23) | |
| 2.3.2 Nondeterminism (pg. 23) | |
| 2.3.3 Discrete sequences and sampled time (pg. 23) | |
| 2.4 Semantics: Executions, reachable states, and invariants (pg. 24) | |
| 2.5 Example: Dijkstra's token ring algorithm (pg. 24) | |
| 2.5.1 Legal states and invariants (pg. 26) | |
| 2.5.2 Asynchronous and synchronous models (pg. 26) | |
| 2.6 Example: Reasoning about impossibility (pg. 27) | |
| 2.7 Exercises (pg. 28) | |
| 3. Modeling Physics (pg. 31) | |
| 3.1 Quick introduction to differential equations (pg. 31) | |
| 3.1.1 Example: Vehicle speed control (pg. 31) | |
| 3.1.2 Language for specifying differential equations (pg. 31) | |
| 3.2 Specifying ordinary differential equations (pg. 33) | |
| 3.2.1 State variables and valuations (pg. 34) | |
| 3.2.2 Dense time and trajectories (pg. 34) | |
| 3.2.3 Trajectories as solutions (pg. 35) | |
| 3.3 Special classes of ODEs (pg. 37) | |
| 3.3.1 Time-invariant and autonomous systems (pg. 37) | |
| 3.3.2 Linear systems (pg. 38) | |
| 3.4 Semantics: Reachable states, invariants, and stability (pg. 39) | |
| 3.4.1 Example: Pendulum (pg. 40) | |
| 3.4.2 Example: Kinematic vehicle model (pg. 42) | |
| 3.5 Lyapunov's direct method for proving stability (pg. 44) | |
| 3.5.1 Stability of linear dynamical systems (pg. 45) | |
| 3.6 Differential equations as automata (pg. 46) | |
| 3.7 Example: Simple economy (pg. 47) | |
| 3.8 Numerical simulations for ordinary differential equations (pg. 48) | |
| 3.9 Closing the loop and control synthesis (pg. 49) | |
| 3.9.1 Proportional-integral-derivative controller (pg. 51) | |
| 3.9.2 Controller synthesis problem (pg. 52) | |
| 3.10 Exercises (pg. 53) | |
| 4. Modeling Cyber-Physical Systems (pg. 55) | |
| 4.1 Quick introduction to hybrid automata (pg. 55) | |
| 4.1.1 Example: Rimless wheel (pg. 55) | |
| 4.1.2 Language for specifying hybrid systems (pg. 56) | |
| 4.2 Specifying hybrid automata (pg. 58) | |
| 4.2.1 State variables and transitions (pg. 58) | |
| 4.2.2 Trajectories and closures (pg. 58) | |
| 4.2.3 Hybrid automata (pg. 60) | |
| 4.2.4 A guide for hybrid modeling (pg. 61) | |
| 4.3 Special classes of hybrid automata (pg. 61) | |
| 4.3.1 Deterministic hybrid automata (pg. 61) | |
| 4.3.2 Switched systems (pg. 62) | |
| 4.3.3 Linear hybrid automata (pg. 63) | |
| 4.3.4 Example: Thermostat (pg. 63) | |
| 4.3.5 Rectangular hybrid automata (pg. 64) | |
| 4.3.6 Timed automata (pg. 65) | |
| 4.4 Semantics: Hybrid executions (pg. 65) | |
| 4.4.1 Numerical simulation of hybrid executions (pg. 67) | |
| 4.4.2 Reachable states, invariants, and stability (pg. 68) | |
| 4.4.3 Time-abstract semantics (pg. 69) | |
| 4.4.4 Execution zoo (pg. 71) | |
| 4.5 Example: Spacecraft docking (pg. 72) | |
| 4.6 Example: Small aircraft traffic management system (pg. 74) | |
| 4.7 Exercises (pg. 75) | |
| 5. Composing Models (pg. 79) | |
| 5.1 Composing automata (pg. 79) | |
| 5.2 Composing input/output automata (pg. 80) | |
| 5.2.1 Input/output automata (pg. 80) | |
| 5.2.2 Compatibility and composition of input/output automata (pg. 80) | |
| 5.3 Example: Channels, logical clocks, and distributed systems (pg. 81) | |
| 5.3.1 First-in, first-out channels (pg. 81) | |
| 5.3.2 Logical time in distributed systems: Lamport clocks (pg. 83) | |
| 5.3.3 Composed system: A network of processes communicating over channels (pg. 84) | |
| 5.3.4 Traces and projections (pg. 85) | |
| 5.4 Composing hybrid input/output automata (pg. 87) | |
| 5.4.1 Hybrid input/output automata (pg. 88) | |
| 5.4.2 Compatibility and composition of hybrid input/output automata (pg. 89) | |
| 5.5 Example: Interconnecting flip-flops (pg. 90) | |
| 5.6 Example: Timed channels (pg. 91) | |
| 5.7 Example: Pulse generator and oscillator (pg. 93) | |
| 5.8 Traces, untiming, and properties of compositions (pg. 93) | |
| 5.9 Example: Emergency braking on highways (pg. 96) | |
| 5.10 Exercises (pg. 98) | |
| 6. Specifying Requirements (pg. 101) | |
| 6.1 Requirements analysis (pg. 101) | |
| 6.2 Safety standards (pg. 102) | |
| 6.2.1 DO-178C (pg. 102) | |
| 6.2.2 ISO 26262 (pg. 104) | |
| 6.2.3 Beyond current safety standards and requirements (pg. 105) | |
| 6.3 From requirements to verification (pg. 105) | |
| 6.3.1 Formal verification algorithms (pg. 106) | |
| 6.3.2 Resources for verification and computational complexity (pg. 107) | |
| 6.3.3 Invariants and safety requirements (pg. 109) | |
| 6.3.4 Progress requirements (pg. 110) | |
| 6.4 Linear temporal logic (pg. 111) | |
| 6.4.1 Background definitions (pg. 112) | |
| 6.4.2 LTL syntax (pg. 113) | |
| 6.4.3 LTL semantics (pg. 113) | |
| 6.5 Computational tree logic (pg. 116) | |
| 6.5.1 Computational tree logic syntax (pg. 116) | |
| 6.5.2 Computational tree logic semantics (pg. 116) | |
| 6.5.3 Expressiveness of linear temporal logic and computational tree logic (pg. 117) | |
| 6.6 Further reading (pg. 118) | |
| 6.6.1 Checking temporal logic models (pg. 118) | |
| 6.6.2 Planning and synthesis with temporal logics (pg. 118) | |
| 6.6.3 Dense time, signal, and stochastic temporal logics (pg. 119) | |
| 6.6.4 Runtime verification and monitoring (pg. 120) | |
| 6.7 Exercises (pg. 121) | |
| 7. Verifying Invariants (pg. 123) | |
| 7.1 Quick introduction to proving invariants (pg. 123) | |
| 7.2 Reasoning with inductive invariants (pg. 125) | |
| 7.2.1 Invariance and composition (pg. 127) | |
| 7.3 Proving timing-based mutual exclusion (pg. 127) | |
| 7.3.1 Example: Fischer's mutual exclusion (pg. 127) | |
| 7.3.2 Analysis of Fischer's mutual exclusion (pg. 130) | |
| 7.4 Proving inductive invariants without solving ordinary differential equations (pg. 133) | |
| 7.4.1 Example: Checking subtangential conditions (pg. 134) | |
| 7.4.2 Barrier certificates (pg. 136) | |
| 7.5 Satisfiability and satisfiability modulo theories (pg. 137) | |
| 7.5.1 Satisfiability (pg. 137) | |
| 7.5.2 Satisfiability modulo theory (pg. 138) | |
| 7.5.3 Modeling for satisfiability and satisfiability modulo theory (pg. 140) | |
| 7.6 Further reading (pg. 141) | |
| 7.6.1 Finding and learning invariants (pg. 141) | |
| 7.7 Exercises (pg. 143) | |
| 8. Abstractions and Compositional Reasoning (pg. 145) | |
| 8.1 Quick introduction to abstractions: Timing abstraction (pg. 145) | |
| 8.2 Abstraction definitions (pg. 148) | |
| 8.3 Proving abstractions: Simulation relations (pg. 149) | |
| 8.4 Bisimulations and time-abstract bisimulations (pg. 152) | |
| 8.4.1 Untiming and bisimulations (pg. 153) | |
| 8.4.2 Example: Simulation and trace inclusion (pg. 154) | |
| 8.4.3 Backward simulations (pg. 154) | |
| 8.5 Hybridization (pg. 155) | |
| 8.6 Substituting with abstractions (pg. 157) | |
| 8.7 Designing a CEGAR-based cyber-physical verification system (pg. 158) | |
| 8.7.1 Space of abstractions (pg. 159) | |
| 8.7.2 Model checker (pg. 162) | |
| 8.7.3 Counterexample validation (pg. 162) | |
| 8.7.4 Refinement strategy (pg. 163) | |
| 8.8 Further reading (pg. 163) | |
| 8.9 Exercises (pg. 163) | |
| 9. Reachability Analysis (pg. 165) | |
| 9.1 Quick introduction to reachability analysis (pg. 165) | |
| 9.2 Finite automata (pg. 166) | |
| 9.2.1 Finite state reachability (pg. 166) | |
| 9.3 Timed automata (pg. 168) | |
| 9.3.1 Syntax for timed automata (pg. 168) | |
| 9.3.2 Example: Timed light switch (pg. 170) | |
| 9.3.3 Clock equivalence relation on states (pg. 170) | |
| 9.3.4 Control state reachability and region automata (pg. 173) | |
| 9.4 Integral timed automata to rectangular hybrid automata (pg. 176) | |
| 9.4.1 Rational timed automata (pg. 176) | |
| 9.4.2 Multirate automata (pg. 176) | |
| 9.4.3 Rectangular hybrid automata (pg. 177) | |
| 9.5 Undecidability of control state reachability for rectangular hybrid automata (pg. 178) | |
| 9.5.1 Two-counter machines (pg. 178) | |
| 9.5.2 Reduction of control state reachability of rectangular hybrid automata to the halting problem of two-counter machines (pg. 179) | |
| 9.5.3 Initialized rectangular hybrid automata (pg. 182) | |
| 9.6 Relaxing the verification problem (pg. 183) | |
| 9.6.1 Bounded reachability analysis (pg. 184) | |
| 9.7 Data structures for reachability analysis (pg. 186) | |
| 9.7.1 Rectangles (pg. 186) | |
| 9.7.2 Polytopes (pg. 189) | |
| 9.7.3 Zonotopes (pg. 192) | |
| 9.7.4 Ellipsoids (pg. 193) | |
| 9.8 Exercises (pg. 194) | |
| 10. Progress Analysis (pg. 197) | |
| 10.1 Quick introduction to progress (pg. 197) | |
| 10.2 Termination of discrete-time automata (pg. 198) | |
| 10.2.1 Termination with well-founded relations (pg. 199) | |
| 10.2.2 Example: UpDown counter (pg. 200) | |
| 10.2.3 Termination with disjunctive well-founded relations (pg. 201) | |
| 10.2.4 Example: UpDown revisited (pg. 202) | |
| 10.3 Self-stabilization (pg. 202) | |
| 10.3.1 Example: Distributed minimum spanning tree algorithm (pg. 203) | |
| 10.3.2 Stabilization of the minimum spanning tree algorithm (pg. 205) | |
| 10.4 Convergence and stability of asynchronous systems without metrics (pg. 206) | |
| 10.4.1 Convergence for finite state systems (pg. 207) | |
| 10.5 Stability proofs for dynamical systems (pg. 208) | |
| 10.6 Stability of hybrid automata (pg. 210) | |
| 10.6.1 Common Lyapunov functions (pg. 210) | |
| 10.6.2 Multiple Lyapunov functions (pg. 211) | |
| 10.6.3 Stability under slow switching: Average dwell time (pg. 212) | |
| 10.7 Exercises (pg. 214) | |
| 11. Data-Driven Verification (pg. 217) | |
| 11.1 Quick introduction to data-driven safety verification (pg. 218) | |
| 11.1.1 Discrepancy functions (pg. 218) | |
| 11.1.2 BasicSimReach algorithm (pg. 219) | |
| 11.1.3 Example: Moore-Greitzer jet engine (pg. 222) | |
| 11.2 Computing discrepancy (pg. 222) | |
| 11.2.1 Linear dynamical systems (pg. 223) | |
| 11.2.2 Nonlinear dynamical systems: Optimization approaches (pg. 223) | |
| 11.2.3 Nonlinear models: Local discrepancy (pg. 224) | |
| 11.3 Hybrid system verification (pg. 226) | |
| 11.3.1 C2E2 verification tool (pg. 227) | |
| 11.3.2 Example: Reachability analysis for PulseGen ‖ 026B30D Oscillator with C2E2 (pg. 228) | |
| 11.4 Example: Powertrain control system (pg. 228) | |
| 11.5 Verifying cyber-physical systems with incomplete models (pg. 229) | |
| 11.5.1 Hybrid automata with black-box modules (pg. 230) | |
| 11.5.2 Learning discrepancy from simulations (pg. 232) | |
| 11.5.3 DryVR verification tool (pg. 235) | |
| 11.6 Example: Analyzing risk in automatic emergency braking systems (pg. 236) | |
| 11.7 Example: Autonomous spacecraft rendezvous (pg. 237) | |
| 11.8 Further reading (pg. 241) | |
| 11.8.1 Related approaches, software tools, and applications (pg. 241) | |
| 11.8.2 Limitations and open problems (pg. 242) | |
| 11.8.3 Falsification (pg. 243) | |
| 11.8.4 Statistical model checking (pg. 243) | |
| 11.8.5 Verification for machine learning modules (pg. 244) | |
| 11.9 Exercises (pg. 244) | |
| Appendix A: Linear Algebra and Real Analysis (pg. 247) | |
| A.1 Sets and functions (pg. 247) | |
| A.1.1 Vectors and norms (pg. 247) | |
| A.1.2 Continuity and derivatives (pg. 248) | |
| A.1.3 Covers and partitions (pg. 248) | |
| A.2 Linear functions (pg. 249) | |
| A.3 Eigenvalues and eigenvectors (pg. 249) | |
| A.3.1 Positive definite matrices (pg. 250) | |
| A.3.2 Jordan normal form (pg. 250) | |
| A.3.3 Matrix norms (pg. 251) | |
| A.3.4 Interval matrices (pg. 251) | |
| A.4 Grönwall's inequality (pg. 252) | |
| Appendix B: Computability and Complexity (pg. 255) | |
| B.1 Computability (pg. 255) | |
| B.1.1 Turing machines (pg. 255) | |
| B.1.2 Configurations and computations (pg. 256) | |
| B.1.3 Language recognition and decidable languages (pg. 257) | |
| B.2 Complexity (pg. 258) | |
| B.2.1 Common complexity classes (pg. 258) | |
| B.3 Reasoning about the optimality of algorithms (pg. 260) | |
| B.3.1 Reductions (pg. 260) | |
| B.3.2 Completeness (pg. 261) | |
| Appendix C: Specification Language Reference (pg. 263) | |
| C.1 Conventions (pg. 263) | |
| C.2 Types (pg. 264) | |
| C.3 Formal arguments (pg. 264) | |
| C.4 Automaton declaration (pg. 265) | |
| C.5 Action declarations (pg. 265) | |
| C.6 Variables (pg. 266) | |
| C.7 Predicates and expressions (pg. 267) | |
| C.8 Transitions (pg. 267) | |
| C.9 Trajectories (pg. 268) | |
| C.10 Urgency (pg. 269) | |
| C.11 Modeling with nondeterminism (pg. 270) | |
| References (pg. 271) | |
| Index (pg. 291) | |
|
eTextbook
Go paperless today! Available online anytime, nothing to download or install.
Features
|
