Verifying Cyber-Physical Systems: A Path to Safe Autonomy
- Length: 312 pages
- Edition: 1
- Language: English
- Publisher: The MIT Press
- Publication Date: 2021-02-16
- ISBN-10: 0262044803
- ISBN-13: 9780262044806
- Sales Rank: #222823 (See Top 100 Books)
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.
Cover Title Page Copyright Dedication Table of Contents Preface 1. Introduction 1.1. What is this book about? The verification problem 1.2. Testing and verification for establishing system requirements 1.3. From systems to models of systems 1.4. Design automation ecosystem 1.5. Challenges and state of the art 1.6. Road map 1.7. Learning and teaching using this book 2. Modeling Computation 2.1. Quick introduction to automata 2.1.1. Example: JK flip-flop 2.1.2. Language for specifying automata 2.2. Specifying automata 2.2.1. State variables and valuations 2.2.2. Predicates 2.2.3. Transitions 2.2.4. Automata 2.3. Special automata classes 2.3.1. Finite and discrete automata 2.3.2. Nondeterminism 2.3.3. Discrete sequences and sampled time 2.4. Semantics: Executions, reachable states, and invariants 2.5. Example: Dijkstra’s token ring algorithm 2.5.1. Legal states and invariants 2.5.2. Asynchronous and synchronous models 2.6. Example: Reasoning about impossibility 2.7. Exercises 3. Modeling Physics 3.1. Quick introduction to differential equations 3.1.1. Example: Vehicle speed control 3.1.2. Language for specifying differential equations 3.2. Specifying ordinary differential equations 3.2.1. State variables and valuations 3.2.2. Dense time and trajectories 3.2.3. Trajectories as solutions 3.3. Special classes of ODEs 3.3.1. Time-invariant and autonomous systems 3.3.2. Linear systems 3.4. Semantics: Reachable states, invariants, and stability 3.4.1. Example: Pendulum 3.4.2. Example: Kinematic vehicle model 3.5. Lyapunov’s direct method for proving stability 3.5.1. Stability of linear dynamical systems 3.6. Differential equations as automata 3.7. Example: Simple economy 3.8. Numerical simulations for ordinary differential equations 3.9. Closing the loop and control synthesis 3.9.1. Proportional-integral-derivative controller 3.9.2. Controller synthesis problem 3.10. Exercises 4. Modeling Cyber-Physical Systems 4.1. Quick introduction to hybrid automata 4.1.1. Example: Rimless wheel 4.1.2. Language for specifying hybrid systems 4.2. Specifying hybrid automata 4.2.1. State variables and transitions 4.2.2. Trajectories and closures 4.2.3. Hybrid automata 4.2.4. A guide for hybrid modeling 4.3. Special classes of hybrid automata 4.3.1. Deterministic hybrid automata 4.3.2. Switched systems 4.3.3. Linear hybrid automata 4.3.4. Example: Thermostat 4.3.5. Rectangular hybrid automata 4.3.6. Timed automata 4.4. Semantics: Hybrid executions 4.4.1. Numerical simulation of hybrid executions 4.4.2. Reachable states, invariants, and stability 4.4.3. Time-abstract semantics 4.4.4. Execution zoo 4.5. Example: Spacecraft docking 4.6. Example: Small aircraft traffic management system 4.7. Exercises 5. Composing Models 5.1. Composing automata 5.2. Composing input/output automata 5.2.1. Input/output automata 5.2.2. Compatibility and composition of input/output automata 5.3. Example: Channels, logical clocks, and distributed systems 5.3.1. First-in, first-out channels 5.3.2. Logical time in distributed systems: Lamport clocks 5.3.3. Composed system: A network of processes communicating over channels 5.3.4. Traces and projections 5.4. Composing hybrid input/output automata 5.4.1. Hybrid input/output automata 5.4.2. Compatibility and composition of hybrid input/output automata 5.5. Example: Interconnecting flip-flops 5.6. Example: Timed channels 5.7. Example: Pulse generator and oscillator 5.8. Traces, untiming, and properties of compositions 5.9. Example: Emergency braking on highways 5.10. Exercises 6. Specifying Requirements 6.1. Requirements analysis 6.2. Safety standards 6.2.1. DO-178C 6.2.2. ISO 26262 6.2.3. Beyond current safety standards and requirements 6.3. From requirements to verification 6.3.1. Formal verification algorithms 6.3.2. Resources for verification and computational complexity 6.3.3. Invariants and safety requirements 6.3.4. Progress requirements 6.4. Linear temporal logic 6.4.1. Background definitions 6.4.2. LTL syntax 6.4.3. LTL semantics 6.5. Computational tree logic 6.5.1. Computational tree logic syntax 6.5.2. Computational tree logic semantics 6.5.3. Expressiveness of linear temporal logic and computational tree logic 6.6. Further reading 6.6.1. Checking temporal logic models 6.6.2. Planning and synthesis with temporal logics 6.6.3. Dense time, signal, and stochastic temporal logics 6.6.4. Runtime verification and monitoring 6.7. Exercises 7. Verifying Invariants 7.1. Quick introduction to proving invariants 7.2. Reasoning with inductive invariants 7.2.1. Invariance and composition 7.3. Proving timing-based mutual exclusion 7.3.1. Example: Fischer’s mutual exclusion 7.3.2. Analysis of Fischer’s mutual exclusion 7.4. Proving inductive invariants without solving ordinary differential equations 7.4.1. Example: Checking subtangential conditions 7.4.2. Barrier certificates 7.5. Satisfiability and satisfiability modulo theories 7.5.1. Satisfiability 7.5.2. Satisfiability modulo theory 7.5.3. Modeling for satisfiability and satisfiability modulo theory 7.6. Further reading 7.6.1. Finding and learning invariants 7.7. Exercises 8. Abstractions and Compositional Reasoning 8.1. Quick introduction to abstractions: Timing abstraction 8.2. Abstraction definitions 8.3. Proving abstractions: Simulation relations 8.4. Bisimulations and time-abstract bisimulations 8.4.1. Untiming and bisimulations 8.4.2. Example: Simulation and trace inclusion 8.4.3. Backward simulations 8.5. Hybridization 8.6. Substituting with abstractions 8.7. Designing a CEGAR-based cyber-physical verification system 8.7.1. Space of abstractions 8.7.2. Model checker 8.7.3. Counterexample validation 8.7.4. Refinement strategy 8.8. Further reading 8.9. Exercises 9. Reachability Analysis 9.1. Quick introduction to reachability analysis 9.2. Finite automata 9.2.1. Finite state reachability 9.3. Timed automata 9.3.1. Syntax for timed automata 9.3.2. Example: Timed light switch 9.3.3. Clock equivalence relation on states 9.3.4. Control state reachability and region automata 9.4. Integral timed automata to rectangular hybrid automata 9.4.1. Rational timed automata 9.4.2. Multirate automata 9.4.3. Rectangular hybrid automata 9.5. Undecidability of control state reachability for rectangular hybrid automata 9.5.1. Two-counter machines 9.5.2. Reduction of control state reachability of rectangular hybrid automata to the halting problem of two-counter machines 9.5.3. Initialized rectangular hybrid automata 9.6. Relaxing the verification problem 9.6.1. Bounded reachability analysis 9.7. Data structures for reachability analysis 9.7.1. Rectangles 9.7.2. Polytopes 9.7.3. Zonotopes 9.7.4. Ellipsoids 9.8. Exercises 10. Progress Analysis 10.1. Quick introduction to progress 10.2. Termination of discrete-time automata 10.2.1. Termination with well-founded relations 10.2.2. Example: UpDown counter 10.2.3. Termination with disjunctive well-founded relations 10.2.4. Example: UpDown revisited 10.3. Self-stabilization 10.3.1. Example: Distributed minimum spanning tree algorithm 10.3.2. Stabilization of the minimum spanning tree algorithm 10.4. Convergence and stability of asynchronous systems without metrics 10.4.1. Convergence for finite state systems 10.5. Stability proofs for dynamical systems 10.6. Stability of hybrid automata 10.6.1. Common Lyapunov functions 10.6.2. Multiple Lyapunov functions 10.6.3. Stability under slow switching: Average dwell time 10.7. Exercises 11. Data-Driven Verification 11.1. Quick introduction to data-driven safety verification 11.1.1. Discrepancy functions 11.1.2. BasicSimReach algorithm 11.1.3. Example: Moore-Greitzer jet engine 11.2. Computing discrepancy 11.2.1. Linear dynamical systems 11.2.2. Nonlinear dynamical systems: Optimization approaches 11.2.3. Nonlinear models: Local discrepancy 11.3. Hybrid system verification 11.3.1. C2E2 verification tool 11.3.2. Example: Reachability analysis for PulseGen. ∥ Oscillator with C2E2 11.4. Example: Powertrain control system 11.5. Verifying cyber-physical systems with incomplete models 11.5.1. Hybrid automata with black-box modules 11.5.2. Learning discrepancy from simulations 11.5.3. DryVR verification tool 11.6. Example: Analyzing risk in automatic emergency braking systems 11.7. Example: Autonomous spacecraft rendezvous 11.8. Further reading 11.8.1. Related approaches, software tools, and applications 11.8.2. Limitations and open problems 11.8.3. Falsification 11.8.4. Statistical model checking 11.8.5. Verification for machine learning modules 11.9. Exercises Appendix A: Linear Algebra and Real Analysis A.1. Sets and functions A.1.1. Vectors and norms A.1.2. Continuity and derivatives A.1.3. Covers and partitions A.2. Linear functions A.3. Eigenvalues and eigenvectors A.3.1. Positive definite matrices A.3.2. Jordan normal form A.3.3. Matrix norms A.3.4. Interval matrices A.4. Grönwall’s inequality Appendix B: Computability and Complexity B.1. Computability B.1.1. Turing machines B.1.2. Configurations and computations B.1.3. Language recognition and decidable languages B.2. Complexity B.2.1. Common complexity classes B.3. Reasoning about the optimality of algorithms B.3.1. Reductions B.3.2. Completeness Appendix C: Specification Language Reference C.1. Conventions C.2. Types C.3. Formal arguments C.4. Automaton declaration C.5. Action declarations C.6. Variables C.7. Predicates and expressions C.8. Transitions C.9. Trajectories C.10. Urgency C.11. Modeling with nondeterminism References Index
Donate to keep this site alive
1. Disable the AdBlock plugin. Otherwise, you may not get any links.
2. Solve the CAPTCHA.
3. Click download link.
4. Lead to download server to download.