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

Abstract

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
PublisherSpringer
Publication date2019
Pages452-477
ISBN (Print)978-3-319-91907-2
ISBN (Electronic)978-3-319-91908-9
DOIs
Publication statusPublished - 2019
SeriesLecture Notes in Computer Science
Volume10000
ISSN0302-9743

Fingerprint

Systems analysis
Pacemakers
Temporal logic
Controllers
Monitoring
Chemical analysis

Cite this

Alur, R., Giacobbe, M., Henzinger, T., Larsen, K. G., & Mikučionis, M. (2019). Continuous-Time Models for System Design and Analysis. In Computing and Software Services (pp. 452-477). Heidelberg: Springer. Lecture Notes in Computer Science, Vol.. 10000 https://doi.org/10.1007/978-3-319-91908-9_22
Alur, Rajeev ; Giacobbe, Mirco ; Henzinger, Thomas ; Larsen, Kim Guldstrand ; Mikučionis, Marius. / Continuous-Time Models for System Design and Analysis. Computing and Software Services. Heidelberg : Springer, 2019. pp. 452-477 (Lecture Notes in Computer Science, Vol. 10000).
@inbook{9074fb264de64095a2a46460aac28ddb,
title = "Continuous-Time Models for System Design and Analysis",
abstract = "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.",
author = "Rajeev Alur and Mirco Giacobbe and Thomas Henzinger and Larsen, {Kim Guldstrand} and Marius Mikučionis",
year = "2019",
doi = "10.1007/978-3-319-91908-9_22",
language = "English",
isbn = "978-3-319-91907-2",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "452--477",
booktitle = "Computing and Software Services",
address = "Germany",

}

Alur, R, Giacobbe, M, Henzinger, T, Larsen, KG & Mikučionis, M 2019, Continuous-Time Models for System Design and Analysis. in Computing and Software Services. Springer, Heidelberg, Lecture Notes in Computer Science, vol. 10000, pp. 452-477. https://doi.org/10.1007/978-3-319-91908-9_22

Continuous-Time Models for System Design and Analysis. / Alur, Rajeev; Giacobbe, Mirco; Henzinger, Thomas; Larsen, Kim Guldstrand; Mikučionis, Marius.

Computing and Software Services. Heidelberg : Springer, 2019. p. 452-477 (Lecture Notes in Computer Science, Vol. 10000).

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

TY - CHAP

T1 - Continuous-Time Models for System Design and Analysis

AU - Alur, Rajeev

AU - Giacobbe, Mirco

AU - Henzinger, Thomas

AU - Larsen, Kim Guldstrand

AU - Mikučionis, Marius

PY - 2019

Y1 - 2019

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-91908-9_22

DO - 10.1007/978-3-319-91908-9_22

M3 - Book chapter

SN - 978-3-319-91907-2

T3 - Lecture Notes in Computer Science

SP - 452

EP - 477

BT - Computing and Software Services

PB - Springer

CY - Heidelberg

ER -

Alur R, Giacobbe M, Henzinger T, Larsen KG, Mikučionis M. Continuous-Time Models for System Design and Analysis. In Computing and Software Services. Heidelberg: Springer. 2019. p. 452-477. (Lecture Notes in Computer Science, Vol. 10000). https://doi.org/10.1007/978-3-319-91908-9_22