Principles of Cyber-Physical Systems

by Rajeev Alur

A foundational text that offers a rigorous introduction to the principles of design, specification, modeling, and analysis 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.

464 pages, Hardcover

First published March 13, 2015

Reviews

[Zhaodan Kong · Rating 5 out of 5]

Next time you attend a control conference, you can try the following experiment: ask any person what a cyber-physical system is and then conduct a simple statistical analysis. One thing you will notice is that different researchers will have completely different opinions on even the definition of cyber-physical systems. But one thing they will agree on is that a cyber-physical system (CPS for short) should consist of two types of components, computing components (cyber part) and physical components (physical part), and the two should interact and communicate with each other.

This book gives a thorough overview of modeling, specification, analysis and design of cyber-physical systems. The content of this book have some overlaps with books on model checking and embedded systems, such as Principles of Model Checking by Christel Baier and Joost-Pieter Katoen and Introduction to Embedded Systems: A Cyber-Physical Systems Approach by Edward A. Lee and Snajit A. Seshia. But the emphasis of this book is on introducing a broad range of basis models, concepts and methods with many illustrative examples, I think quite rightly, considering the lack of introductory textbooks on such an important topic.

[Ron · Rating 5 out of 5]

This book provides an excellent introduction into the foudational topics of cyber-physical systems (hybrid and embedded systems). It introduces various reactive component models; sychronous, asynchronous, continous, and timed. The book also introduces hybrid systems (combinations of models). Aside from reactive models, the book also provides a basic introduction into formally describing, proving, and analyzing saftey and liveness requirments. Saftey requirements are described as boolean-valued invariants over the set of reacheable states (which potentially can be proved by induction, with or without inductive strengthening). A liveness requirment is described using linear-temporal logic (LTL) as a boolean-valued invariant over a trace (a sequence of valuations over a variable). I recommend the book to any graduate-level scientist or engineer looking for a non-repetitive and non-burdensome introduction to cyber-physical systems.