In den letzten 15 Jahren ist die Anzahl der Steuergeräte in Oberklassefahrzeugen auf etwa 100 gestiegen, wobei der Großteil aller Innovationen durch Elektronik und Software entsteht. Dies macht Software zu einem entscheidenden Innovationstreiber in der Automobilindustrie, birgt jedoch auch Risiken, insbesondere durch Programmfehler. Das Testen komplexer Software-Systeme kann lediglich Fehler aufzeigen, jedoch nicht deren Abwesenheit. Formale Methoden bieten eine Garantie dafür, dass ein System die Anforderungen erfüllt. Die vorgestellten Ansätze zielen darauf ab, die Software-Entwicklung in kleinen und mittleren Unternehmen durch formale Verifikation zu verbessern. Der erste Ansatz analysiert Zeitanforderungen für eingebettete Systeme mithilfe von Model-Checking. Hierbei wird ein bestehendes Variantensystem für Steuergeräte modelliert und eine Einplanbarkeitsanalyse durchgeführt. Zudem wurde ein Framework zur Verwaltung der Varianten entwickelt, das eine bestehende Software-Plattform in eine Produktlinie umwandelt. Der zweite Ansatz fokussiert sich auf die Verifikation von Programmcode durch den Model-Checker Arcade. Die Binär-Code-Verifikation kann den Testaufwand verringern und bietet den Vorteil, das Ausbleiben von Fehlern zu beweisen, was mit herkömmlichem Testen nicht möglich ist.
