Controller verification meets controller code

Abstract

Cyber-physical systems are notoriously hard to verify due to the complex interaction between continuous physical behavior and discrete 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 verification method for cyber-physical systems, using flowpipe-based verification methods to verify legally binding requirements for electrified 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.

Authors 4

1. Felix Freiberger

   Saarland University

   Affiliation as printed

   Saarland University, Saarbrücken, Germany

2. Stefan Schupp Aachen TU Wien

   RWTH Aachen University · TU Wien

   Affiliation as printed

   TU Wien, Wien, Austria and RWTH Aachen University, Aachen, Germany

3. Holger Hermanns

   Saarland University

   Affiliation as printed

   Saarland University, Saarbrücken, Germany

4. Erika Ábrahám Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany