Chuchu Fan: Formal Methods for Safe Autonomy: Data-driven Verification, Synthesis, and Applications
ACM, October 2024, 184 pp, ISBN: 979-8-4007-0865-7. https://dl.acm.org/doi/book/10.1145/3603288
Summary
The book Formal Methods for Safe Autonomy: Data-driven Verification, Synthesis, and Applications by Chuchu Fan sets forth a vision for formal verification of cyber-physical systems recast in the data-driven age. By making simulators an integral part of the verification and synthesis processes, the book introduces a family of scalable algorithms that provide guarantees of safe autonomy and illustrates them on a set of formally validated applications. Achieving scalability while maintaining the rigor of formal methods is what sets this work apart from previous approaches.
Although not primarily intended as an introductory text, this book can nonetheless serve as a solid entry point into formal verification and synthesis of cyber-physical systems, particularly for graduate students and researchers with an interest in the field. The included examples and case studies make it a valuable resource for teaching.
This review is written by Thao Dang 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.
Formal Methods for Safe Autonomy: Data-driven Verification, Synthesis, and Applications
by Chuchu Fan.
Review
Autonomous systems increasingly inhabit safety-critical domains where failures can have serious consequences. It is within this demanding context that Formal Methods for Safe Autonomy: Data- driven Verification, Synthesis, and Applications by Chuchu Fan makes a timely and remarkable contribution. The book builds upon a doctoral dissertation honored with the 2020 ACM Doctoral Dissertation Award, translating theoretical innovations into practical applications in the formal verification of cyber-physical systems (CPS) and redefining the boundary between theory and practice.
This refreshing and groundbreaking book appeals to both specialists and a broader audience. It goes beyond a treatise on solutions and algorithms; it sets forth a vision for how formal methods— traditionally seen as too computationally expensive for industrial-scale systems—can be recast in the data-driven age. Ensuring the safety of autonomous systems is not a matter of incrementally improving existing testing methodologies. The brute-force approach of simulation and field testing faces an insurmountable limitation: the combinatorial explosion of system states and decision choices. Another critical limitation is coverage. No matter how many tests are run, there will always be untested scenarios—rare corner cases that often lead to failures. Formal methods are pivotal in tackling this issue. By mathematically reasoning about models, they aim to prove properties that hold across infinitely many executions. Yet here lies the obstacle: models of real-world systems are rarely simple. They are nonlinear, hybrid, high-dimensional, and often incomplete. Traditional formal methods, while elegant, stumble on these complexities. Indeed, the pioneering works of the 1990s and early 2000s laid theoretical foundations but struggled to scale. For years, critics regarded them as primarily academic studies—strong in theory but with limited practical relevance. This book provides strong evidence that such skepticism is increasingly unwarranted.
The central idea of the book is that formal verification and synthesis can be made practi- cal by embracing data. Rather than relying solely on models—which are often unavailable or incomplete—the methods developed here combine mathematical reasoning with simulation data. In doing so, they bridge the gap between the rigor of proofs and the complexity and unknowns of real-world systems. This paradigm shift is subtle but profound. By making simulators an integral part of the verification process, the book introduces a family of scalable algorithms that provide guarantees of safe autonomy. This balance—achieving scalability while maintaining rigor—is what sets this work apart from previous approaches.
The first four chapters present an introduction to the topic of the book, notations, and back- ground including the models used for describing the behaviors of autonomous systems and CPS, sensitivity analysis and its use in existing data-driven verification approaches. The major contri- butions of the book are presented in the following four chapters. Chapter 5 presents an algorithm, based on simulation traces and the computation of discrep- ancy functions, capable of over-approximating reachable states for nonlinear systems with locally optimal tightness. The integration of learning theory into verification—through the PAC (Prob- ably Approximately Correct) framework, for instance—foreshadows the challenges posed by the increasing role of machine learning in autonomous systems. This book offers a blueprint for how such integration can be approached.
Chapter 6 describes the DryVR (Data-driven System for Verification and Reasoning) frame- work for models with black-box components. Real-world systems often include components that defy accurate modeling. The DryVR framework innovatively treats such systems as combinations of “white-box” and “black-box” components. By using learning-based methods to approximate sensitivity, DryVR can deliver probabilistic guarantees—a contribution especially relevant in to- day’s era of AI-driven autonomy.
Chapter 7 deals with partial order reduction. In distributed autonomous systems, concur- rent actions lead to a combinatorial explosion in possible interleavings. Classical partial order reduction is too strict, requiring exact commutativity. The approximate version introduced here relaxes the commutativity notion, yielding exponential reductions in explored executions while still maintaining meaningful safety guarantees.
Moving beyond verification, Chapter 8 presents a scalable controller synthesis technique, im- plemented in the tool RealSyn. By considering a combination of an open-loop controller and a tracking controller and reformulating synthesis problems into satisfiability modulo theories (SMT), the RealSyn tool can efficiently handle linear systems under disturbances. Together, these contributions constitute a toolset—comprising Compare Execute Check En- gine (C2E2) for verification of hybrid systems, DryVR for verification of systems with black-box components, and RealSyn for controller synthesis—and a set of formally validated applications— such as a suite of Toyota engine control modules, satellite rendezvous protocols, and an advanced driver assistance system (ADAS).
Although not primarily intended as an introductory text, this book can nonetheless serve as a solid entry point into formal verification and synthesis of cyber-physical systems, particularly for graduate students and researchers with an interest in the field. The included examples and case studies make it a valuable resource for teaching. Due to its focus on a specific methodological approach, a background in logic, dynamical systems, model checking, and controller synthesis is required for a deep understanding. The bibliography, however, is extensive and offers a well- curated overview of the relevant literature.
In conclusion, Formal Methods for Safe Autonomy: Data-driven Verification, Synthesis, and Applications embodies exactly what the field of autonomous systems needs today: scalable tech- niques, certifiable guarantees, and a firm focus on safety. It is well positioned to become a key reference for both researchers and practitioners, contributing meaningfully to the future of safe autonomous systems.