★This is a clear, practical guide to designing safe and verifiable medical cyber-physical systems.

Biomedical systems—such as pacemakers and automated insulin pumps—are Cyber-Physical Systems (CPSs) that must operate safely and reliably at all times. This book introduces a systematic design methodology for Medical CPSs (MCPSs) using the synchronous approach, which ensures deterministic and reactive execution—key to safety-critical performance.

Through a detailed case study of a pacemaker and a modeled human heart, this book demonstrates how the synchronous approach enables accurate modeling, verification, and automated code generation. Using the SCCharts language, readers learn how to model the cardiac conduction system and a DDD-mode pacemaker, derive embedded implementations, and validate them via a synchronous heart simulator.

The book then covers formal verification using the UPPAAL model checker, followed by run-time verification methods that form the foundation for preventing adversarial attacks. It concludes with references to open-source tools and future research directions relevant to the CPS community.

Dr. Hammond Pearce
a Senior Lecturer (a.k.a. Assistant Professor) at UNSW Sydney's School of Computer Science and Engineering.
His main research focus is in hardware and software cybersecurity, including embedded systems, cyber-physical systems, and additive manufacturing. He also examines the implications of machine learning (ML) on design and applications in this space. He is particularly interested in how AI might be leveraged for new design strategies, including automated code writing and bug repair. As part of this work he won the inaugural Efabless AI-Generated Open-Source Silicon Design Challenge, the IEEE S&P Distinguished Paper award, and the ACM TODAES Best Paper Award.
He received the B.E. (Hons) degree in Computer Systems Engineering in 2014 and the Ph.D. in Computer Systems Engineering in 2020 both from the University of Auckland, Auckland, New Zealand. In 2019 he took part in the NASA International Internship Programme and worked at NASA Ames in California, and he has also worked in several industry positions, including as a full-stack web developer and as an electronics contractor working on Li-ion battery management systems.

He teaches COMP3601 Design Project A, where students are introduced to complex FPGA development via the development of a large group project.

Partha Roop
Partha is the Professor and Head of the Department of Electrical and Computer and Software Engineering at the University of Auckland:.
Partha's research interests are in safety of AI, ethical AI, and AI applications in cyber-physical systems in digital health, autonomous systems and Machine Learning for Real-Time Systems. His work has both academic and industrial uptake.
Earlier, he co-founded APIMatic: apimatic.io, a cloud services company with two of his PhD students, which is a global leader on automatic SDK generation from APIs. His work on digital twins of human organs, such as the heart and the gut has influenced the work of major partners on this topic such as Mathworks.
Partha is the co-editor-in-chief of ACM Books: ACM Books Editorial Board