Die Softwareentwicklung im Automobilbereich ist gekennzeichnet durch die immer zahlreicheren, komplexeren und intelligenteren Steuerungen und durch den Trend zum Einsatz drahtloser Systeme (by-wire-Technik). Diese neuen Systeme, aber auch die schon eingesetzten Airbag oder ABS-Systeme implizieren höchste Sicherheitsansprüche an den gesamten Entwicklungsprozeß. Insbesondere im Bereich Softwareentwicklung sind traditonelles Handcodieren und intensives Unit-Testen nicht mehr zielführend. Methoden wie automatisches Codegenerieren, Simulation der Spezifikation und ähnliches sind seit einigen Jahren bekannt. Im vorliegenden Beitrag wird darüber hinaus ein Ansatz vorgestellt. der in der Luftfahrtindustrie erfolgreich zu sicheren Software-Entwicklung der fly-by-wire Systeme eingesetzt wird. Mit einer sehr formalen, synchronen Sprache wie LUSTRE und der Oberfläche SCADE werden Systeme mit dem Ziel beschrieben, deterministischen Code zu generieren, mit einem höchsten Qualitätsansprüchen genügenden Codegenerator (DO178B Level A) zu arbeiten und Vorteile dieser Spezifikationssprache - formale Verifikation - zusätzlich zur bekannten funktionalen Simulation zu benutzen. LUSTRE beinhaltet umfangreiche Semantikschecks, die neben normalen syntaktischen und Typenchecks auch Kausalität und Clocks abprüft. Die Erfahrung hat gezeigt, daß beide Checks sehr effektiv Modellierungsprobleme finden, welche mit anderen Verfahren kaum zu finden sind. Mit LUSTRE und seinen Vorteilen sowie einen möglichst automatischen Zusammenspiel mit einem Systembeschreibungswerkzeug wie MATLAB/SIMULINK entsteht ein durchgängiger Flow von der Spezifikation bis hin zum embedded Code. Ein weiterer Vorteil der formalen Sprache ist die Möglichkeit als zusätzliches Testwerkzeug die 'Formale Verifikation' (konkret Modelcheck) einzusetzen. Ziel ist es, die herkömmliche funktionale Systemsimulation zu unterstützen und den Testrahmen, die Testtiefe und den Umfang erheblich zu erweitern.