[Back]


Talks and Poster Presentations (with Proceedings-Entry):

F. Freiberger, S. Schupp, H. Hermanns, E. Abraham:
"Controller Verification meets Controller Code: A Case Study";
Talk: MEMOCODE'21: the 19th ACM-IEEE International Conference on Formal Methods and Models for System Design, Beijing, China (Online due to Covid); 2021-11-20 - 2021-11-22; in: "19th ACM-IEEE International Conference on Formal Methods and Models for System Design", Association for Computing Machinery, New York, NY, United States (2021), ISBN: 978-1-4503-9127-6; 98 - 103.



English abstract:
Cyber-physical systems are notoriously hard to verify due to the
complex interaction between continuous physical behavior and dis-
crete control. A widespread and important class is formed by digital
controllers that operate on fixed control cycles to interact with the
physical environment they are embedded in. This paper presents
a case study for integrating such controllers into a rigorous verifi-
cation method for cyber-physical systems, using flowpipe-based
verification methods to verify legally binding requirements for elec-
trified vehicles to a custom bike design. The controller is integrated
in the underlying model in a way that correctly represents the input
discretization performed by any digital controller.

German abstract:
Cyber-physical systems sind wegen der komplexen Interaktion von kontinuierlichen und diskreten Verhalten bekanntermaßen schwer zu verifizieren. Eine verbreitete und wichtige Klasse dieser Systeme wird durch die periodische Interaktion von digitalen Regelungen mit physikalischen Entitäten gebildet. Diese Arbeit präsentiert eine Fallstudie, in der diese Art von Regelungen in eine rigorose Verifikationsmethode für CPS eingebunden wird. Dabei wird eine Flowpipe-basierte Verifikationsmethode verwendet, um rechtliche Anforderungen an die Betriebnahme von elektrifizierten Zweirädern für ein maßgeschneidertes Zweirad zu verifizieren. Die Regelung ist dabei verlustfrei inklusiver der Diskretisierung der Eingabe in das zugrundeliegende Modell des Zweirades integriert

Keywords:
Controller, hybrid automata, verification


"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
http://dx.doi.org/10.1145/3487212.3487337


Created from the Publication Database of the Vienna University of Technology.