A case study of systematic top-down design of cyber-physical models with integrated validation and formal verification

Christoph Luckeneder, Hermann Kaindl

Publikation: Wissenschaftliche FachzeitschriftKonferenzartikelBegutachtung


Abstract models are required to handle the complexity for designing and verifying large-scale systems. An open problem is to consistently and systematically derive a more concrete model from an abstract model with regard to verification of its behavior against certain properties. Based on our recently proposed workflow for systematic top-down design of models of a Cyber-physical System (CPS), we present an in-depth case study of Adaptive Cruise Control (ACC). It includes both verification through model checking and validation in the sense that a refined model is checked for its fit with reality. This approach works top-down for designing a concrete model by starting from an abstract model. The resulting concrete model was validated and indirectly verified in this case study. In addition, we made a cross-check by verifying it directly on the concrete level. Hence, our case study provides some empirical evidence on the feasibility of this new workflow for top-down design of models.

Seiten (von - bis)1828-1836
FachzeitschriftProceedings of the ACM Symposium on Applied Computing
PublikationsstatusVeröffentlicht - 2019
Extern publiziertJa
Veranstaltung34th Annual ACM Symposium on Applied Computing, SAC 2019 - Limassol, Zypern
Dauer: 8 Apr. 201912 Apr. 2019

Bibliographische Notiz

Publisher Copyright:
© 2019 Copyright held by the owner/author(s). Publication rights licensed to ACM.