The Modeling and Analysis in Mobility Software Engineering research group deals with applied and theoretical methods in the field of autonomous driving. The central research question is: What requirements should an autonomous vehicle fulfill before it is allowed to share the roads of this world with us humans and how can these requirements be ensured? In order to answer this research question, three basic pillars of research are being pursued. The first research pillar deals with the formal specification of driving maneuvers, with which the maneuvers become machine-understandable and analyzable. The aim here is to map two key aspects of maneuvers: Spatial and temporal aspects. Spatial aspects include, for example, the fact that one vehicle is in front of another or that there is an intersection ahead. Temporal aspects include, for example, that actions happen one after the other (e.g. blinking before changing lanes) or take a certain amount of time. In this approach, spatial traffic logic and analysis methods for real-time automata are used to demonstrate the safety, reliability and other desirable properties of driving maneuvers.

The next research pillar raises the question: What should traffic rules for autonomous vehicles look like? It quickly becomes clear that regulations for humans, such as the German road traffic regulations (StVO), cannot be adopted "1 to 1": Natural language is imprecise and many rules require common sense, which cannot be directly transferred to autonomous systems. This focus area is working on a digital highway code for autonomous vehicles, which contains adapted traffic rules. In addition to the machine-readable formulation, the prioritization of traffic rules in exceptional cases, as well as legal and ethical issues, must also be considered for such a code. The last research pillar is aimed at the explainability and comprehensibility of complex systems. In times of increasing complexity of autonomous systems, the self-explanatory nature of decisions made by these machines becomes all the more important in order to strengthen user trust in the systems, but also to be able to understand and verify decisions. To this end, methods are being developed with which explanations can be automatically extracted from technical system models. In teaching, these topics will be addressed in a planned lecture on "Timed Systems", as well as in planned practical courses, seminars and topics for final theses.