Principles of cyber-physical systems

A cyber-physical system consists of a collection of computing devices communicating with one another and interacting with the physical world via sensors and actuators in a feedback loop. Increasingly, such systems are everywhere, from smart buildings to medical devices to automobiles. This textbook offers a rigorous and comprehensive introduction to the principles of design, specification, modeling, and analysis of cyber-physical systems. The book draws on a diverse set of subdisciplines, including model-based design, concurrency theory, distributed algorithms, formal methods of specification and verification, control theory, real-time systems, and hybrid systems, explaining the core ideas from each that are relevant to system design and analysis.

The book explains how formal models provide mathematical abstractions to manage the complexity of a system design. It covers both synchronous and asynchronous models for concurrent computation, continuous-time models for dynamical systems, and hybrid systems for integrating discrete and continuous evolution. The role of correctness requirements in the design of reliable systems is illustrated with a range of specification formalisms and the associated techniques for formal verification. The topics include safety and liveness requirements, temporal logic, model checking, deductive verification, stability analysis of linear systems, and real-time scheduling algorithms. Principles of modeling, specification, and analysis are illustrated by constructing solutions to representative design problems from distributed algorithms, network protocols, control design, and robotics.

This book provides the rapidly expanding field of cyber-physical systems with a long-needed foundational text by an established authority. It is suitable for classroom use or as a reference for professionals.

Author Notes

Rajeev Alur is Zisman Family Professor of Computer and Information Science and Director of the Embedded Systems Masters program at the University of Pennsylvania.

