Der nächste große Innovationsschritt in der Automobilbranche wird der Übergang zu immer umfassenderen Fahrerassistenzsystemen (ADAS) und automatischen Fahrfunktionen (ADF) sein. Vollautomatisiert fahrende Fahrzeuge müssen jederzeit in der Lage sein, alle möglichen Verkehrs- und Notsituationen sicher zu bewältigen. Ein entscheidendes Kriterium für die Einführung und gesellschaftliche Akzeptanz von ADF ist die Erhaltung oder Verbesserung dieses hohen Sicherheitsniveaus. Um dies zu gewährleisten sind effiziente Test- und Validierungstechniken unabdingbar. BTC-ES hat spezifisches Know-How im Bereich formaler Prüfungen für sicherheitskritische Systeme. Dieses Know-How wird BTC-ES einbringen, um automatisiert eine formale Prüfung von Anforderungen für ADAS und ADF Systeme zu ermöglichen. Diese geprüften Anforderungen sind dann eine solide Basis für die folgenden Engineering Phasen. In ENABLE-S3 wird BTC an der formalen Spezifikation von sicherheitskritischen Anforderungen arbeiten. Aus diesen formalen Anforderungen können C-Observer generiert werden, die als Diagnoseeinheiten in Testumgebungen eingebettet werden können. Weiterhin strebt BTC an, formale Spezifikationenen auf Konsistenz und Korrektheit zu prüfen, um schon früh Fehler und Inkonsistenzen in den Anforderungen aufzudecken. Dazu muss das existierende Werkzeug BTC EmbeddedSpecifier um entsprechende formale Checks erweiter werden. BTC-ES wird den Use Case Provider DENSO Automotive aktiv bei der Formalisierung seiner Anforderungen sowie bei der Anwendung der formalen Methoden unterstützen.