Name of participant: Till Schallau
Project’s name: A Domain-Specific Language for Verifying Behavioral Requirements of Autonomous Vehicles (VeRBAL)
Project description:
The project VeRBAL develops a domain-specific language (DSL) for the formal specification and validation of behavioral requirements for autonomous driving systems.
Motivation
Autonomous vehicles must follow complex traffic regulations and safety norms. These are typically expressed in natural language and legal terms, which are often ambiguous or underspecified. As a result, transferring such requirements into testable, machine-readable formats remains a major challenge. This gap complicates the verification of correct system behavior under realistic conditions and hinders safety certification processes.
Project Goal
VeRBAL aims to make formal methods usable for domain experts without a background in logic or programming. The core idea is to provide an intuitive, structured and visual DSL that allows experts to express behavioral expectations, such as traffic rules or safety constraints, in a way that is both understandable and formally precise. These specifications are then automatically translated into logical monitors for validating system behavior on recorded real-world or simulated driving data.
The DSL is implemented using the JetBrains MPS platform and builds on the logic CMFTBL (Counting Metric First-Order Temporal Binding Logic), enabling rich temporal and contextual reasoning. Through this, requirements can capture, for instance, whether a vehicle stops before a red light, maintains safe distances, or reacts correctly to pedestrian crossings.
Impact
VeRBAL enables non-technical domain experts, such as legal analysts or safety engineers, to formally define what constitutes correct behavior for autonomous vehicles, without writing a single line of code or formal logic. The DSL bridges the gap between natural-language traffic laws and executable logic, making legal requirements operational.
Software Campus Partner: TU Dortmund and Volkswagen AG
Implementation period: 01.05.2025 – 31.12.2026