Preface	p. xi
1 Introduction	p. 1
1.1 What Is a Cyber-Physical System?	p. 1
1.2 Key Features of Cyber-Physical Systems	p. 2
1.3 Overview of Topics	p. 5
1.4 Guide to Course Organization	p. 7
2 Synchronous Model	p. 13
2.1 Reactive Components	p. 13
2.1.1 Variables, Valuations, and Expressions	p. 13
2.1.2 Inputs, Outputs, and States	p. 14
2.1.3 Initialization	p. 15
2.1.4 Update	p. 16
2.1.5 Executions	p. 18
2.1.6 Extended-State Machines	p. 19
2.2 Properties of Components	p. 21
2.2.1 Finite-State Components	p. 21
2.2.2 Combinational Components	p. 22
2.2.3 Event-Triggered Components*	p. 24
2.2.4 Nondeterministic Components	p. 26
2.2.5 Input-Enabled Components	p. 29
2.2.6 Task Graphs and Await Dependencies	p. 30
2.3 Composing Components	p. 36
2.3.1 Block Diagrams	p. 36
2.3.2 Input/Output Variable Renaming	p. 38
2.3.3 Parallel Composition	p. 38
2.3.4 Output Hiding	p. 47
2.4 Synchronous Designs	p. 49
2.4.1 Synchronous Circuits	p. 50
2.4.2 Cruise Control System	p. 54
2.4.3 Synchronous Networks*	p. 58
Bibliographic Notes	p. 63
3 Safety Requirements	p. 65
3.1 Safety Specifications	p. 65
3.1.1 Invariants of Transition Systems	p. 65
3.1.2 Role of Requirements in System Design	p. 70
3.1.3 Safety Monitors	p. 75
3.2 Verifying Invariants	p. 78
3.2.1 Proving Invariants	p. 78
3.2.2 Automated Invariant Verification*	p. 85
3.2.3 Simulation-Based Analysis	p. 87
3.3 Enumerative Search*	p. 90
3.4 Symbolic Search	p. 97
3.4.1 Symbolic Transition Systems	p. 98
3.4.2 Symbolic Breadth-First Search	p. 103
3.4.3 Reduced Ordered Binary Decision Diagrams*	p. 109
Bibliographic Notes	p. 123
4 Asynchronous Model	p. 125
4.1 Asynchronous Processes	p. 125
4.1.1 States, Inputs, and Outputs	p. 126
4.1.2 Input. Output, and Internal Actions	p. 126
4.1.3 Executions	p. 131
4.1.4 Extended-State Machines	p. 132
4.1.5 Operations on Processes	p. 136
4.1.6 Safety Requirements	p. 141
4.2 Asynchronous Design Primitives	p. 142
4.2.1 Blocking vs. Non-blocking Synchronization	p. 142
4.2.2 Deadlocks	p. 143
4.2.3 Shared Memory	p. 145
4.2.4 Fairness Assumptions*	p. 154
4.3 Asynchronous Coordination Protocols	p. 162
4.3.1 Leader Election	p. 163
4.3.2 Reliable Transmission	p. 167
4.3.3 Wait-Free Consensus*	p. 170
Bibliographic Notes	p. 179
5 Liveness Requirements	p. 181
5.1 Temporal Logic	p. 181
5.1.1 Linear Temporal Logic	p. 182
5.1.2 LTL Specifications	p. 189
5.1.3 LTL Specifications for Asynchronous Processes*	p. 193
5.1.4 Beyond LTL*	p. 197
5.2 Model Checking	p. 199
5.2.1 Büchi Automata	p. 200
5.2.2 From LTL to Büchi Automata*	p. 206
5.2.3 Nested Depth-First Search*	p. 212
5.2.4 Symbolic Repeatability Checking	p. 216
5.3 Proving Liveness*	p. 222
5.3.1 Eventuality Properties	p. 222
5.3.2 Conditional Response Properties	p. 224
Bibliographic Notes	p. 229
6 Dynamical Systems	p. 231
6.1 Continuous-Time Models	p. 231
6.1.1 Continuously Evolving Inputs and Outputs	p. 231
6.1.2 Models with Disturbance	p. 241
6.1.3 Composing Components	p. 242
6.1.4 Stability	p. 243
6.2 Linear Systems	p. 247
6.2.1 Linearity	p. 248
6.2.2 Solutions of Linear Differential Equations	p. 251
6.2.3 Stability	p. 259
6.3 Designing Controllers	p. 263
6.3.1 Open-Loop vs. Feedback Controller	p. 263
6.3.2 Stabilizing Controller	p. 264
6.3.3 PID Controllers*	p. 269
6.4 Analysis Techniques*	p. 276
6.4.1 Numerical Simulation	p. 277
6.4.2 Barrier Certificates	p. 280
Bibliographic Notes	p. 287
7 Timed Model	p. 289
7.1 Timed Processes	p. 289
7.1.1 Timing-Based Light Switch	p. 289
7.1.2 Buffer with a Bounded Delay	p. 291
7.1.3 Multiple Clocks	p. 292
7.1.4 Formal Model	p. 294
7.1.5 Timed Process Composition	p. 297
7.1.6 Modeling Imperfect Clocks*	p. 300
7.2 Timing-Based Protocols	p. 301
7.2.1 Timing-Based Distributed Coordination	p. 302
7.2.2 Audio Control Protocol*	p. 305
7.2.3 Dual Chamber Implantable Pacemaker	p. 310
7.3 Timed Automata	p. 317
7.3.1 Model of Timed Automata	p. 318
7.3.2 Region Equivalence*	p. 319
7.3.3 Matrix-Based Representation for Symbolic Analysis	p. 328
Bibliographic Notes	p. 338
8 Real-Time Scheduling	p. 339
8.1 Scheduling Concepts	p. 339
8.1.1 Scheduler Architecture	p. 340
8.1.2 Periodic Job Model	p. 341
8.1.3 Schedulability	p. 345
8.1.4 Alternative Job Models	p. 350
8.2 EDF Scheduling	p. 352
8.2.1 EDF for Periodic Job Model	p. 352
8.2.2 Optimality of EDF	p. 356
8.2.3 Utilization-Based Schedulability Test	p. 358
8.3 Fixed-Priority Scheduling	p. 361
8.3.1 Deatuine-Monotonic and Rate-Monotonic Policies	p. 361
8.3.2 Optimality of Deadline-Monotonic Policy*	p. 365
8.3.3 Schedulability Test for Rate-Monotonic Policy*	p. 371
Bibliographic Notes	p. 378
9 Hybrid Systems	p. 379
9.1 Hybrid Dynamical Models	p. 379
9.1.1 Hybrid Processes	p. 379
9.1.2 Process Composition	p. 386
9.1.3 Zeno Behaviors	p. 389
9.1.4 Stability	p. 393
9.2 Designing Hybrid Systems	p. 395
9.2.1 Automated Guided Vehicle	p. 395
9.2.2 Obstacle Avoidance with Multi-robot Coordination	p. 398
9.2.3 Multi-hop Control Networks*	p. 406
9.3 Linear Hybrid Automata*	p. 413
9.3.1 Example Pursuit Game	p. 414
9.3.2 Formal Model	p. 417
9.3.3 Symbolic Reachability Analysis	p. 420
Bibliographic Notes	p. 430
Bibliography	p. 431
Index	p. 439

Available:*

On Order

Summary

Summary

Author Notes

Table of Contents