Im Folgenden finden Sie einen Überblick über das Programm. Der Workshop wird über ein Zoom-Meeting ablaufen für welches Sie die Zugangsdaten von der Konferenzorganisation zugeschickt bekommen werden.

Über unseren Keynote Speaker Prof. Dr.-Ing. Markus Maurer

Markus Maurer studierte von 1987-1993 Elektrotechnik an der TU München. Im Jahr 2000 wurde er an der Universität der Bundeswehr zum Thema „Flexible Automatisierung von Straßenfahrzeugen mit Rechnersehen“ promoviert. Bei der Audi AG verantwortete er die Serienentwicklung von Systemen zur Abstandsregelung (ACC) und zur Anhaltewegverkürzung (AWV) und verschiedene Forschungsaktivitäten (Automatische Notbremse, Heading Control). Seit dem Jahr 2008 erforscht er als Professor für „Elektronische Fahrzeugsysteme“ an der TU Braunschweig Systeme für das automatisierte Fahren. In den letzten Jahren geht seine Forschungsgruppe vom inhärenten Risiko autonomer Straßenfahrzeuge aus. Sie erforscht und entwickelt Konzepte, Methoden und Algorithmen, um dieses Risiko für die Gesellschaft beherrschbar zu machen.

Programm

Uhrzeit Inhalt
13:30-13:35 Begrüßung
13:35-14:30 Keynote: Prof. Dr.-Ing. Markus Maurer
Das inhärente Risiko autonomer Straßenfahrzeuge
Autonomem Fahren wohnt ein inhärentes Risiko inne, das sich verringern nicht aber ganz eliminieren lässt. Markus Maurer motiviert dieses Risiko aus langjährigen Forschungs- und Entwicklungsarbeiten an automatisierten und assistierten Fahrzeugen. Die Risiken ergeben sich aus der Komplexität der Aufgabe in einer offenen Welt und der Komplexität der technische Systeme. Diese Bestandsaufnahme eint inzwischen die Expert*innen im Thema; Lösungsansätze sind noch nicht etabliert. Maurer skizziert zwei Entwicklungsparadigmen, die die Entwicklung von sicheren autonomen Fahrzeugen unterstützen sollen: Die wertebasierte Entwicklung und Safety-By-Design.
14:30-15:00 Jan Steffen Becker
Model Checking Amalthea with Spin
Although the Amalthea meta-model has emerged in the past years to an industrially adopted exchange format for (also safety-critical) embedded software architectures, model checking has been seldom applied to Amalthea models so far. This work presents a simple and extensible translation approach from Amalthea to Promela models for analysis with the widely used Spin model checker. This is a first step towards applying standard stae-of-the-art model checkers to Amalthea.
15:00-15:30 Pause
15:30-16:00 Marc Hentze
Determining Vehicle Test Sets for Over-the-Air Software Updates
Modern cars are highly customizable to satisfy the requirements and needs of different customers. This customization directly affects the car software, as it needs to adapt its behaviour according to the car configuration. However, the resulting software variability often causes millions of possible software variants. Hence, when aiming to deploy a software update, an exhaustive testing of all affected vehicles and their software variants is not feasible. To mitigate this problem, a small test set of vehicles needs to be determined that is as representative as possible while being small enough to allow the testing of each contained vehicle. In our talk, we present an automatic approach of determining the desired vehicle set and show the steps that were needed to realize it.
16:00-16:30 Prof. Dr. Paula Herber
Formal Verification of Intelligent Cyber-Physical Systemswith the Interactive Theorem Prover KeYmaera X
Cyber-physical systems are increasingly used in dynamic environments, and have to make safety-critical decisions autonomously. Machine learning is a powerful technique to make such decisions. For example, reinforcement learning can be used to learn controllers that outperform manually designed controllers in highly dynamic or uncertain environments. However, the learning process and the resulting controllers often impede system verification, as their behavior is hard to predict. To formally guarantee safety properties, a formal description is required, which is often not available in industrial design processes and hard to obtain for unpredictable machine learning components. In this talk, we present our current work on the semi-automatic deductive verification of intelligent cyber-physical systems. To support industrial design processes, we target the widely used modeling language Simulink together with its Reinforcement Learning Toolbox. To support deductive formal verification, we propose to use and extend our existing framework for the service-oriented verification of hybrid systems that are modeled in Simulink. The framework enables the automated transformation of Simulink models or services into differential dynamic logic and formal verification with the interactive theorem prover KeYmaera X.
16:30-17:00 Treffen der GI-Fachgruppe Automotive Software Engineering