Abstract Traditionally, extensive vehicle testing is applied to assure the robustness and safety of automotive systems. This approach is highly challenged by increasing system complexity. Formal verification lends a powerful framework for model-based safety assurance, but due to the mixed discrete–continuous behavior of automotive systems, traditional tools for discrete program verification are helpful but not sufficient. In academia, during the last two decades new approaches arose for the formal verification of such mixed discrete-continuous systems. However, the industry is not fully aware of this development, the tools are seldom tried and their applicability is not well examined. In a Ford–RWTH research alliance project, we aimed at evaluating the potential of knowledge and technology transfer in this area. This paper has two main objectives. Firstly, we want to report on the state-of-the-art in the above-mentioned academic development in a generally understandable form, targeted to interested potential users. Secondly, we want to share our observations after testing different available tools for their applicability and usability in the automotive sector and as a conclusion devise some recommendations.

Over the last decades, the development of algorithms and tools for the safety verification of hybrid systems has been content of intensive research. Numerous novel ideas have been presented and implemented in different tools. Whereas the majority of these tools offer fixed implementations, only few general libraries have been provided for the development of new verification tools. HyPro is such an example, providing a C++ programming library for the implementation of certain types of reachability analysis algorithms for linear hybrid systems. These algorithms, based on flowpipe construction, need geometric or symbolic representation for state sets of hybrid systems. HyPro offers datatypes for different representations, conversions between them, and efficient algorithms based on these datatypes. Since its release in 2017, HyPro's functionalities have been extended by several implementations. In this paper we give a general introduction to flowpipe-construction-based methods and report on HyPro's functional advances as well as on applications of the library.

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.