Muutke küpsiste eelistusi

Verifying Cyber-Physical Systems: A Path to Safe Autonomy [Kõva köide]

3.75/5 (8 hinnangut Goodreads-ist)
  • Formaat: Hardback, 304 pages, kõrgus x laius: 229x178 mm, 80 black and white illustrations
  • Sari: Cyber Physical Systems Series
  • Ilmumisaeg: 16-Feb-2021
  • Kirjastus: MIT Press
  • ISBN-10: 0262044803
  • ISBN-13: 9780262044806
Teised raamatud teemal:
Verifying Cyber-Physical Systems: A Path to Safe AutonomySuurem pilt
  • Formaat: Hardback, 304 pages, kõrgus x laius: 229x178 mm, 80 black and white illustrations
  • Sari: Cyber Physical Systems Series
  • Ilmumisaeg: 16-Feb-2021
  • Kirjastus: MIT Press
  • ISBN-10: 0262044803
  • ISBN-13: 9780262044806
Teised raamatud teemal:
Püsilink: https://www.kriso.ee/db/9780262044806.html
Märksõnad:
"A unified mathematical framework for rigorously modeling and analyzing cyber-physical systems"--

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