Continuous-Time Models for System Design and Analysis

Rajeev Alur, Mirco Giacobbe, Thomas Henzinger, Kim Guldstrand Larsen, Marius Mikučionis

Research output: Contribution to book/anthology/report/conference proceedingBook chapterResearchpeer-review

11 Citations (Scopus)


We illustrate the ingredients of the state-of-the-art of model-based approach for the formal design and verification of cyber-physical systems. To capture the interaction between a discrete controller and its continuously evolving environment, we use the formal models of timed and hybrid automata. We explain the steps of modeling and verification in the tools Uppaal and SpaceEx using a case study based on a dual-chamber implantable pacemaker monitoring a human heart. We show how to design a model as a composition of components, how to construct models at varying levels of detail, how to establish that one model is an abstraction of another, how to specify correctness requirements using temporal logic, and how to verify that a model satisfies a logical requirement.
Original languageEnglish
Title of host publicationComputing and Software Services
Place of PublicationHeidelberg
Publication date2019
ISBN (Print)978-3-319-91907-2
ISBN (Electronic)978-3-319-91908-9
Publication statusPublished - 2019
SeriesLecture Notes in Computer Science


Dive into the research topics of 'Continuous-Time Models for System Design and Analysis'. Together they form a unique fingerprint.

Cite this