Rajeev Alur: Principles of Cyber-Physical Systems
Summary
The book Principles of Cyber-Physical Systems by Rajeev Alur introduces the principles of design, specification, modeling and analysis of cyber-physical systems with compositional modeling at its heart. This textbook – written with incredible care and attention to pedagogical detail – covers all the relevant fundamental notions. A host of carefully designed exercises should allow it to be used both as course material and for self-study.
This review is written by Uli Fahrenberg for FME’s Book Review Committee (BRC). The aim of the BRC is to provide to the formal methods community, and to the scientific community in general, high-quality reviews of books on topics of interest to the community.
Principles of Cyber-Physical Systems
by
TRajeev Alur.
Review
This textbook is an extensive and very careful introduction to the principles of design, specification, modeling and analysis of cyber-physical systems. It has compositional modeling at its heart, covering both synchronous and asynchronous models using input-output block diagrams. Specifications are introduced in two stages, first safety requirements using reachability analysis and then, more generally, liveness specifications using linear temporal logic.
The later chapters introduce dynamical systems, timed models, real-time scheduling and hybrid systems. The chapter on dynamical systems gives a brief introduction to control theory, covering linear dynamical systems, Lyapunov stability and bounded-input-output stability, controller design up to PID controllers, and analysis using numerical methods and barrier certificates.
The chapter on timed models is based on a version of timed automata, but uses a graphical input-output presentation consistent with the rest of the book. It introduces timed processes and their composition and proceeds to zone-based reachability analysis. The chapter on real-time scheduling covers basic scheduler architecture and schedulability and then introduces Earliest Deadline First (EDF) and fixed-priority scheduling in detail.
The final chapter on hybrid systems combines the material introduced for dynamical systems and for timed models. After some examples which also cover Zeno behavior in detail, it procedes to stability and hybrid systems design. The final section treats linear hybrid automata and their symbolic reachability analysis.
This is a textbook written with incredible care and attention to pedagogical detail. It is easy to read and full of examples, but lacks nothing in precision. To give but one illustration, the first section of the final chapter on hybrid systems starts with an introduction to hybrid processes using the well-known thermostat and bouncing-ball examples, then goes into process composition, again both formally and by example, only to notice that the bouncing ball exhibits Zeno behavior (again introduced both formally and using examples) and how this effects the composition of “a ball bouncing next to [a] thermostat”.
In conclusion, this text is an extensive and readable introduction to cyber-physical systems. A host of carefully designed exercises should allow it to be used as course material (advanced under-graduate or graduate), as well as for self-study. The end-of-chapter bibliographic notes provide plenty of material for further study.
The book is also suitable as a reference for researchers. All that is required as background is some mathematical maturity easily acquired during the first years of undergraduate study.